A Decidability Result for the Model Checking of Infinite-State Systems
Identifieur interne : 003142 ( Main/Exploration ); précédent : 003141; suivant : 003143A Decidability Result for the Model Checking of Infinite-State Systems
Auteurs : Daniele Zucchelli [Italie] ; Enrica Nicolini [France]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2012-01-01.
English descriptors
Abstract
Abstract: We present a decidability result for the model checking of a certain class of properties that can be conveniently expressed as ground formulae of a first-order temporal fragment. The decidability result is obtained by importing into the context of model-checking problems some techniques developed for the combination of decision procedures for the satisfiability of constraints. The general decidability result is then specialized for checking properties of particular interest, such as liveness and safety, and, for the latter case, a more optimized algorithm has been proposed.
Url:
DOI: 10.1007/s10817-010-9192-z
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003C20
- to stream Istex, to step Curation: 003B76
- to stream Istex, to step Checkpoint: 000904
- to stream Hal, to step Corpus: 000153
- to stream Hal, to step Curation: 000153
- to stream Hal, to step Checkpoint: 002903
- to stream Main, to step Merge: 003199
- to stream Main, to step Curation: 003142
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Decidability Result for the Model Checking of Infinite-State Systems</title><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FAECE290D78902F38DCD8A6E195DD7EAA3E9ADA6</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/s10817-010-9192-z</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-ZG4L1XT1-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C20</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C20</idno><idno type="wicri:Area/Istex/Curation">003B76</idno><idno type="wicri:Area/Istex/Checkpoint">000904</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000904</idno><idno type="wicri:doubleKey">0168-7433:2010:Zucchelli D:a:decidability:result</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00576873</idno><idno type="url">https://hal.inria.fr/inria-00576873</idno><idno type="wicri:Area/Hal/Corpus">000153</idno><idno type="wicri:Area/Hal/Curation">000153</idno><idno type="wicri:Area/Hal/Checkpoint">002903</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002903</idno><idno type="wicri:doubleKey">0168-7433:2010:Zucchelli D:a:decidability:result</idno><idno type="wicri:Area/Main/Merge">003199</idno><idno type="wicri:Area/Main/Curation">003142</idno><idno type="wicri:Area/Main/Exploration">003142</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Decidability Result for the Model Checking of Infinite-State Systems</title><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Via Comelico 39/41, 20135, Milano</wicri:regionArea><wicri:noRegion>Milano</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA Nancy-Grand Est, 615, rue du Jardin Botanique, 54602, Villers-les-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-les-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2012-01-01">2012-01-01</date><biblScope unit="volume">48</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="42">42</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Combination methods</term><term>Infinite-state systems</term><term>Model checking</term><term>Satisfiability problems</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present a decidability result for the model checking of a certain class of properties that can be conveniently expressed as ground formulae of a first-order temporal fragment. The decidability result is obtained by importing into the context of model-checking problems some techniques developed for the combination of decision procedures for the satisfiability of constraints. The general decidability result is then specialized for checking properties of particular interest, such as liveness and safety, and, for the latter case, a more optimized algorithm has been proposed.</div></front></TEI><affiliations><list><country><li>France</li><li>Italie</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Villers-les-Nancy</li></settlement></list><tree><country name="Italie"><noRegion><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></noRegion><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></country><country name="France"><region name="Grand Est"><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name></region><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003142 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003142 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FAECE290D78902F38DCD8A6E195DD7EAA3E9ADA6
|texte= A Decidability Result for the Model Checking of Infinite-State Systems
}}
| This area was generated with Dilib version V0.6.33. |  |