Abstract
This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioral semantics over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller’s celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied.
This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioral semantics over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller’s celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
L. Aceto, T. Chen, W. Fokkink, and A. Ingolfsdottir. On the axiomatizability of priority. Proceedings of Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Part II}, volume 4052 of LNCS, pages 480–491, Springer, 2006.
L. Aceto, W. Fokkink and A. Ingolfsdottir. Ready to preorder: Get your BCCSP axiomatization for free! Proceedings of CALCO’07, volume 4624 of LNCS, pages 338–367. Springer, 2007.
L. Aceto, W. Fokkink, A. Ingolfsdottir, and B. Luttik. CCS with Hennessy’s merge has no finite equational axiomatization. Theoretical Computer Science, 330(3):377–405, 2005.
L. Aceto, W. Fokkink, A. Ingolfsdottir, and B. Luttik. Finite equational bases in process algebra: Results and open questions. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of LNCS, pages 338–367. Springer, 2005.
L. Aceto, W. Fokkink, A. Ingolfsdottir, and M.R. Mousavi. Lifting non-finite axiomatizability results to extensions of process algebras. Technical Report CSR-08-05, TU/Eindhoven, 2008.
L. Aceto, W. Fokkink, A. Ingolfsdottir, and S. Nain. Bisimilarity is not finitely based over BPA with interrupt. Theoretical Computer Science, 366(1–2):60–81, 2006.
L. Aceto and M. Hennessy. Termination, deadlock, and divergence. Journal of the ACM, 39(1):147–187, 1992.
L. Aceto, A. Ingolfsdottir and M. R. Mousavi. Impossibility results for the equational theory of Timed CCS. Proceedings of CALCO’07, volume 4624 of LNCS, pages 80–95, Springer, 2007.
J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1–3):109–137, 1984.
S.C.C. Blom, W.J. Fokkink, J.F. Groote, I. van Langevelde, B. Lisser, and J.C. van de Pol. mCRL: A toolset for analysing algebraic specifications. Proceedings of CAV’01, volume 2102 of LNCS, pages 250-254, Springer, 2001.
S. L. Bloom and Z. Ésik. Nonfinite axiomatizability of shuffle inequalities. Proceedings of TAPSOFT’95, volume 915 of LNCS, pages 318–333. Springer, 1995.
Z. Ésik and M. Bertol. Nonfinite axiomatizability of the equational theory of shuffle. Acta Informatica, 35(6):505–539, 1998.
M. Hennessy. A term model for synchronous processes. Information and Control, 51(1):58–75, 1981.
M. Hennessy. Algebraic Theory of Processes. Foundations of Computing Series. MIT Press, 1988.
H. Hermanns. Interactive Markov Chains and the Quest for Quantified Quality. Volume 2428 of LNCS, Springer, 2002.
G. Lüttgen and W. Vogler. Bisimulation on speed: worst-case efficiency. Information and Computation, 191(2): 105–144, 2004.
G. Lüttgen and W. Vogler. Bisimulation on speed: Lower time bounds. Proceedings of FOSSACS’04, volume 2987 of LNCS, Springer, 2004.
G. Lüttgen and W. Vogler. Bisimulation on speed: A unified approach. Theoretical Computer Science, 360(1–3):209-227, 2006.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
F. Moller. Axioms for Concurrency. Ph.D. Thesis, University of Edinburgh, 1989.
F. Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 142–153. IEEE Computer Society, 1990.
F. Moller. The importance of the left merge operator in process algebras. In Proceedings of ICALP’90, volume 443 of LNCS, pages 752–764. Springer, 1990.
F. Moller and C.M.N. Tofts. A temporal calculus of communicating systems. In Proceedings of CONCUR’90, volume 458 of LNCS, pages 401–415. Springer, 1990.
F. Moller and C. Tofts. Relating processes with respect to speed. In Proceedings of CONCUR ’91, volume 527 of LNCS, pages 424–438. Springer, 1991.
X. Nicollin, J. Sifakis. The algebra of timed processes, ATP: Theory and application. Information and Computation, 114(1):131–178, 1994.
M. Sipser. Introduction to the Theory of Computation. 2nd Ed., PWS Publishing, 2005.
W. Yi. Real-time behaviour of asynchronous agents. In Proceedings of CONCUR’90, volume 458 of LNCS, pages 502–520. Springer, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Aceto, L., Fokkink, W., Ingolfsdottir, A., Mousavi, M. (2008). Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_21
Download citation
DOI: https://doi.org/10.1007/978-0-387-09680-3_21
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09679-7
Online ISBN: 978-0-387-09680-3
eBook Packages: Computer ScienceComputer Science (R0)