The paper is devoted to the investigation of behavioral equivalences of concurrent systems modeled by Petri nets with silent transitions. Basic τ-equivalences and back-forth τ-bisimulation equivalences known from the literature are supplemented by new ones, giving rise to complete set of equivalence notions in interleaving / true concurrency and linear / branching time semantcis. Their interrelations are examined for the general class of nets as well as for their subclasses of nets without siltent transitions and sequential nets (nets without concurrent transitions). In addition, the preservation of all the equivalence notions by refinements (allowing one to consider the systems to be modeled on a lower abstraction levels) is investigated.
Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa.de:bsz:14-qucosa-100370 |
Date | 27 November 2012 |
Creators | Tarasyuk, Igor V. |
Contributors | Russian Academy of Sciences, A.P. Ershov Institute of Informatics Systems, Technische Universität Dresden, Fakultät Informatik |
Publisher | Saechsische Landesbibliothek- Staats- und Universitaetsbibliothek Dresden |
Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
Language | English |
Detected Language | English |
Type | doc-type:workingPaper |
Format | application/pdf, application/postscript, application/zip |
Relation | dcterms:isPartOf:Technische Berichte / Technische Universität Dresden, Fakultät Informatik ; 2000,11 (TUD-FI00-11 November 2000) |
Page generated in 0.0157 seconds