Abstract
Labeled transition systems are key structures for modeling computation. In this paper, we show how they lend themselves to ordinary logical analysis (without any special new formalisms), by introducing their standard first-order theory. This perspective enables us to raise several basic model-theoretic questions of definability, axiomatization and preservation for various notions of process equivalence found in the computational literature, and answer them using well-known logical techniques (including the Compactness theorem, Saturation and Ehrenfeucht games). Moreover, we consider what happens to this general theory when one restricts attention to special classes of transition systems (in particular, finite ones), as well as extended logical languages (in particular, infinitary first-order logic). We hope that this puts standard logical formalisms on the map as a serious option for a theory of computational processes. As a side benefit, our approach increases comparability with several other existing formalisms over labeled transition systems (such as Process Algebra or Modal Logic). We provide some pointers to this effect, too.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Baeten, J. and Bergstra, J.A., 1993, ‘On Sequential Composition, Action Prefixes and Process Prefix’, Departments of Computer Science, University of Amsterdam and University of Eindhoven.
Bergstra, J.A. and Klop, J.-W., 1984, ‘Process Algebra for Synchronous Communication’,Information and Control 60, 109–137.
Bergstra, J.A. and Klop, J.-W., 1986, ‘Process Algebra: Specification and Verification in Bisimulation Semantics’, inMathematics and Computer Science II, M. Hazewinkelet al., eds., North-Holland, Amsterdam, pp. 61–94.
Bergstra, J.A. and Klop, J.-W., 1988, ‘A Complete Inference System for Regular Processes with Silent Moves’, inLogic Colloquium '86, F. Drake and J. Truss, eds., North-Holland, Amsterdam, pp. 21–81.
Chang, C.C. and Keisler, H.J., 1973,Model Theory, North-Holland, Amsterdam.
De Jongh, D. and Troelstra, A., 1966, ‘On the Connection of Partially Ordered Sets with Some Pseudo-Boolean Algebras’,Indagationes Mathematicae 28, 317–329.
De Nicola, R. and Vaandrager, F., 1990, ‘Three Logics of Branching Bisimulation’, inProceedings 5th LICS Conference, Computer Society Press, pp. 118–129.
Doets, K., 1987,Completeness and Definability. Applications of the Ehrenfeucht Game in Second-Order and Intensional Logic, Dissertation, Mathematical Institute, University of Amsterdam.
Doets, K., 1993,Model Theory, Lecture Notes for the Fifth European Summer School in Logic, Language and Information, University of Lisbon.
Goldblatt, R., 1982,Axiomatizing the Logic of Computer Programming, Springer, Berlin.
Gurevich, Y., 1985, ‘Logic and the Challenge of Computer Science’, Computing Research Laboratory, The University of Michigan, Ann Arbor.
Harel, D., 1984, ‘Dynamic Logic’, inHandbook of Philosophical Logic, Vol. II, D. Gabbay and F. Guenthner, eds., Reidel, Dordrecht, pp. 497–604.
Hennessy, M. and Milner, R., 1985, ‘Algebraic Laws for Nondeterminism and Concurrency’,Journal of the ACM 32, 137–161.
Immerman, N. and Kozen, D., 1987, ‘Definability with Bounded Number of Bound Variables’, inProceedings IEEE 1987, pp. 236–244.
Keisler, H.J., 1971,Model Theory for Infinitary Logic, North-Holland, Amsterdam.
Keisler, H.J., 1977, ‘Fundamentals of Model Theory’,in Handbook of Mathematical Logic, J. Barwise, ed., North-Holland, Amsterdam, pp. 47–103.
Milner, R., 1980,A Calculus of Communicating Systems, Springer, Berlin.
Park, D., 1981, ‘Concurrency and Automata on Infinite Sequences’, inProceedings 5th GI Conference, Springer, Berlin, pp. 167–183.
Salwicki, A., 1970, ‘Formalised Algorithmic Languages’,Bulletin Polish Academy of Sciences, Series Sci. Math. Astr. Phy., Vol. 18, pp. 227–232.
Stirling, C., 1989, ‘Modal and Temporal Logics’, to appear inHandboook of Logic in Computer Science, S. Abramskyet al., eds., Oxford University Press, Oxford.
Van Benthem, J., 1976,Modal Correspondence Theory, Dissertation, Mathematical Institute, University of Amsterdam.
Van Benthem, J., 1985,Modal Logic and Classical Logic, Bibliopolis, Napoli.
Van Benthem, J., 1991,Language in Action. Categories, Lambdas and Dynamic Logic, North-Holland, Amsterdam.
Van Benthem, J., 1993, ‘Which Program Constructions Are Safe for Bisimulation?’, Institute for Logic, Language and Computation, University of Amsterdam. (To appear in D. Richard et al., eds., Logic Colloquium. Clermont-Ferrand 1994, Elsevier Science Publishers, Amsterdam).
Van Benthem, J., van Eyck, J. and Stebletsova, V., 1993, ‘Modal Logic, Transition Systems and Processes’, Centre for Mathematics and Computer Science (CWI), Amsterdam. (To appear in the Journal of Logic and Computation).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Van Benthem, J., Bergstra, J. Logic of transition systems. J Logic Lang Inf 3, 247–283 (1994). https://doi.org/10.1007/BF01160018
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01160018