Abstract
The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics is defined in terms of bisimilarity that, in the finite case, can be computed via the well-known partition refinement algorithm. However, the behaviour of interactive systems is in many cases infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity.
This work was carried out during the tenure of an ERCIM “Alain Bensoussan” Fellowship Programme and supported by the IST 2004-16004 SEnSOria.
Chapter PDF
Similar content being viewed by others
References
Amadio, R.M., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous π-calculus. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 147–162. Springer, Heidelberg (1996)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional semantics for open Petri nets based on deterministic processes. M.S.C.S 15(1), 1–35 (2005)
Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B.: Bisimilarity and behaviour-preserving reconfiguration of open petri nets. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 126–142. Springer, Heidelberg (2007)
Bonchi, F., Montanari, U.: Symbolic semantics revisited. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 395–412. Springer, Heidelberg (2008)
Bonchi, F., Montanari, U.: Minimization algorithm for symbolic bisimilarity. Technical Report TR-08-27, Department of Informatics, University of Pisa (2008)
Cardelli, L., Gordon, A.D.: Mobile ambients. T.C.S. 240(1), 177–213 (2000)
Fernandez, J.C., Mounier, L.: “on the fly“ verification of behavioural equivalences and preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 181–191. Springer, Heidelberg (1992)
Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: Verifying mobile processes in the hal environment. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 511–515. Springer, Heidelberg (1998)
Hennessy, M., Lin, H.: Symbolic bisimulations. T.C.S. 138(2), 353–389 (1995)
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)
Kanellakis, P.C., Smolka, S.A.: Ccs expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43–68 (1990)
Merro, M., Zappa Nardelli, F.: Bisimulation proof methods for mobile ambients. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 584–598. Springer, Heidelberg (2003)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i and ii. Information and Computation 100(1), 1–40 (1992)
Montanari, U., Pistore, M.: Finite state verification for the asynchronous pi-calculus. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 255–269. Springer, Heidelberg (1999)
Montanari, U., Pistore, M.: An introduction to history dependent automata. Electr. Notes Theor. Comput. Sci. 10 (1997)
Montanari, U., Sassone, V.: Dynamic congruence vs. progressing bisimulation for ccs. Fundamenta Informaticae 16(1), 171–199 (1992)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)
Pistore, M., Sangiorgi, D.: A partition refinement algorithm for the π-calculus. Information and Computation 164(2), 264–321 (2001)
Sangiorgi, D.: A theory of bisimulation for the π-calculus. Acta Informatica 33(1), 69–97 (1996)
Victor, B., Moller, F.: The mobility workbench - a tool for the pi-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonchi, F., Montanari, U. (2009). Minimization Algorithm for Symbolic Bisimilarity . In: Castagna, G. (eds) Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science, vol 5502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00590-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-00590-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00589-3
Online ISBN: 978-3-642-00590-9
eBook Packages: Computer ScienceComputer Science (R0)