Show simple item record

dc.contributor.authorCortadella, Jordi
dc.contributor.authorKishinevsky, Michael
dc.contributor.authorLavagno, Luciano
dc.contributor.authorYakovlev, Alex
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.date.accessioned2018-12-13T14:18:53Z
dc.date.available2018-12-13T14:18:53Z
dc.date.issued1998-08
dc.identifier.citationCortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A. Deriving Petri nets from finite transition systems. "IEEE transactions on computers", Agost 1998, vol. 47, núm. 8, p. 859-882.
dc.identifier.issn0018-9340
dc.identifier.urihttp://hdl.handle.net/2117/125784
dc.description.abstractThis paper presents a novel method to derive a Petri net from any specification model that can be mapped into a state-based representation with arcs labeled with symbols from an alphabet of events (a Transition System, TS). The method is based on the theory of regions for Elementary Transition Systems (ETS). Previous work has shown that, for any ETS, there exists a Petri Net with minimum transition count (one transition for each label) with a reachability graph isomorphic to the original Transition System. Our method extends and implements that theory by using the following three mechanisms that provide a framework for synthesis of safe Petri nets from arbitrary TSs. First, the requirement of isomorphism is relaxed to bisimulation of TSs, thus extending the class of synthesizable TSs to a new class called Excitation-Closed Transition Systems (ECTS). Second, for the first time, we propose a method of PN synthesis for an arbitrary TS based on mapping a TS event into a set of transition labels in a PN. Third, the notion of irredundant region set is exploited, to minimize the number of places in the net without affecting its behavior. The synthesis method can derive different classes of place-irredundant Petri Nets (e.g., pure, free choice, unique choice) from the same TS, depending on the constraints imposed on the synthesis algorithm. This method has been implemented and applied in different frameworks. The results obtained from the experiments have demonstrated the wide applicability of the method.
dc.format.extent24 p.
dc.language.isoeng
dc.publisherInstitute of Electrical and Electronics Engineers (IEEE)
dc.subjectÀrees temàtiques de la UPC::Informàtica::Informàtica teòrica
dc.subject.lcshFormal methods (Computer science)
dc.subject.lcshPetri nets
dc.subject.otherTransition systems
dc.subject.otherConcurrent systems
dc.subject.otherAsynchronous systems
dc.subject.otherSynthesis
dc.titleDeriving Petri nets from finite transition systems
dc.typeArticle
dc.subject.lemacMètodes formals (Informàtica)
dc.subject.lemacPetri, Xarxes de
dc.contributor.groupUniversitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals
dc.identifier.doi10.1109/12.707587
dc.description.peerreviewedPeer Reviewed
dc.relation.publisherversionhttps://ieeexplore.ieee.org/document/707587
dc.rights.accessOpen Access
local.identifier.drac1636453
dc.description.versionPostprint (published version)
local.citation.authorCortadella, J.; Kishinevsky, M.; Lavagno, L.; Yakovlev, A.
local.citation.publicationNameIEEE transactions on computers
local.citation.volume47
local.citation.number8
local.citation.startingPage859
local.citation.endingPage882


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record