Abstract
In this paper we propose a new approach to check history-preserving equivalence for Petri nets. Exploiting this approach, history-preserving bisimulation is proved decidable for the class of finite nets which are n-safe for some n (the approaches of [17] and of [8] work just for 1-safe nets). Moreover, since we map nets on ordinary transition systems, standard results and algorithms can be re-used, yielding for instance the possibility of deriving minimal realizations. The proposed approach can be applied also to other concurrent formalisms based on partial order semantics, like CCS with causality [4].
Research supported in part by CNR Integrated Project Metodi e Strumenti per la Progettazione e la Verifica di Sistemi Eterogenei Connessi mediante Reti di Comunicazione and Esprit Working Group CONFER2.
Preview
Unable to display preview. Download preview PDF.
References
E. Best, R. Devillers, A. Kiehn and L. Pomello. Fully concurrent bisimulation. Acta Informatica 28:231–264, 1991.
A. Bouali, S. Gnesi and S. Larosa. The integration project for the JACK environment. In EATCS Bullettin, 1994.
G. Boudol, I. Castellani, M. Hennessy and A. Kiehn. Observing localities. Theoretical Computer Science 114:31–61, 1993.
Ph. Darondeau and P. Degano. Causal trees. In Proc. ICALP'89, LNCS 372. Springer-Verlag, 1989.
P. Degano, R. De Nicola and U. Montanari. Observational equivalences for concurrency models. In Proc. Formal Description of Programming Concepts — III, 1986. North-Holland, 1987.
P. Degano, R. De Nicola and U. Montanari. Partial orderings descriptions and observations of nondeterministic concurrent processes. In Proc. REX School/Workshop on Linear Time, Branching Time and Partial Orders in Logica and Models for Concurrency, LNCS 354. Springer Verlag, 1989.
U. Goltz and W. Reisig. The non-sequential behaviour of Petri nets. Information and Control 57:125–147, 1983.
L. Jategaonkar and A. Meyer. Deciding true concurrency equivalences on finite safe nets. Theoretical Computer Science 154:107–143, 1996. Extended abstract in Proc. ICALP'93, LNCS 700. Springer Verlag, 1993.
B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of nonfinite-state programs. Information and Computation 107:272–302, 1993.
P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86:43–68, 1990.
U. Montanari and M. Pistore. Checking bisimilarity for finitary π-calculus. In Proc. CONCUR'95, LNCS 962. Springer Verlag, 1995.
U. Montanari and M. Pistore. History-dependent automata. Draft. Available as ftp://ftp.di.unipi.it/pub/Papers/pistore/HDautomata.ps.gz. Also: Technical Report, Università di Pisa, to appear.
U. Montanari, M. Pistore and D. Yankelevich. Efficient minimization up to location equivalence. In Proc. ESOP'96, LNCS 1058. Springer Verlag, 1996.
R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.
A. Rabinovich and B. A. Trakhtenbrot. Behaviour structures and nets. Fundamenta Informaticae 11:357–404, 1988.
R. Valk and M. Jantzen. The residue vector sets with applications to decidability problems in Petri nets. In Proc. APN'84, LNCS 188. Springer Verlag, 1984.
W. Vogler. Deciding history preserving bisimilarity. In Proc. ICALP'91, LNCS 510. Springer Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Montanari, U., Pistore, M. (1997). Minimal transition systems for history-preserving bisimulation. In: Reischuk, R., Morvan, M. (eds) STACS 97. STACS 1997. Lecture Notes in Computer Science, vol 1200. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023477
Download citation
DOI: https://doi.org/10.1007/BFb0023477
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62616-9
Online ISBN: 978-3-540-68342-1
eBook Packages: Springer Book Archive