×

zbMATH — the first resource for mathematics

Logic of transition systems. (English) Zbl 0827.03019
Summary: 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.

MSC:
03B80 Other applications of logic
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
03B45 Modal logic (including the logic of norms)
03C07 Basic properties of first-order languages and structures
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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. · Zbl 0942.68608
[2] Bergstra, J.A. and Klop, J.-W., 1984, ?Process Algebra for Synchronous Communication?,Information and Control 60, 109-137. · Zbl 0597.68027 · doi:10.1016/S0019-9958(84)80025-X
[3] 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.
[4] 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. · Zbl 0647.68033
[5] Chang, C.C. and Keisler, H.J., 1973,Model Theory, North-Holland, Amsterdam.
[6] De Jongh, D. and Troelstra, A., 1966, ?On the Connection of Partially Ordered Sets with Some Pseudo-Boolean Algebras?,Indagationes Mathematicae 28, 317-329. · Zbl 0137.02203
[7] De Nicola, R. and Vaandrager, F., 1990, ?Three Logics of Branching Bisimulation?, inProceedings 5th LICS Conference, Computer Society Press, pp. 118-129.
[8] Doets, K., 1987,Completeness and Definability. Applications of the Ehrenfeucht Game in Second-Order and Intensional Logic, Dissertation, Mathematical Institute, University of Amsterdam.
[9] Doets, K., 1993,Model Theory, Lecture Notes for the Fifth European Summer School in Logic, Language and Information, University of Lisbon.
[10] Goldblatt, R., 1982,Axiomatizing the Logic of Computer Programming, Springer, Berlin. · Zbl 0474.68045
[11] Gurevich, Y., 1985, ?Logic and the Challenge of Computer Science?, Computing Research Laboratory, The University of Michigan, Ann Arbor.
[12] Harel, D., 1984, ?Dynamic Logic?, inHandbook of Philosophical Logic, Vol. II, D. Gabbay and F. Guenthner, eds., Reidel, Dordrecht, pp. 497-604. · Zbl 0875.03076
[13] Hennessy, M. and Milner, R., 1985, ?Algebraic Laws for Nondeterminism and Concurrency?,Journal of the ACM 32, 137-161. · Zbl 0629.68021 · doi:10.1145/2455.2460
[14] Immerman, N. and Kozen, D., 1987, ?Definability with Bounded Number of Bound Variables?, inProceedings IEEE 1987, pp. 236-244.
[15] Keisler, H.J., 1971,Model Theory for Infinitary Logic, North-Holland, Amsterdam. · Zbl 0222.02064
[16] Keisler, H.J., 1977, ?Fundamentals of Model Theory?,in Handbook of Mathematical Logic, J. Barwise, ed., North-Holland, Amsterdam, pp. 47-103.
[17] Milner, R., 1980,A Calculus of Communicating Systems, Springer, Berlin. · Zbl 0452.68027
[18] Park, D., 1981, ?Concurrency and Automata on Infinite Sequences?, inProceedings 5th GI Conference, Springer, Berlin, pp. 167-183.
[19] Salwicki, A., 1970, ?Formalised Algorithmic Languages?,Bulletin Polish Academy of Sciences, Series Sci. Math. Astr. Phy., Vol. 18, pp. 227-232. · Zbl 0198.02801
[20] Stirling, C., 1989, ?Modal and Temporal Logics?, to appear inHandboook of Logic in Computer Science, S. Abramskyet al., eds., Oxford University Press, Oxford.
[21] Van Benthem, J., 1976,Modal Correspondence Theory, Dissertation, Mathematical Institute, University of Amsterdam.
[22] Van Benthem, J., 1985,Modal Logic and Classical Logic, Bibliopolis, Napoli. · Zbl 0639.03014
[23] Van Benthem, J., 1991,Language in Action. Categories, Lambdas and Dynamic Logic, North-Holland, Amsterdam. · Zbl 0717.03001
[24] 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).
[25] 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).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.