×

zbMATH — the first resource for mathematics

Non-interleaving bisimulation equivalences on basic parallel processes. (English) Zbl 1185.68444
Summary: We show polynomial time algorithms for deciding hereditary history preserving bisimilarity (in \(O(n^{3} \log n))\) and history preserving bisimilarity (in \(O(n^{6}))\) on the class Basic Parallel Processes. The latter algorithm also decides a number of other non-interleaving behavioural equivalences (e.g., distributed bisimilarity) which are known to coincide with history preserving bisimilarity on this class. The common general scheme of both algorithms is based on a fixpoint characterization of the equivalences for tree-like labelled event structures. The technique for realizing the greatest fixpoint computation in the case of hereditary history preserving bisimilarity is based on the revealed tight relationship between equivalent tree-like labelled event structures. In the case of history preserving bisimilarity, a technique of deciding classical bisimilarity on acyclic Petri nets is used.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008
[2] S. Christensen, Decidability and decomposition in process algebras, Ph.D. thesis, Department of Computer Science, University of Edinburgh, UK, 1993.
[3] Mayr, R., Process rewrite systems, Information and computation, 156, 1-2, 264-286, (2000) · Zbl 1046.68566
[4] Srba, J., Roadmap of infinite results, Formal models and semantics, vol. 2, (2004), World Scientific Publishing Co. · Zbl 1065.68073
[5] R.v. Glabbeek, U. Goltz, Equivalence notions for concurrent systems and refinement of actions, in: Proc. MFCS’89, LNCS, vol. 379, 1989, pp. 237-248. · Zbl 0755.68095
[6] Aceto, L., Relating distributed, temporal and causal observations of simple processes, Fundamenta informaticae, 17, 4, 369-397, (1992) · Zbl 0847.68032
[7] I. Castellani, Bisimulations for concurrency, Ph.D. thesis, University of Edinburgh, 1988.
[8] P. Darondeau, P. Degano, Causal trees, in: Proc. ICALP’89, LNCS, vol. 372, 1989, pp. 234-248.
[9] A. Kiehn, A note on distributed bisimulations, unpublished draft, 1999.
[10] I. Castellani, Process algebras with localities, in: Handbook of Process Algebra, Chapter 15, Elsevier, 2001, pp. 945-1046.
[11] Aceto, L.; preserving, History, Causal and mixed-ordering equivalence over stable event structures, Fundamenta informaticae, 17, 319-331, (1992) · Zbl 0767.68074
[12] S. Fröschle, Decidability of plain and hereditary history-preserving bisimulation for BPP, in: Proc. EXPRESS’99, ENTCS, vol. 27, 1999.
[13] Lasota, S., Decidability of performance equivalence for basic parallel processes, Theoretical computer science, 360, 172-192, (2006) · Zbl 1099.68070
[14] Gorrieri, R.; Roccetti, M.; Stancampiano, E., A theory of processes with durational actions, Theoretical computer science, 140, 1, 73-94, (1995) · Zbl 0874.68113
[15] Joyal, A.; Nielsen, M.; Winskel, G., Bisimulation from open maps, Information and computation, 127, 164-185, (1996) · Zbl 0856.68067
[16] S. Fröschle, T. Hildebrandt, On plain and hereditary history-preserving bisimulation, in: MFCS’99, LNCS, vol. 1672, Springer-Verlag, 1999, pp. 354-365. · Zbl 0959.68087
[17] Jurdziński, M.; Nielsen, M.; Srba, J., Undecidability of domino games and hhp-bisimilarity, Information and computation, 184, 343-368, (2003) · Zbl 1054.68094
[18] Fröschle, S., The decidability border of hereditary history preserving bisimilarity, Information processing letters, 93, 6, 289-293, (2005) · Zbl 1173.68538
[19] J. Srba, Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard, in: Proc. STACS’02, LNCS, vol. 2285, 2002. · Zbl 1054.68096
[20] P. Jančar, Bisimilarity of basic parallel processes is PSPACE-complete, in: Proc. LICS’03, IEEE Computer Society, 2003, pp. 218-227.
[21] Jategaonkar, L.; Meyer, A.R., Deciding true concurrency equivalences on safe, finite nets, Theoretical computer science, 154, 107-143, (1996) · Zbl 0877.68056
[22] J. Esparza, A. Kiehn, On the model checking problem for branching time logics and basic parallel processes, in: CAV’95, LNCS, vol. 939, Springer-Verlag, 1995, pp. 353-366.
[23] K. Sunesen, M. Nielsen, Behavioural equivalence for infinite systems—partially decidable!, in: ICATPN’96, LNCS, vol. 1091, Springer-Verlag, 1996, pp. 460-479.
[24] P. Jančar, Z. Sawa, On distributed bisimilarity over basic parallel processes, in: Proc. AVIS’05, 2005.
[25] S. Fröschle, S. Lasota, Decomposition and complexity of hereditary history preserving bisimulation on BPP, in: Proc. CONCUR’05, LNCS, vol. 3653, Springer-Verlag, 2005, pp. 263-277. · Zbl 1134.68434
[26] S. Fröschle, Composition and decomposition in true-concurrency, in: V. Sassone (Ed.), Proc. FOSSACS’05, LNCS, vol. 3441, Springer, 2005, pp. 333-347.
[27] S. Fröschle, Decidability and coincidence of equivalences for concurrency, Ph.D. thesis, University of Edinburgh, 2004.
[28] Hirshfeld, Y.; Jerrum, M.; Moller, F., A polynomial time algorithm for deciding bisimulation equivalence of normed basic parallel processes, Mathematical structures in computer science, 6, 251-259, (1996) · Zbl 0857.68042
[29] S. Lasota, A polynomial-time algorithm for deciding true concurrency equivalences of basic parallel processes, in: Proc. MFCS’03, LNCS, vol. 2747, Springer-Verlag, 2003, pp. 521-530. · Zbl 1124.68392
[30] S. Fröschle, S. Lasota, Normed processes, unique decomposition, and complexity of bisimulation equivalences, in: Proc. Infinity’06, ENTCS, vol. 239, Elsevier, 2009, pp. 17-42. · Zbl 1347.68264
[31] P. Jančar, M. Kot, Bisimilarity on normed Basic Parallel Processes can be decided in time \(O(n^3)\), in: R. Bharadwaj (Ed.), Proc. Third International Workshop on Automated Verification of Infinite-State Systems - AVIS 2004, 2004.
[32] D. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), Theoretical Computer Science: 5th GI-Conference, Karlsruhe, LNCS, vol. 104, Springer-Verlag, 1981, pp. 167-183.
[33] C. Stirling, Bisimulation, model checking and other games, notes for Mathfit Workshop on Finite Model Theory, University of Wales, Swansea (July 1996). Available from: <http://www.dcs.ed.ac.uk/home/cps/mfit.ps/>.
[34] M. Bednarczyk, Hereditary history preserving bisimulation or what is the power of the future perfect in program logics, Technical Report, Polish Academy of Sciences, Gdańsk, 1991.
[35] Aho, A.; Hopcroft, J.; Ullman, J., The design and analysis of computer algorithms, (1974), Addison-Wesley Publishing Co.
[36] Esparza, J., Petri nets, commutative context-free grammars, and basic parallel processes, Fundamenta informatica, 31, 1, 13-25, (1997) · Zbl 0882.68101
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.