Abstract
The idea of composition and decomposition to obtain computability results is particularly relevant for true-concurrency. In contrast to the interleaving world, where composition and decomposition must be considered with respect to a process algebra operator, e.g. parallel composition, we can directly recognize whether a truly-concurrent model such as a labelled asynchronous transition system or a 1-safe Petri net can be dissected into independent ‘chunks of behaviour’. In this paper we introduce the corresponding concept ‘decomposition into independent components’, and investigate how it translates into truly-concurrent bisimulation equivalences. We prove that, under a natural restriction, history preserving (hp), hereditary hp (hhp), and coherent hhp (chhp) bisimilarity are decomposable with respect to prime decompositions. Apart from giving a general proof technique our decomposition theory leads to several coincidence results. In particular, we resolve that hp, hhp, and chhp bisimilarity coincide for ‘normal form’ basic parallel processes.
Chapter PDF
References
Penczek, W., Kuiper, R.: Traces and logic. In: The Book of Traces, pp. 307–381. World Scientific, Singapore (1995)
Madhusudan, P., Thiagarajan, P.S.: Controllers for discrete event systems via morphisms. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 18–33. Springer, Heidelberg (1998)
Jurdziński, M., Nielsen, M., Srba, J.: Domino hereditary history preserving bisimilarity is undecidable. Inform. and Comput. 184, 343–368 (2003)
Vogler, W.: Deciding history preserving bisimilarity. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 495–505. Springer, Heidelberg (1991)
Jategaonkar, L., Meyer, A.R.: Deciding true concurrency equivalences on safe, finite nets. TCS 154, 107–143 (1996)
Montanari, U., Pistore, M.: Minimal transition systems for history-preserving bisimulation. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 413–425. Springer, Heidelberg (1997)
Esparza, J., Kiehn, A.: On the model checking problem for branching time logics and basic parallel processes. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 353–366. Springer, Heidelberg (1995)
Sunesen, K., Nielsen, M.: Behavioural equivalence for infinite systems—partially decidable? In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 460–479. Springer, Heidelberg (1996)
Jančar, P.: Strong bisimilarity on basic parallel processes is PSPACE-complete. In: LICS 2003. IEEE, Los Alamitos (2003)
Srba, J.: Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 535–546. Springer, Heidelberg (2002)
Lasota, S.: A polynomial-time algorithm for deciding true concurrency equivalences of basic parallel processes. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 521–530. Springer, Heidelberg (2003)
Fröschle, S.: Decidability of plain and hereditary history-preserving bisimulation for BPP. In: EXPRESS 1999. ENTCS, vol. 27 (1999)
Fröschle, S.: Decidability and Coincidence of Equivalences for Concurrency. PhD thesis, University of Edinburgh (2004)
Winskel, G., Nielsen, M.: Models for concurrency. In: Handbook of logic in computer science, vol. 4, pp. 1–148. Oxford Univ. Press, Oxford (1995)
Fröschle, S.: The decidability border of hereditary history preserving bisimilarity. Information Processing Letters (to appear)
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)
Jančar, P., Kot, M.: Bisimilarity on normed basic parallel processes can be decided in time o(n 3). In: AVIS 2004. ENTCS (2004)
Christensen, S., Hirshfeld, Y., Moller, F.: Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In: LICS 1993, pp. 386–396. IEEE, Los Alamitos (1993)
Milner, R., Moller, F.: Unique decomposition of processes. TCS 107, 357–363 (1993)
Fröschle, S.: Composition and decomposition in true-concurrency. Technical Report 276, Institute of Informatics, University of Warsaw (2004)
Fröschle, S., Hildebrandt, T.: On plain and hereditary history-preserving bisimulation. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 354–365. Springer, Heidelberg (1999)
Pin, J.E.: Syntactic semigroups. In: Handbook of formal languages, vol. 1, pp. 680–746. Springer, Heidelberg (1997)
Norman, C.W.: Undergraduate Algebra. Oxford Science Publications (1986)
Truss, J.K.: Discrete Mathematics for Computer Scientists. Addison-Wesley, Reading (1991)
Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, University of Edinburgh (1993)
Mukund, M.: Hereditary history preserving bisimulation is decidable for trace-labelled systems. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 289–300. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fröschle, S. (2005). Composition and Decomposition in True-Concurrency. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)