Learning Centre

Automata-theoretic and bounded model checking for linear temporal logic

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Latvala, Timo
dc.date.accessioned 2012-02-17T07:10:58Z
dc.date.available 2012-02-17T07:10:58Z
dc.date.issued 2005-08-12
dc.identifier.isbn 951-22-7788-3
dc.identifier.issn 1457-7615
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/2600
dc.description.abstract In this work we study methods for model checking the temporal logic LTL. The focus is on the automata-theoretic approach to model checking and bounded model checking. We begin by examining automata-theoretic methods to model check LTL safety properties. The model checking problem can be reduced to checking whether the language of a finite state automaton on finite words is empty. We describe an efficient algorithm for generating small finite state automata for so called non-pathological safety properties. The presented implementation is the first tool able to decide whether a formula is non-pathological. The experimental results show that treating safety properties can benefit model checking at very little cost. In addition, we find supporting evidence for the view that minimising the automaton representing the property does not always lead to a small product state space. A deterministic property automaton can result in a smaller product state space even though it might have a larger number states. Next we investigate modular analysis. Modular analysis is a state space reduction method for modular Petri nets. The method can be used to construct a reduced state space called the synchronisation graph. We devise an on-the-fly automata-theoretic method for model checking the behaviour of a modular Petri net from the synchronisation graph. The solution is based on reducing the model checking problem to an instance of verification with testers. We analyse the tester verification problem and present an efficient on-the-fly algorithm, the first complete solution to tester verification problem, based on generalised nested depth-first search. We have also studied propositional encodings for bounded model checking LTL. A new simple linear sized encoding is developed and experimentally evaluated. The implementation in the NuSMV2 model checker is competitive with previously presented encodings. We show how to generalise the LTL encoding to a more succint logic: LTL with past operators. The generalised encoding compares favourably with previous encodings for LTL with past operators. Links between bounded model checking and the automata-theoretic approach are also explored. en
dc.format.extent 54, [77]
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Helsinki University of Technology en
dc.publisher Teknillinen korkeakoulu fi
dc.relation.ispartofseries Research reports / Helsinki University of Technology, Laboratory for Theoretical Computer Science. A en
dc.relation.ispartofseries 95 en
dc.relation.haspart Timo Latvala. 2003. Efficient model checking of safety properties. In: T. Ball and S. Rajamani, editors, Model Checking Software. 10th International SPIN Workshop, Portland, Oregon, USA. Lecture Notes in Computer Science, volume 2648, pp. 74-88. [article1.pdf] © 2003 Springer-Verlag. By permission.
dc.relation.haspart Timo Latvala and Marko Mäkelä. 2004. LTL model checking for modular Petri nets. In: J. Cortadella and W. Reisig, editors, Applications and Theory of Petri Nets 2004. 25th International Conference, ICATPN 2004, Bologna, Italy. Lecture Notes in Computer Science, volume 3099, pp. 298-311. [article2.pdf] © 2004 Springer-Verlag. By permission.
dc.relation.haspart Timo Latvala and Heikki Tauriainen. 2004. Improved on-the-fly verification with testers. Nordic Journal of Computing, 11 (2): 148-164. [article3.pdf] © 2004 Publishing Association Nordic Journal of Computing. By permission.
dc.relation.haspart Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. 2004. Simple bounded LTL model checking. In: A. Hu and A. Martin, editors, Formal Methods in Computer-Aided Design 2004. 5th International Conference, FMCAD 2004, Austin, Texas, USA. Lecture Notes in Computer Science, volume 3312, pp. 186-200. [article4.pdf] © 2004 Springer-Verlag. By permission.
dc.relation.haspart Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. 2005. Simple is better: efficient bounded model checking for past LTL. In: R. Cousot, editor, Verification, Model Checking, and Abstract Interpretation 2005. 6th International Conference, VMCAI 2005, Paris, France. Lecture Notes in Computer Science, volume 3385, pp. 380-395. [article5.pdf] © 2005 Springer-Verlag. By permission.
dc.subject.other Computer science en
dc.subject.other Mathematics en
dc.title Automata-theoretic and bounded model checking for linear temporal logic en
dc.type G5 Artikkeliväitöskirja fi
dc.description.version reviewed en
dc.contributor.department Department of Computer Science and Engineering en
dc.contributor.department Tietotekniikan osasto fi
dc.subject.keyword verification en
dc.subject.keyword model checking en
dc.subject.keyword LTL en
dc.subject.keyword automata en
dc.subject.keyword safety properties en
dc.subject.keyword Petri nets en
dc.subject.keyword modular analysis en
dc.subject.keyword LTS en
dc.subject.keyword testers en
dc.subject.keyword bounded model checking en
dc.subject.keyword PLTL en
dc.identifier.urn urn:nbn:fi:tkk-005603
dc.type.dcmitype text en
dc.type.ontasot Väitöskirja (artikkeli) fi
dc.type.ontasot Doctoral dissertation (article-based) en
dc.contributor.lab Laboratory for Theoretical Computer Science en
dc.contributor.lab Tietojenkäsittelyteorian laboratorio fi
local.aalto.digifolder Aalto_64110
local.aalto.digiauth ask

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication