Abstract
We present a first-order extension of the algebraic theory about processes known as ACP and its main models. Useful predicates on processes, such as deadlock freedom and determinism, can be added to this theory through first-order definitional extensions. Model theory is used to analyse the discrepancies between identity in the models of the first-order extension of ACP and bisimilarity of the transition systems extracted from these models, and also the discrepancies between deadlock freedom in the models of a suitable first-order definitional extension of this theory and deadlock freedom of the transition systems extracted from these models. First-order definitions are material to the formalization of an interpretation of one theory about processes in another. We give a comprehensive example of such an interpretation too.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60, 109–137 (1984)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)
Milner, R. (ed.): A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Bergstra, J.A., Loots, M.E.: Program algebra for sequential code. Journal of Logic and Algebraic Programming 51, 125–156 (2002)
Bergstra, J.A., Bethke, I.: Polarized process algebra and program equivalence. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1–21. Springer, Heidelberg (2003)
Baeten, J.C.M., Bergstra, J.A.: On sequential composition, action prefixes and process prefix. Formal Aspects of Computing 6, 250–268 (1994)
Shoenfield, J.R.: Mathematical Logic. Addison-Wesley Series in Logic. Addison-Wesley, Reading (1967)
Chang, C.C., Keisler, H.J.: Model Theory, 3rd edn. Studies in Logic and the Foundations of Mathematics, vol. 73. Elsevier, Amsterdam (1990)
Hodges, W.A.: Model Theory. Encyclopedia of Mathematics and Its Applications, vol. 42. Cambridge University Press, Cambridge (1993)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. Theoretical Computer Science 51, 129–176 (1987)
Hennessy, M., Milner, R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM 32, 137–161 (1985)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. In: de Bakker, J.W., Hazewinkel, M., Lenstra, J.K. (eds.) Proceedings Mathematics and Computer Science I. CWI Monograph, vol. 1, pp. 89–138. North-Holland, Amsterdam (1986)
Bergstra, J.A., Klop, J.W.: Process algebra: Specification and verification in bisimulation semantics. In: Hazewinkel, M., Lenstra, J.K., Meertens, L.G.L.T. (eds.) Proceedings Mathematics and Computer Science II. CWI Monograph, vol. 4, pp. 61–94. North-Holland, Amsterdam (1986)
Bergstra, J.A., Klop, J.W.: Process theory based on bisimulation semantics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 50–122. Springer, Heidelberg (1989)
Bergstra, J.A., Klop, J.W.: A convergence theorem in process algebra. In: de Bakker, J.W., Rutten, J.J.M.M. (eds.) Ten Years of Concurrency Semantics, pp. 164–195. World Scientific, Singapore (1992)
van Benthem, J.F.A.K., Bergstra, J.A.: Logic of transition systems. Journal of Logic, Language and Information 3, 247–283 (1995)
Fokkink, W.J.: Introduction to Process Algebra. In: Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2000)
van Benthem, J.F.A.K., van Eijck, D.J.N., Stebletsova, V.: Modal logic, transition systems and processes. Journal of Logic and Computation 4, 811–855 (1994)
Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 82–95. Springer, Heidelberg (1984)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Fokkink, W.J.: A complete equational axiomatization for prefix iteration. Information Processing Letters 52, 333–337 (1994)
Bergstra, J.A., Bethke, I., Ponse, A.: Process algebra with iteration and nesting. Computer Journal 37, 243–258 (1994)
Bergstra, J.A., Fokkink, W.J., Ponse, A.: Process algebra with recursive operations. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 333–389. Elsevier, Amsterdam (2001)
Bergstra, J.A., Ponse, A.: Non-regular iterators in process algebra. Theoretical Computer Science 269, 203–229 (2001)
Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Formal Aspects of Computing 3, 142–188 (1991)
Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Formal Aspects of Computing 8, 188–208 (1996)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. In: Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2002)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Conditional axioms and α/ β-calculus in process algebra. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 53–75. North-Holland, Amsterdam (1987)
Bergstra, J.A., Middelburg, C.A., Ştefănescu, G.: Network algebra for asynchronous dataflow. International Journal of Computer Mathematics 65, 57–88 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bergstra, J.A., Middelburg, C.A.(. (2005). Model Theory for Process Algebra. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_21
Download citation
DOI: https://doi.org/10.1007/11601548_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30911-6
Online ISBN: 978-3-540-32425-6
eBook Packages: Computer ScienceComputer Science (R0)