Improving symbolic model checking by rewriting temporal logic formulae
Identifieur interne : 000803 ( PascalFrancis/Checkpoint ); précédent : 000802; suivant : 000804Improving symbolic model checking by rewriting temporal logic formulae
Auteurs : David Deharbe [Brésil] ; Anamaria Martins Moreira [Brésil] ; Christophe Ringeissen [France]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2002.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
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.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:03-0333782Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Improving symbolic model checking by rewriting temporal logic formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Deharbe">David Deharbe</name><affiliation wicri:level="2"><inist:fA14 i1="01"><s1>Universidade Federal do Rio Grande do Norte - UFRN</s1><s2>Natal, RN</s2><s3>BRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Brésil</country><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation></author><author><name sortKey="Martins Moreira, Anamaria" sort="Martins Moreira, Anamaria" uniqKey="Martins Moreira A" first="Anamaria" last="Martins Moreira">Anamaria Martins Moreira</name><affiliation wicri:level="2"><inist:fA14 i1="01"><s1>Universidade Federal do Rio Grande do Norte - UFRN</s1><s2>Natal, RN</s2><s3>BRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Brésil</country><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA-INRIA</s1><s2>Nancy</s2><s3>FRA</s3><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">03-0333782</idno><date when="2002">2002</date><idno type="stanalyst">PASCAL 03-0333782 INIST</idno><idno type="RBID">Pascal:03-0333782</idno><idno type="wicri:Area/PascalFrancis/Corpus">000785</idno><idno type="wicri:Area/PascalFrancis/Curation">000258</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000803</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000803</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Improving symbolic model checking by rewriting temporal logic formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Deharbe">David Deharbe</name><affiliation wicri:level="2"><inist:fA14 i1="01"><s1>Universidade Federal do Rio Grande do Norte - UFRN</s1><s2>Natal, RN</s2><s3>BRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Brésil</country><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation></author><author><name sortKey="Martins Moreira, Anamaria" sort="Martins Moreira, Anamaria" uniqKey="Martins Moreira A" first="Anamaria" last="Martins Moreira">Anamaria Martins Moreira</name><affiliation wicri:level="2"><inist:fA14 i1="01"><s1>Universidade Federal do Rio Grande do Norte - UFRN</s1><s2>Natal, RN</s2><s3>BRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Brésil</country><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>LORIA-INRIA</s1><s2>Nancy</s2><s3>FRA</s3><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2002">2002</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm complexity</term><term>Formal verification</term><term>Logic model</term><term>Model checking</term><term>Program verification</term><term>Rewriting systems</term><term>Temporal logic</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Complexité algorithme</term><term>Vérification programme</term><term>Logique temporelle</term><term>Système réécriture</term><term>Modèle logique</term><term>Vérification formelle</term><term>Logique arbre calcul point fixe</term><term>Vérification énumérative</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0></fA01><fA08 i1="01" i2="1" l="ENG"><s1>Improving symbolic model checking by rewriting temporal logic formulae</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>RTA 2002 : rewriting techniques and applications : Copenhagen, 22-24 July 2002</s1></fA09><fA11 i1="01" i2="1"><s1>DEHARBE (David)</s1></fA11><fA11 i1="02" i2="1"><s1>MARTINS MOREIRA (Anamaria)</s1></fA11><fA11 i1="03" i2="1"><s1>RINGEISSEN (Christophe)</s1></fA11><fA12 i1="01" i2="1"><s1>TISON (Sophie)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>Universidade Federal do Rio Grande do Norte - UFRN</s1><s2>Natal, RN</s2><s3>BRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></fA14><fA14 i1="02"><s1>LORIA-INRIA</s1><s2>Nancy</s2><s3>FRA</s3><sZ>3 aut.</sZ></fA14><fA20><s1>207-221</s1></fA20><fA21><s1>2002</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA26 i1="01"><s0>3-540-43916-1</s0></fA26><fA43 i1="01"><s1>INIST</s1><s2>16343</s2><s5>354000108481420150</s5></fA43><fA44><s0>0000</s0><s1>© 2003 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>18 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>03-0333782</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0></fA64><fA66 i1="01"><s0>DEU</s0></fA66><fC01 i1="01" l="ENG"><s0>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.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A05</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Complexité algorithme</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Algorithm complexity</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Complejidad algoritmo</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Vérification programme</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Program verification</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Verificación programa</s0><s5>02</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Logique temporelle</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Temporal logic</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Lógica temporal</s0><s5>03</s5></fC03><fC03 i1="04" i2="3" l="FRE"><s0>Système réécriture</s0><s5>04</s5></fC03><fC03 i1="04" i2="3" l="ENG"><s0>Rewriting systems</s0><s5>04</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Modèle logique</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Logic model</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Modelo lógico</s0><s5>05</s5></fC03><fC03 i1="06" i2="3" l="FRE"><s0>Vérification formelle</s0><s5>06</s5></fC03><fC03 i1="06" i2="3" l="ENG"><s0>Formal verification</s0><s5>06</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Logique arbre calcul point fixe</s0><s4>INC</s4><s5>82</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Vérification énumérative</s0><s4>CD</s4><s5>96</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>Model checking</s0><s4>CD</s4><s5>96</s5></fC03><fN21><s1>230</s1></fN21><fN82><s1>PSI</s1></fN82></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on rewriting techniques and applications</s1><s3>Copenhagen DNK</s3><s4>2002-07-22</s4></fA30></pR></standard></inist><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="Deharbe">David Deharbe</name></region><name sortKey="Martins Moreira, Anamaria" sort="Martins Moreira, Anamaria" uniqKey="Martins Moreira A" first="Anamaria" last="Martins 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></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000803 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000803 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:03-0333782
|texte= Improving symbolic model checking by rewriting temporal logic formulae
}}
| This area was generated with Dilib version V0.6.33. |  |