Skip to main content
SpringerLink
Log in
Book cover

Annual Symposium on Theoretical Aspects of Computer Science

STACS 1997: STACS 97 pp 413–425Cite as

Minimal transition systems for history-preserving bisimulation

  • Parallel and Distributed Systems II
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1200))

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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Best, R. Devillers, A. Kiehn and L. Pomello. Fully concurrent bisimulation. Acta Informatica 28:231–264, 1991.

    Article  Google Scholar 

  2. A. Bouali, S. Gnesi and S. Larosa. The integration project for the JACK environment. In EATCS Bullettin, 1994.

    Google Scholar 

  3. G. Boudol, I. Castellani, M. Hennessy and A. Kiehn. Observing localities. Theoretical Computer Science 114:31–61, 1993.

    Article  Google Scholar 

  4. Ph. Darondeau and P. Degano. Causal trees. In Proc. ICALP'89, LNCS 372. Springer-Verlag, 1989.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. U. Goltz and W. Reisig. The non-sequential behaviour of Petri nets. Information and Control 57:125–147, 1983.

    Article  Google Scholar 

  8. 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.

    Article  Google Scholar 

  9. B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of nonfinite-state programs. Information and Computation 107:272–302, 1993.

    Article  Google Scholar 

  10. P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86:43–68, 1990.

    Article  Google Scholar 

  11. U. Montanari and M. Pistore. Checking bisimilarity for finitary π-calculus. In Proc. CONCUR'95, LNCS 962. Springer Verlag, 1995.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. U. Montanari, M. Pistore and D. Yankelevich. Efficient minimization up to location equivalence. In Proc. ESOP'96, LNCS 1058. Springer Verlag, 1996.

    Google Scholar 

  14. R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.

    Article  Google Scholar 

  15. A. Rabinovich and B. A. Trakhtenbrot. Behaviour structures and nets. Fundamenta Informaticae 11:357–404, 1988.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. W. Vogler. Deciding history preserving bisimilarity. In Proc. ICALP'91, LNCS 510. Springer Verlag, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Pisa, Corso Italia 40, 56100, Pisa, Italy

    Ugo Montanari & Marco Pistore

Authors
  1. Ugo Montanari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco Pistore
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rüdiger Reischuk Michel Morvan

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation