Abstract
For finite-state systems non-interleaving equivalences are computationally at least as hard as interleaving equivalences. In this paper we show that when moving to infinite-state systems, this situation may change dramatically.
We compare standard language equivalence for process description languages with two generalizations based on traditional approaches capturing non-interleaving behaviour, pomsets representing global causal dependency, and locality representing spatial distribution of events.
We first study equivalences on Basic Parallel Processes, BPP, a process calculus equivalent to communication free Petri nets. For this simple process language our two notions of non-interleaving equivalences agree. More interestingly, we show that they are decidable, contrasting a result of Hirshfeld that standard interleaving language equivalence is undecidable. Our result is inspired by a recent result of Esparza and Kiehn, showing the same phenomenon in the setting of model checking.
We follow up investigating to which extent the result extends to larger subsets of CCS and TCSP. We discover a significant difference between our non-interleaving equivalences. We show that for a certain non-trivial subclass of processes between BPP and TCSP, not only are the two equivalences different, but one (locality) is decidable whereas the other (pomsets) is not. The decidability result for locality is proved by a reduction to the reachability problem for Petri nets.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky, Eliminating Local Non-determinism: a New Semantics for CCS, Computer Systems Laboratory, Queen Mary College, Report no. 290 (1981).
L. Aceto, A Static View of Localities, Formal Aspects of Computing, 6 (2), 202–222 (1994).
G. Boudol, I. Castellani, M. Hennessy and A. Kiehn, Observing Localities, Theoretical Computer Science, 114, 31–61, 1993.
S. Christensen. Decidability and Decomposition in Process Algebras Ph.D. Thesis, University of Edinburgh, CST-105-93, 1993.
S. Christensen, H. Hüttel, Decidability Issues for Infinite-State Processes — a Survey, EATCS Bulletin 51, 156–166 (1993).
S. Christensen, Y. Hirshfeld and F. Moller, Bisimulation equivalence is decidable for basic parallel processes, CONCUR '93, Springer LNCS 715, 143–157 (1993).
J. Engelfriet, Tree automata and tree grammars, University of Aarhus, DAIMI FN-10 (1975).
J. Esparza, Petri nets, commutative context-free grammars, and Basic Parallel Processes, in Proceedings of Fundamentals of Computation Theory, (FCT'95), LNCS 965, Springer Verlag 1995.
J. Esparza and A. Kiehn, On the Model Checking Problem for Branching Logics and Basic Parallel Processes, CAV '95, Springer LNCS 939, 353–366 (1995).
Y. Hirshfeld, Petri Nets and the Equivalence Problem, CSL '93, Springer LNCS 882, 165–174 (1994).
C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, International Series in Computer Science (1985).
H. Hütte, Undecidable Equivalences for Basic Parallel Processes, TACS '94, Springer LNCS 789, 454–464 (1994).
P. Jancar and F. Moller, Checking Regular Properties of Petri Nets, CONCUR '95, Springer LNCS 962, 348–362 (1995).
L. Jategaonkar and A. Meyer, Deciding true concurrency equivalences on finite safe nets. ICALP '93, Springer LNCS 700, 519–531 (1993).
A. Kiehn and M. Hennessy, On the Decidability on Non-interleaving Equivalences, CONCUR '94, Springer LNCS 836, 18–33 (1994)
S.R. Kosaraju. Decidability of Reachability in Vector Addition Systems. 14th Annual ACM Symposium on Theory of Computing, San Francisco, 267–281 (1982).
E.W. Mayr, Persistence of Vector Replacement Systems is Decidable. Acta Informatica 15, 309–318 (1981).
E.W. Mayr and A.R. Meyer, The Complexity of the Finite Containment Problem for Petri Nets, Journal of the ACM, 28(3), 561–576 (1981).
A. Mazurkiewicz, Basic notions of trace theory, in de Bakker, de Roever and Rozenberg (eds.), Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency, Springer LNCS 354, 285–363 (1988).
A.R.G. Milner, Communication and concurrency, Prentice Hall (1989).
M.L. Minsky, Computation — Finite and Infinite Machines, Prentice Hall (1967).
M. Mukund and M. Nielsen, CCS, Locations and Asynchronous Transition Systems, FST & TCS '92, Springer LNCS 652, 328–341 (1992).
E.R. Olderog and C.A.R. Hoare, Specification-Oriented Semantics for Communicating Processes, Acta Informatica, 23, 9–66 (1986).
V.R. Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, 15(1), 33–71 (1986).
W. Reisig, A note on the representation of finite tree automata. Information Processing Letters, 8(5):239–240, June 1979
W. Reisig, Petri Nets — an Introduction, EATCS Monograph in Computer Science, Springer (1985).
K. Sunesen and M. Nielsen, Behavioural equivalence for infinite systems — partially decidable!, Technical Report RS-95-55, BRICS, Aarhus University (1995).
D. Taubner, Finite Representations of CCS and TCSP Programs by Automata and Petri Nets, Springer LNCS 369 (1989).
W. Thomas, Automata on Infinite Objects, in Handbook of Theoretical Computer Science, vol B, ed. J. van Leeuwen, Elsevier, 133–192 (1990).
R.J. van Glabbeek, Comparative concurrency semantics and refinement of actions, PhD thesis, CWI Amsterdam (1990).
R.J. van Glabbeek and U. Goltz, Equivalence Notions for Concurrent Systems and Refinement of Actions, MFCS '89, Springer LNCS 379, 237–248 (1989).
P. Wolper and P. Godefroid, Partial Order Methods for Temporal Verification, Concur '93, Springer LNCS 715, 233–246 (1993).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sunesen, K., Nielsen, M. (1996). Behavioural equivalence for infinite systems — Partially decidable!. In: Billington, J., Reisig, W. (eds) Application and Theory of Petri Nets 1996. ICATPN 1996. Lecture Notes in Computer Science, vol 1091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61363-3_25
Download citation
DOI: https://doi.org/10.1007/3-540-61363-3_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61363-3
Online ISBN: 978-3-540-68505-0
eBook Packages: Springer Book Archive