On the symmetry reduction method for Petri nets and similar formalisms

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorJunttila, Tommi
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-10T08:58:40Z
dc.date.available2012-02-10T08:58:40Z
dc.date.issued2003-10-31
dc.description.abstractThe symmetry reduction method is a technique for alleviating the combinatorial explosion problem arising in the state space analysis of concurrent systems. This thesis studies various issues involved in the method. The focus is on systems modeled with Petri nets and similar formalisms, such as the Murφ description language. For place/transition nets, the computational complexity of the sub-tasks involved in the method is established. The problems of finding the symmetries of a net, comparing whether two markings are equivalent under the symmetries, producing canonical representatives for markings, and deciding whether a marking symmetrically covers another are classified to well-known complexity classes. New algorithms for the central task of producing canonical representatives for markings are presented. The algorithms apply and combine techniques from computational group theory and from the algorithms for the graph isomorphism problem. The experimental results show that the new algorithms are competitive against the previous ones described in the literature. Data symmetries, i. e., state space symmetries produced by symmetric use of data values, of a class high-level Petri nets, algebraic system nets, are also studied. It is defined how the permutations of the data values produce corresponding permutations in the state space of the net. In addition, sufficient conditions for the annotations in the net are defined in order to ensure that the produced permutations are indeed symmetries. Because these conditions turn out to be computationally difficult to verify, an approximation rule is additionally given. The practical use of the developed theory is illustrated by defining a class of high-level Petri nets allowing the use of common data types such as lists, sets, and arrays. The data symmetries of such nets are produced in a way similar to well-formed nets and the Murφ system, i. e., by declaring some primitive data types to be permutable and restricting the set of applicable operations on such types. New algorithms for checking whether two states are equivalent and for producing representatives for states under data symmetries are also described. The proposed algorithms either directly use the existing algorithms for the graph isomorphism problem, or use a partition refinement process modified from such algorithms. The algorithms are not limited to high-level Petri nets but are also applicable to the Murφ description language. The experimental results show that the new algorithms are competitive against the previous ones implemented in the Murφ tool.en
dc.description.versionrevieweden
dc.format.extent155
dc.format.mimetypeapplication/pdf
dc.identifier.isbn951-22-6745-4
dc.identifier.issn1457-7615
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/2116
dc.identifier.urnurn:nbn:fi:tkk-000843
dc.language.isoenen
dc.publisherHelsinki University of Technologyen
dc.publisherTeknillinen korkeakoulufi
dc.relation.ispartofseriesResearch reports / Helsinki University of Technology, Laboratory for Theoretical Computer Science. Aen
dc.relation.ispartofseries80en
dc.subject.keywordstate space analysisen
dc.subject.keywordsymmetryen
dc.subject.keywordPetri netsen
dc.subject.keywordplace/transition netsen
dc.subject.keywordalgebraic system netsen
dc.subject.keywordthe Murφ systemen
dc.subject.otherComputer scienceen
dc.titleOn the symmetry reduction method for Petri nets and similar formalismsen
dc.typeG4 Monografiaväitöskirjafi
dc.type.dcmitypetexten
dc.type.ontasotVäitöskirja (monografia)fi
dc.type.ontasotDoctoral dissertation (monograph)en
local.aalto.digiauthask
local.aalto.digifolderAalto_63447
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
isbn9512267454.pdf
Size:
1.25 MB
Format:
Adobe Portable Document Format