Abstractions for hybrid systems
Identifieur interne : 004E51 ( Main/Merge ); précédent : 004E50; suivant : 004E52Abstractions for hybrid systems
Auteurs : Ashish Tiwari [États-Unis]Source :
- Formal Methods in System Design [ 0925-9856 ] ; 2008-02-01.
English descriptors
Abstract
Abstract: We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.
Url:
DOI: 10.1007/s10703-007-0044-3
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001E18
- to stream Istex, to step Curation: 001D95
- to stream Istex, to step Checkpoint: 001102
Links to Exploration step
ISTEX:8213F313ABB512ED9F185E98E24159FB0521BEA4Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Abstractions for hybrid systems</title>
<author><name sortKey="Tiwari, Ashish" sort="Tiwari, Ashish" uniqKey="Tiwari A" first="Ashish" last="Tiwari">Ashish Tiwari</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:8213F313ABB512ED9F185E98E24159FB0521BEA4</idno>
<date when="2007" year="2007">2007</date>
<idno type="doi">10.1007/s10703-007-0044-3</idno>
<idno type="url">https://api.istex.fr/ark:/67375/VQC-3M5V64DC-S/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001E18</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001E18</idno>
<idno type="wicri:Area/Istex/Curation">001D95</idno>
<idno type="wicri:Area/Istex/Checkpoint">001102</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001102</idno>
<idno type="wicri:doubleKey">0925-9856:2007:Tiwari A:abstractions:for:hybrid</idno>
<idno type="wicri:Area/Main/Merge">004E51</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Abstractions for hybrid systems</title>
<author><name sortKey="Tiwari, Ashish" sort="Tiwari, Ashish" uniqKey="Tiwari A" first="Ashish" last="Tiwari">Ashish Tiwari</name>
<affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country>
<wicri:regionArea>SRI International, 333 Ravenswood Ave., Menlo Park, CA</wicri:regionArea>
<placeName><region type="state">Californie</region>
</placeName>
</affiliation>
<affiliation></affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Formal Methods in System Design</title>
<title level="j" type="sub">An International Journal</title>
<title level="j" type="abbrev">Form Methods Syst Des</title>
<idno type="ISSN">0925-9856</idno>
<idno type="eISSN">1572-8102</idno>
<imprint><publisher>Springer US; http://www.springer-ny.com</publisher>
<pubPlace>Boston</pubPlace>
<date type="published" when="2008-02-01">2008-02-01</date>
<biblScope unit="volume">32</biblScope>
<biblScope unit="issue">1</biblScope>
<biblScope unit="page" from="57">57</biblScope>
<biblScope unit="page" to="83">83</biblScope>
</imprint>
<idno type="ISSN">0925-9856</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0925-9856</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Hybrid systems</term>
<term>Predicate abstraction</term>
<term>Qualitative simulation</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.</div>
</front>
</TEI>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004E51 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 004E51 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Merge |type= RBID |clé= ISTEX:8213F313ABB512ED9F185E98E24159FB0521BEA4 |texte= Abstractions for hybrid systems }}
This area was generated with Dilib version V0.6.33. |