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

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorHeljanko, Keijo
dc.contributor.departmentDepartment of Computer Science and Engineeringen
dc.contributor.departmentTietotekniikan osastofi
dc.contributor.labLaboratory for Theoretical Computer Scienceen
dc.contributor.labTietojenkäsittelyteorian laboratoriofi
dc.date.accessioned2012-02-10T09:16:17Z
dc.date.available2012-02-10T09:16:17Z
dc.date.issued2002-03-22
dc.description.abstractIn 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.description.versionrevieweden
dc.format.extent55, [97]
dc.format.mimetypeapplication/pdf
dc.identifier.isbn951-22-5893-5
dc.identifier.issn1457-7615
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/2166
dc.identifier.urnurn:nbn:fi:tkk-001362
dc.language.isoenen
dc.publisherHelsinki University of Technologyen
dc.publisherTeknillinen korkeakoulufi
dc.relation.haspartK. 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.haspartK. 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.haspartJ. 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.haspartJ. 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.haspartK. 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.haspartK. 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.relation.ispartofseriesResearch reports / Helsinki University of Technology, Laboratory for Theoretical Computer Science. Aen
dc.relation.ispartofseries71en
dc.subject.keywordverificationen
dc.subject.keywordmodel checkingen
dc.subject.keywordPetri netsen
dc.subject.keywordcomplete finite prefixesen
dc.subject.keywordpartial order methodsen
dc.subject.keywordsymbolic methodsen
dc.subject.keywordbounded model checkingen
dc.subject.otherComputer scienceen
dc.titleCombining symbolic and partial order methods for model checking 1-safe Petri netsen
dc.typeG5 Artikkeliväitöskirjafi
dc.type.dcmitypetexten
dc.type.ontasotVäitöskirja (artikkeli)fi
dc.type.ontasotDoctoral dissertation (article-based)en
local.aalto.digiauthask
local.aalto.digifolderAalto_80335
Files
Original bundle
Now showing 1 - 7 of 7
No Thumbnail Available
Name:
isbn9512258935.pdf
Size:
578.06 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article1.pdf
Size:
313.99 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article2.pdf
Size:
266.68 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article3.pdf
Size:
212.63 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article4.pdf
Size:
285.71 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article5.pdf
Size:
262.3 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
article6.pdf
Size:
237.4 KB
Format:
Adobe Portable Document Format