Abstract
It is well known that bisimulation on μ-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Ésik necessarily involve implicational rules. However, both systems rely on features which go beyond pure equational Horn logic: either the rules are impure by involving non-equational side-conditions, or they are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic.
This paper presents a positive and a negative result regarding axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner’s impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner’s and Bloom/Ésik’s axiomatisations are incomplete without the congruence rule, and neither system has a complete extension in rank 1 equational axioms. It remains open whether there are higher-rank equational axioms or Horn rules which would render Milner’s or Bloom/Ésik’s axiomatisations complete for unguarded processes.
This is a preview of subscription content, log in via an institution to check access.
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., Chen, T., Fokkink, W., Ingolfsdottir, A.: On the axiomatizability of priority. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 480–491. Springer, Heidelberg (2006)
Aceto, L., Fokkink, W., Ingolfsdottir, 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., Jeffrey, A.: A complete axiomatization of timed bisimulation for a class of timed regular behaviours. TCS 152(2), 251–268 (1995)
Andersen, H.R., Mendler, M.: An asynchronous process algebra with multiple clocks. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 58–73. Springer, Heidelberg (1994)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Springer, Heidelberg (1998)
Bloom, S.L., Ésik, Z.: Iteration algebras. Foundations of Computer Science 3(3), 245–302 (1992)
Bloom, S.L., Ésik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. In: EATCS Monographs in TCS, Springer, Heidelberg (1993)
Bloom, S.L., Ésik, Z.: Iteration algebras are not finitely axiomatizable. In: Gonnet, G.H., Viola, A. (eds.) LATIN 2000. LNCS, vol. 1776, pp. 367–376. Springer, Heidelberg (2000)
Chen, T., Fokkink, W.: On finite alphabets and infinite bases III: Simulation. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 421–434. Springer, Heidelberg (2006)
Cleaveland, R., Lüttgen, G., Mendler, M.: An algebraic theory of multiple clocks. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 166–180. Springer, Heidelberg (1997)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Australia (1971)
Ésik, Z.: The equational theory of fixed points with applications to generalized language theory. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 21–36. Springer, Heidelberg (2002)
Fokkink, W.: A complete equational axiomatization for prefix iteration. Information Processing Letters 52(6), 333–337 (1994)
Fokkink, W., Zantema, H.: Basic process algebra with iteration: Completeness of its equational axioms. The Computer J. 37(4), 259–267 (1994)
van Glabbeek, R.: The linear time–branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)
van Glabbeek, R.: A complete axiomatization for branching bisimulation congruence of finite state behaviours. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 473–484. Springer, Heidelberg (1993)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inform. & Comp. 110(2), 366–390 (1994)
Mendler, M., Lüttgen, G.: Is observational congruence on μ-expressions axiomatisable in equational Horn logic? Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik, Techn. Rep. No. 72, Univ. of Bamberg (June 2007)
Milner, R.: A complete inference system for a class of regular behaviours. J. of Computer and System Sciences 28(3), 439–466 (1984)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviours. Inform. & Comp. 81(2), 227–247 (1989)
Moller, F.: Axioms for Concurrency. PhD thesis, LFCS, Univ. of Edinburgh (1989), Also published as ECS-LFCS-89-84
Moller, F.: The nonexistence of finite axiomatisations for CCS congruences. In: LICS 1990, pp. 142–153. IEEE Computer Society Press, Los Alamitos (1990)
Nadathur, G., Miller, D.: Higher-order Horn clauses. JACM 37(4), 777–814 (1990)
Sewell, P.: Nonaxiomatisability of equivalences over finite state processes. Annals of Pure and Applied Logic 90, 163–191 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mendler, M., Lüttgen, G. (2007). Is Observational Congruence Axiomatisable in Equational Horn Logic?. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)