Abstract
Ready simulation has proven to be one of the most significant semantics in process theory. It is at the heart of a number of general results that pave the way to a comprehensive understanding of the spectrum of process semantics. Since its original definition by Bloom, Istrail and Meyer in 1995, several authors have proposed generalizations of ready simulation to deal with internal actions. However, a thorough study of the (non-)existence of finite (in)equational bases for weak ready simulation semantics is still missing in the literature. This paper presents a complete account of positive and negative results on the axiomatizability of weak ready simulation semantics over the language BCCSP. In addition, this study offers a thorough analysis of the axiomatizability properties of weak simulation semantics.
Luca Aceto and Anna Ingolfsdottir have been partially supported by the projects ‘New Developments in Operational Semantics’ (nr. 080039021) and ‘Meta-theory of Algebraic Process Theories’ (nr. 100014021) of the Icelandic Research Fund. David de Frutos Escrig and Carlos Gregorio-Rodríguez have been partially supported by the Spanish projects TESIS (TIN2009-14312-C02-01), DESAFIOS10 (TIN2009-14599-C03-01) and PROMETIDOS S2009/TIC-1465. The paper was begun when David de Frutos Escrig and Carlos Gregorio-Rodríguez held Abel Extraordinary Chair positions at Reykjavik University, and finalized while Luca Aceto and Anna Ingolfsdottir held Abel Extraordinary Chairs at Universidad Complutense de Madrid, Spain, supported by the NILS Mobility Project.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aceto, L., Bloom, B., Vaandrager, F.W.: Turning SOS rules into equations. Information and Compututation 111(1), 1–52 (1994)
Aceto, L., de Frutos Escrig, D., Gregorio-Rodríguez, C., Ingólfsdóttir, A.: Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet. Information Processing Letters 111(9), 408–413 (2011)
Aceto, L., Fokkink, W.J., Ingólfsdóttir, A.: Ready to preorder: Get your BCCSP axiomatization for free! In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 65–79. Springer, Heidelberg (2007)
Aceto, L., Fokkink, W.J., Ingólfsdóttir, A., Luttik, B.: Finite equational bases in process algebra: Results and open questions. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 338–367. Springer, Heidelberg (2005)
Aceto, L., Fokkink, W., Ingolfsdottir, A., Luttik, B.: A finite equational base for CCS with left merge and communication merge. ACM Trans. Comput. Log. 10(1) (2009)
Aceto, L., Fokkink, W., Ingólfsdóttir, A., Mousavi, M.R.: Lifting non-finite axiomatizability results to extensions of process algebras. Acta Informatica 47(3), 147–177 (2010)
Aceto, L., Hennessy, M.: Termination, deadlock and divergence. Journal of the ACM 39(1), 147–187 (1992)
Aceto, L., Ingolfsdottir, A., Luttik, B., van Tilburg, P.: Finite equational bases for fragments of CCS with restriction and relabelling. In: 5th IFIP International Conference on Theoretical Computer Science. IFIP, vol. 273, pp. 317–332. Springer, Heidelberg (2008)
Baeten, J., Basten, T., Reniers, M.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press, Cambridge (2009)
Baeten, J.C.M., de Vink, E.P.: Axiomatizing GSOS with termination. Journal of Logic and Algebraic Programming 60-61, 323–351 (2004)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60(1-3), 109–137 (1984)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)
Chen, T.: Clocks, Dice and Processes. PhD thesis, Centrum voor Wiskunde en Informatica (CWI), Vrije Universiteit, Amsterdam (2009)
Chen, T., Fokkink, W.: On the axiomatizability of impossible futures: Preorder versus equivalence. In: LICS, pp. 156–165. IEEE Computer Society, Los Alamitos (2008)
Chen, T., Fokkink, W., Luttik, B., Nain, S.: On finite alphabets and infinite bases. Information and Computation 206(5), 492–519 (2008)
Chen, T., Fokkink, W., van Glabbeek, R.J.: Ready to preorder: The case of weak process semantics. Information Processing Letters 109(2), 104–111 (2008)
de Frutos-Escrig, D., Gregorio-Rodríguez, C., Palomino, M.: On the unification of process semantics: Equational semantics. Electronic Notes in Theoretical Computer Science 249, 243–267 (2009)
de Frutos-Escrig, D., Gregorio-Rodríguez, C.: Universal coinductive characterizations of process semantics. In: 5th IFIP International Conference on Theoretical Computer Science. IFIP, vol. 273, pp. 397–412. Springer, Heidelberg (2008)
de Frutos-Escrig, D., Gregorio-Rodríguez, C.: (Bi)simulations up-to characterise process semantics. Information and Computation 207(2), 146–170 (2009)
de Frutos-Escrig, D., Gregorio-Rodríguez, C., Palomino, M.: Ready to preorder: an algebraic and general proof. Journal of Logic and Algebraic Programming 78(7), 539–551 (2009)
De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)
van Glabbeek, R.J.: The linear time - branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
van Glabbeek, R.J.: The linear time – branching time spectrum I; the semantics of concrete, sequential processes. In: Handbook of Process Algebra, vol. ch. 1, pp. 3–99. Elsevier, Amsterdam (2001)
van Glabbeek, R.J., Weijland, P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
van Glabbeek, R.J.: A characterisation of weak bisimulation congruence. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 26–39. Springer, Heidelberg (2005)
Groote, J.F.: A new strategy for proving omega-completeness applied to process algebra. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 314–331. Springer, Heidelberg (1990)
Hennessy, M.: A term model for synchronous processes. Informationa and Control 51(1), 58–75 (1981)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–161 (1985)
Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28 (1991)
Lüttgen, G., Vogler, W.: Ready simulation for concurrency: It’s logical! Information and Computation 208(7), 845–867 (2010)
Milner, R.: An algebraic definition of simulation between programs. In: Proceedings 2nd Joint Conference on Artificial Intelligence, pp. 481–489. BCS (1971); Also available as Report No. CS-205, Computer Science Department, Stanford University
Milner, R.: A modal characterisation of observable machine behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 25–34. Springer, Heidelberg (1981)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviors. Information and Computation 81(2), 227–247 (1989)
Moller, F.: Axioms for Concurrency. PhD thesis, Report CST-59-89, Department of Computer Science, University of Edinburgh (1989)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)
Ulidowski, I.: Axiomatisations of weak equivalences for De Simone languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 219–233. Springer, Heidelberg (1995)
Ulidowski, I.: Refusal simulation and interactive games. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 208–222. Springer, Heidelberg (2002)
Voorhoeve, M., Mauw, S.: Impossible futures and determinism. Information Processing Letters 80(1), 51–58 (2001)
Walker, D.: Bisimulation and divergence. Information and Computation 85(2), 202–241 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., de Frutos Escrig, D., Gregorio-Rodríguez, C., Ingolfsdottir, A. (2011). Axiomatizing Weak Ready Simulation Semantics over BCCSP. In: Cerone, A., Pihlajasaari, P. (eds) Theoretical Aspects of Computing – ICTAC 2011. ICTAC 2011. Lecture Notes in Computer Science, vol 6916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23283-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-23283-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23282-4
Online ISBN: 978-3-642-23283-1
eBook Packages: Computer ScienceComputer Science (R0)