Abstract
An introduction to (first-order) Ehrenfeucht-Fraïssé games is presented, and three applications in theoretical computer science are discussed. These are concerned with the expressive power of first-order logic over graphs, formal languages definable in first-order logic, and modal logic over labelled transition systems.
The present work was supported by EBRA Working Group ”Algebraic and Syntactic Methods in Computer Science (ASMICS II)”.
Chapter PDF
Similar content being viewed by others
Keywords
- Modal Logic
- Expressive Power
- Label Transition System
- Theoretical Computer Science
- Formal Language Theory
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.
References
J. Barwise, S. Feferman (eds.), Model-Theoretic Logics, Springer-Verlag, Berin-Heidelberg, New York 1985.
U. Bosse, An “Ehrenfeucht-Fraïssé game” for fixpoint logic and stratified fixpoint logic, manuscript, Math. Inst., Universität Freiburg, 1992.
H.D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic, Springer-Verlag, New York 1984 (revised and extended edition to appear 1993).
A. Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fund. Math. 49 (1961), 129–141.
R. Fagin, Monadic generalized spectra, Z. math. Logik u. Grundl. Math. 21 (1975), 123–134.
R. Fagin, L. Stockmeyer, M.Y. Vardi, A simple proof that connectivity separates existential and universal monadic second-order logic over finite structures, IBM Rep. RJ 8647, 1992.
J. Flum, First-order logic and its extensions, in: Proc. ISILC Logic Conf, Kiel, Springer Lect. Notes in Math. 499 (1975), 248–310.
J. Flum, On bounded theories, in: Computer Science Logic (E. Börger et al., eds.), Springer LNCS 626 (1992), 111–118.
R. Fraïssé, Sur quelques classifications des relations, basés sur des isomorphismes restreints, Publ. Sci. de l'Univ. Alger, Sér. A 1 (1954), 35–182.
H. Gaifman, On local and non-local properties, in: Proc. of the Herbrand Symposium, Logic Colloquium '81 (J. Stern, ed.), North-Holland, Amsterdam 1982, pp. 105–135.
E. Grädel, On transitive closure logic, in: Computer Science Logic (E. Börger et al., eds.), Springer LNCS 626 (1992), 149–165.
Y. Gurevich, S. Shelah, Rabin's uniformization problem, J. Symb. Logic 48 (1983), 1105–1119.
W.P. Hanf, Model-theoretic methods in the study of elementary logic, in: The Theory of Models (J.W. Addison, L. Henkin, A. Tarski, eds.), North-Holland, Amsterdam 1965, pp. 132–145.
M. Hennessy, R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach. 21 (1985), 137–161.
J. Hintikka, Distributive normal forms in the calculus of predicates, Acta Philos. Fennica 6 (1953).
N. Immerman, Upper and lower bounds for first-order expressibility, J. Comput. System Sci. 25 (1982), 76–98.
N. Immerman, D. Kozen, Definability with a bounded number of bound variables, Inform. Comput. 83 (1989), 121–139.
Ph. Kolaitis, M. Vardi, On the expressive power of Datalog: Tools and a case study, Proc. 9th ACM Symp. on Principles of Database Systems, 61–71.
R.E. Ladner, Application of model-theoretic games to discrete linear orders and finite automata, Inform. Contr. 33 (1977), 281–303.
D. Lippert, W. Thomas, Relativized star-free expressions, first-order logic, and a concatenation game, in: Semigroup Theory and Applications (H. Jürgensen et al. eds.), Springer Lect. Notes in Math. 1320 (1988), 194–204.
R. Milner, Operational and algebraic semantics of concurrent processes, in: Handbook of Theoretical Computer Science (J. v. Leeuwen, ed.), Vol. B, Elsevier Science Publ., Amsterdam 1990, pp. 1201–1241.
D. Monk, Mathematical Logic, Springer-Verlag, New York 1976.
H. Oguztüzün, A fragment of first-order logic adequate for observation equivalence, in: Computer Science Logic (E. Borger et al., eds.), Springer LNCS 626 (1992), 287–291.
D. Park, Concurrency and automata on infinite sequences, in: Theoretical Computer Science (P. Deussen, ed.), Springer LNCS 104 (1981), 167–183.
A. Potthoff, Modulo counting quantifiers over finite trees, in: CAAP'92 (J.C. Raoult, ed.), LNCS 581 (1992), 265–278.
J.G. Rosenstein, Linear Orderings, Academic Press, New York 1982.
D. Scott, A note on distributive normal forms, in: Essays in Honour of Jaakko Hintikka (E. Saarinen et al., eds.), Reidel, Dordrecht 1979, pp. 75–90.
S. Shelah, The monadic theory of order, Ann. Math. 102 (1975), 379–419.
W. Thomas, An application of the Ehrenfeucht-Fraïssé game in formal language theory, Bull. Soc. Math. France, Mem. 16 (1984), 11–21.
W. Thomas, A concatenation game and the dot-depth hierarchy, in: Computation Theory and Logic (E. Börger, ed.), LNCS 270 (1987), 415–426.
W. Thomas, On chain logic, path logic, and first-order logic over infinite trees, Proc. 2nd LICS, Ithaca, N.Y. 1987, 245–256.
W. Thomas, On logics, tilings, and automata, in: Proc. 18th ICALP, Madrid (J. Leach Albert et al., eds.), Springer LNCS 510 (1991), 441–454.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thomas, W. (1993). On the Ehrenfeucht-Fraïssé game in theoretical computer science. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_89
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_89
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive