Combining symbolic and partial order methods for model checking 1-safe Petri nets

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Heljanko, Keijo
dc.date.accessioned 2012-02-10T09:16:17Z
dc.date.available 2012-02-10T09:16:17Z
dc.date.issued 2002-03-22
dc.identifier.isbn 951-22-5893-5
dc.identifier.issn 1457-7615
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/2166
dc.description.abstract In this work, methods are presented for model checking finite state asynchronous systems, more specifically 1-safe Petri nets, with the aim of alleviating the state explosion problem. Symbolic model checking techniques are used, combined with two partial order semantics known as net unfoldings and processes. We start with net unfoldings and study deadlock and reachability checking problems, using complete finite prefixes of net unfoldings introduced by McMillan. It is shown how these problems can be translated compactly into the problem of finding a stable model of a logic program. This combined with an efficient procedure for finding stable models of a logic program, the Smodels system, provides the basis of a prefix based model checking procedure for deadlock and reachability properties, which is competitive with previously published procedures using prefixes. This work shows that, if the only thing one can assume from a prefix is that it is complete, nested reachability properties are relatively hard. Namely, for several widely used temporal logics which can express a violation of a certain fixed safety property, model checking is PSPACE-complete in the size of the complete finite prefix. A model checking approach is devised for the linear temporal logic LTL-X using complete finite prefixes. The approach makes the complete finite prefix generation formula specific, and the prefix completeness notion application specific. Using these ideas, an LTL-X model checker has been implemented as a variant of a prefix generation algorithm. The use of bounded model checking for asynchronous systems is studied. A method to express the process semantics of a 1-safe Petri net in symbolic form as a set of satisfying truth assignments of a constrained Boolean circuit is presented. In the experiments the BCSat system is used as a circuit satisfiability checker. Another contribution employs logic programs with stable model semantics to develop a new linear size bounded LTL-X model checking translation that can be used with step semantics of 1-safe Petri nets. en
dc.format.extent 55, [97]
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 71 en
dc.relation.haspart K. Heljanko: Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets, Fundamenta Informaticae 37(3):247-268, 1999. [article1.pdf] © 1999 IOS Press. By permission.
dc.relation.haspart K. Heljanko: Model checking with finite complete prefixes is PSPACE-complete, in Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'2000), State College, Pennsylvania, USA, August 2000, volume 1877 of Lecture Notes in Computer Science, pages 108-122. [article2.pdf] © 2000 Springer-Verlag. By permission.
dc.relation.haspart J. Esparza, K. Heljanko: A new unfolding approach to LTL model checking, in Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), Geneva, Switzerland, July 2000, volume 1853 of Lecture Notes in Computer Science, pages 475-486. [article3.pdf] © 2000 Springer-Verlag. By permission.
dc.relation.haspart J. Esparza, K. Heljanko: Implementing LTL model checking with net unfoldings, in Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), Toronto, Canada, May 2001, volume 2057 of Lecture Notes in Computer Science, pages 37-56. [article4.pdf] © 2001 Springer-Verlag. By permission.
dc.relation.haspart K. Heljanko: Bounded reachability checking with process semantics, in Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'2001), Aalborg, Denmark, August 2001, volume 2154 of Lecture Notes in Computer Science, pages 218-232. [article5.pdf] © 2001 Springer-Verlag. By permission.
dc.relation.haspart K. Heljanko, I. Niemelä: Bounded LTL model checking with stable models, in Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'2001), Vienna, Austria, September 2001, volume 2173 of Lecture Notes in Artificial Intelligence, pages 200-212. [article6.pdf] © 2001 Springer-Verlag. By permission.
dc.subject.other Computer science en
dc.title Combining symbolic and partial order methods for model checking 1-safe Petri nets 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 Petri nets en
dc.subject.keyword complete finite prefixes en
dc.subject.keyword partial order methods en
dc.subject.keyword symbolic methods en
dc.subject.keyword bounded model checking en
dc.identifier.urn urn:nbn:fi:tkk-001362
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


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse

My Account