Abstract
This paper presents a complete account of positive and negative results on the finite axiomatizability of weak complete simulation semantics over the language BCCSP. We offer finite (un)conditional ground-complete axiomatizations for the weak complete simulation precongruence. In sharp contrast to this positive result, we prove that, in the presence of at least one observable action, the (in)equational theory of the weak complete simulation precongruence over BCCSP does not have a finite (in)equational basis. In fact, the set of (in)equations in at most one variable that hold in weak complete simulation semantics over BCCSP does not have an (in)equational basis of ‘bounded depth’, let alone a finite one.
Luca Aceto and Anna Ingólfsdóttir have been partially supported by the projects ‘New Developments in Operational Semantics’ (nr. 080039021) and ‘Meta-theory of Algebraic Process Theories’ (No. 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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aceto, L., Bloom, B., Vaandrager, F.W.: Turning SOS rules into equations. Information and Computation 111(1), 1–52 (1994)
Aceto, L., de Frutos Escrig, D., Gregorio-Rodríguez, C., Ingólfsdóttir, A.: Axiomatizing Weak Ready Simulation Semantics over BCCSP. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 7–24. Springer, Heidelberg (2011)
Aceto, L., Fokkink, W., 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., Ingólfsdóttir, A., Mousavi, M.: Lifting non-finite axiomatizability results to extensions of process algebras. Acta Informatica 47(3), 147–177 (2010)
Baeten, J., Basten, T., Reniers, M.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press (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., Fokkink, W., van Glabbeek, R.: On the axiomatizability of impossible futures (unpublished manuscript, 2011)
Chen, T., Fokkink, W., Luttik, B., Nain, S.: On finite alphabets and infinite bases. Information and Computation 206(5), 492–519 (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)
van Glabbeek, R.: The linear time – branching time spectrum I; the semantics of concrete, sequential processes. In: Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier (2001)
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 (1985)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)
Milner, R.: An algebraic definition of simulation between programs. In: Proceedings 2nd Joint Conference on Artificial Intelligence, pp. 481–489. BCS (1971)
Milner, R.: Communication and Concurrency. Prentice Hall (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)
Park, D.M.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., de Frutos-Escrig, D., Gregorio-Rodríguez, C., Ingólfsdóttir, A. (2012). The Equational Theory of Weak Complete Simulation Semantics over BCCSP. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds) SOFSEM 2012: Theory and Practice of Computer Science. SOFSEM 2012. Lecture Notes in Computer Science, vol 7147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27660-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-27660-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27659-0
Online ISBN: 978-3-642-27660-6
eBook Packages: Computer ScienceComputer Science (R0)