Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
Identifieur interne : 001C32 ( Istex/Checkpoint ); précédent : 001C31; suivant : 001C33Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
Auteurs : David Déharbe [Brésil] ; Anamaria Martins Moreira [Brésil] ; Christophe Ringeissen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NF-CTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NF-CTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.
Url:
DOI: 10.1007/3-540-45610-4_15
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:395EAC54F49E719F8819BA68AAF9829935FAE91CLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name></author><author><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:395EAC54F49E719F8819BA68AAF9829935FAE91C</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45610-4_15</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-1QL06KCC-3/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000D59</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000D59</idno><idno type="wicri:Area/Istex/Curation">000D50</idno><idno type="wicri:Area/Istex/Checkpoint">001C32</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C32</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name><affiliation wicri:level="2"><country xml:lang="fr">Brésil</country><wicri:regionArea>Universidade Federal do Rio Grande do Norte — UFRN, Natal, RN</wicri:regionArea><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name><affiliation wicri:level="2"><country xml:lang="fr">Brésil</country><wicri:regionArea>Universidade Federal do Rio Grande do Norte — UFRN, Natal, RN</wicri:regionArea><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NF-CTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NF-CTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.</div></front></TEI><affiliations><list><country><li>Brésil</li><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Rio Grande do Norte</li></region><settlement><li>Nancy</li></settlement></list><tree><country name="Brésil"><region name="Rio Grande do Norte"><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name></region><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name></country><country name="France"><region name="Grand Est"><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></region><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001C32 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001C32 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:395EAC54F49E719F8819BA68AAF9829935FAE91C
|texte= Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
}}
| This area was generated with Dilib version V0.6.33. |  |