Abstract
In this paper, we study the complexity and decidability issues of checking trace and bisimulation equivalences for the model of systems with many identical processes with respect to various interprocess communication structures. In our model, each system consists of an arbitrary number of identical finite state processes using Milner's Calculus of Communicating Systems (CCS) as the style of interprocess communication. As it turns out, checking trace and bisimulation equivalences are undecidable for star-like and linear systems, whereas the two problems are complete for PSPACE and PTIME, respectively, for fully connected systems.
This work was supported in part by the National Science Council of the Republic of China under Grant NSC-84-2221-E-002-039.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Christensen, S. and Hüttel, H. Decidability issues for infinite-state processes — a survey. EATCS Bulletin 51, pp. 156–166, (1993).
Clark, E., Grümberg, O. and Browne, M. Reasoning about networks with many identical finite-state processes. PODC'86, pp. 240–248, (1986).
Garg, V. Analysis of distributed systems with many identical processes. IEEE Int. Conf. on Distributed Computing Systems, pp. 358–365, (1988).
German, S. and Sistla, A. Reasoning about systems with many processes. JACM 39, 675–735, (1992).
Girkar, M. and Moll, R. Undecidability of bisimulations in concurrent systems with indefinite number of identical processes. Dept. of Computer Science, Univ. of Massachusetts, CMPSCI Technical Report 93-86, December 1993.
Girkar, M. and Moll, R. New results on the analysis of concurrent systems with an indefinite number of processes. CONCUR'94, (1994).
Hirshfeld, Y. Petri nets and the equivalence problem. CSL, (1993).
Hüttel, H. Undecidable equivalences for basic parallel processes. 13th FST&TCS, pp. 454–464, (1993).
Jančar, P. Decidability questions for bisimilarity of Petri nets and some related problems. STACS'94, LNCS 755, pp. 581–592, (1994).
Kanellakis, P. and Smolka, S. On the analysis of cooperation and antagonism in networks of communicating processes, Algorithmica 3, pp. 421–450, (1988).
Kanellakis, P. and Smolka, S. CCS expression, finite state processes, and three problems of equivalence. Information and Computation 86, pp. 43–68, (1990).
Sistla, A. and German, S. Reasoning with many processes. LICS'87, pp. 138–152, (1987).
van Glabbeek, R. The linear time-branching time spectrum. CONCUR'90, LNCS 458, pp. 278–297, (1990).
Yen, H. Priority systems with many identical processes. Acta Informatica 28, pp. 681–692 (1991).
Yen, H., Jian, S., and Lao, T. Deciding Bisimulation and Trace Equivalences for Systems with Many Identical Processes. Tech. Report, Dept. of Electrical Engineering, National Taiwan Univ., 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yen, HC., Jian, ST., Lao, TP. (1995). Deciding bisimulation and trace equivalences for systems with many identical processes. In: Staples, J., Eades, P., Katoh, N., Moffat, A. (eds) Algorithms and Computations. ISAAC 1995. Lecture Notes in Computer Science, vol 1004. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015435
Download citation
DOI: https://doi.org/10.1007/BFb0015435
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60573-7
Online ISBN: 978-3-540-47766-2
eBook Packages: Springer Book Archive