Abstract
This is a survey article on the connections between the “sequential calculus” of Büchi, a system which allows to formalize properties of words, and the theory of automata. In the sequential calculus, there is a predicate for each letter and the unique extra non logical predicate is the relation symbol <, which is interpreted as the usual order on the integers. Several famous classes have been classified within this logic. We briefly review the main results concerning second order, which covers classes like PH, NP, P, etc., and then study in more detail the results concerning the monadic second-order and first-order logic. In particular, we survey the results and fascinating open problems dealing with the first-order quantifier hierarchy. We also discuss the first-order logic of one successor and the linear temporal logic. There are in fact three levels of results, since these logics can be interpreted on finite words, infinite words or bi-infinite words. The paper is self-contained. In particular, the necessary background on automata and finite semigroups is presented in a long introductory section, which includes some very recent results on the algebraic theory of infinite words.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
J. Almeida, Implicit operations on finiteJ-trivial semigroups and a conjecture of I. Simon, J. Pure Appl. Algebra 69(1990)205–218.
M. Arfi, Polynomials operations and relational languages,4th STACS, Lecture Notes in Computer Science 247 (Springer, 1987) pp. 198–206.
M. Arfi, Opérations polynomiales et hiérarchies de concaténation, Theor. Comput. Sci. 91(1991)71–84.
A. Arnold, A syntactic congruence for rational ω-languages, Theor. Comput. Sci. 39(1985)333–335.
D. Beauquier, Bi-limites de langages reconnaissables, Theor. Comput. Sci. 33(1984)335–342.
D. Beauquier, Ensembles reconnaissables de mots bi-infinis, in:Automata on Infinite Words, ed. M. Nivat, Lecture Notes in Computer Science 192 (Springer, 1985) pp. 28–46.
D. Beauquier and M. Nivat, About rational sets of factors of a bi-infinite word, in:Automata, Languages and Programming, ed. W. Brauer, Lecture Notes in Computer Science 194 (Springer, 1985) pp. 33–42.
D. Beauquier and J.E. Pin, Factors of words, in:Automata, Languages and Programming, eds. G. Ausiello, M. Dezani-Ciancaglini and S. Ronchi Della Rocca, Lecture Notes in Computer Science 372 (Springer, 1989) pp. 63–79.
D. Beauquier and J.E. Pin, Languages and scanners, Theor. Comput. Sci. 84(1991)3–21.
J.A. Brzozowski and R. Knast, The dot-depth huerarchy of star-free languages is infinite, J. Comput. Syst. Sci. 16(1978)37–55.
J.A. Brzozowski and I. Simon, Characterizations of locally testable languages, Discr. Math. 4(1973)243–271.
J.R. Büchi, Weak second-order arithmetic and finite automata, Z. Math. Logik und Grundl. Math. 6(1960)66–92.
J.R. Büchi, On a decision method in restricted second-order arithmetic,Proc. 1960 Int. Congr. for Logic, Methodology and Philosophy of Science (Stanford University Press, Stanford, 1962) pp. 1–11.
J.R. Büchi and L.H. Landweber, Definability in the monadic second-order theory of successors, J. Symb. Logic 34(1969)166–170.
S. Cho and D.T. Huynh, Finite automaton aperiodicity is PSPACE-complete, Theor. Comput. Sci. 88(1991)99–116.
J. Cohen, On the expressive power of temporal logic for infinite words, Theor. Comput. Sci. 83(1991)301–312.
J. Cohen, D. Perrin and J.E. Pin, On the expressive power of temporal logic, J. Comput. Syst. Sci. (1993).
K. Compton, On rich words, in:Combinatoric Words, Progress and Perspectives, ed. L. Cummings (Academic Press, 1983) pp. 39–62
D. Cowan, Inverse monoids of dot-depth 2, Int. J. Alg. Comp. 3(1993)411–424.
S. Eilenberg,Automata, Languages and Machines, Vol. A (Academic Press, New York, 1974).
S. Eilenberg,Automata, Languages and Machines, Vol. B (Academic Press, New York, 1976).
C.C. Elgot, Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc. 98(1961)21–52.
E.A. Emerson, Temporal and modal logic, in:Handbook of Theoretical Computer Science, Vol. B:Formal Models and Semantics (Elsevier, 1990) pp. 995–1072.
R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets,SIAM-AMS Proc. 7(1974)43–73.
R. Fagin, Finite-model theory — a personal perspective, Theor. Comput. Sci. 116(1993)3–31.
H. Gaifman, On local and non-local properties,Proc. Herbrandt Symposium, Logic Colloquium '81, ed. J. Stern, Studies in Logic 107 (North-Holland, Amsterdam, 1982) pp. 105–135.
D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, On the temporal analysis of fairness,Proc. 7th ACM Symp. Princ. Progr. Lang. (1980) pp. 163–173.
B.R. Hodgson, Décidabilité par automate fini, Ann. Sci. Math. Québec 7(1983)39–57.
J.A. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles (1968).
S.C. Kleene, Representation of events in nerve nets and finite automata, in:Automata Studies, eds. C.E. Shannon and J. McCarthy (Princeton University Press, Princeton, NJ, 1956) pp. 3–42.
N. Immerman, Languages that capture complexity classes, SIAM J. Comput. 16(1987)760–778.
N. Immerman, Nondeterministic space is closed under complement, SIAM J. Comput. 17(1988)935–938.
J. Justin and G. Pirillo, On a natural extension of Jacob's rank, J. Combin. Theory 43(1986)205–218.
R. Ladner, Application of model theoretic games to discrete linear orders and finite automata, Inform. Contr. 33(1977)281–303.
G. Lallement,Semigroups and Combinatorial Applications (Wiley, New York, 1979).
H. Landweber, Finite state games — a solvability algorithm for restricted second-order arithmetic, Notices Amer. Math. Soc. 14(1967)129–130.
H. Landweber, Decision problems for ω-automata, Math. Syst. Theor. 3(1969)376–384.
R. McNaughton, Testing and generating infinite sequences by a finite automaton, Inform. Contr. 9(1966)521–530.
R. McNaughton, Algebraic decision procedures for local testability, Math. Syst. Theor. 8(1974)60–76.
R. McNaughton and S. Pappert,Counter-free Automata (MIT Press, 1971).
A.R. Meyer, Weak monadic second order theory of successor is not elementary recursive,Proc. Boston University Logic Colloquium, Lecture Notes in Mathematics 453 (Springer, Berlin/Heidelberg/New York, 1975) pp. 132–154.
C. Michaux and F. Point, Les ensemblesk-reconnaissables sont définissables dans (ℕ, +,V k ), C.R. Acad. Sci. Paris 303(1986)939–942.
M. Nivat and D. Perrin, Ensembles reconnaissables de mots biinfinis, Can. J. Math 38(1986)513–537.
J.P. Pécuchet, Variétés de semigroupes et mots infinis,STACS 86, eds. B. Monien and G. Vidal-Naquet, Lecture Notes in Computer Science 210 (Springer, 1986) pp. 180–191.
J.P. Pécuchet, Etude syntaxique des parties reconnaissables de mots infinis,Proc. 13th ICALP, ed. L. Kott, Lecture Notes in Computer Science 226 (1986) pp. 294–303.
D. Perrin, Variétés de semigroupes et mots infinis, C.R. Acad. Sci. Paris 295(1982)595–598.
D. Perrin, Recent results on automata and infinite words, in:Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 176 (Springer, New York/Berlin, 1984) pp. 134–148.
D. Perrin, An introduction to automata on infinite words, in:Automata on Infinite Words, ed. M. Nivat, Lecture Notes in Computer Science 192 (Springer, 1984) pp. 2–17.
D. Perrin, Automata, in:Handbook of Theoretical Computer Science, ed. J. Van Leeuwen, Vol. B:Formal Models and Semantics (Elsevier, 1990) chap. 1.
D. Perrin and J.E. Pin, First order logic and star-free sets, J. Comput. Syst. Sci. 32(1986)393–406.
D. Perrin and J.E. Pin, Mots infinis, LITP Report 93-40, to appear.
D. Perrin and P.E. Schupp, Automata on the integers, recurrence distinguishability and the equivalence and decidability of monadic theories,Proc. 1st IEEE Symp. on Logic in Computer Science (1986) pp. 301–304.
J.-E. Pin, Hiérarchies de concaténation, RAIRO Inform. Théor. 18(1984)23–46.
J.-E. Pin,Variétés de Langages Formels (Masson, Paris, 1984); English translation:Varieties of Formal Languages (Plenum, New York, 1986).
J.-E. Pin and H. Straubing, Monoids of upper triangular matrices,Colloquia Mathematica Societatis Janos Bolyai 39 (Semigroups, Szeged, 1981) pp. 259–272.
J.-E. Pin and P. Weil, Polynomial closure and unambiguous products,Proc. 22nd ICALP, Lecture Notes in Computer Science 944 (Springer, Berlin, 1995) pp. 348–359.
W.V. Quine, Concatenation as a basis for arithmetic, J. Symb. Logic 11(1946)105–114.
F.D. Ramsey, On a problem of formal logic, Proc. London Math. Soc. 30(1929)338–384.
M.P. Schützenberger, On finite monoids having only trivial subgroups, Inform. Contr. 8(1965)190–194.
A.L. Semenov, On certain extensions of the arithmetic of addition of natural numbers, Math. USSR Izvestiya 15(1980)401–418.
D. Siefkes, Büchi's monadic second order successor arithmetic, Lecture Notes in Math. 120 (Springer, Berlin, 1970).
I. Simon, Piecewise testable events,Proc. 2nd GI Conf., Lecture Notes in Computer Science 33 (Springer, Berlin, 1975) pp. 214–222.
I. Simon, Factorization forests of finite height, Theor. Comput. Sci. 72(1990)65–94.
J. Stern, Characterization of some classes of regular events, Theor. Comput. Sci. 35(1985)17–42.
J. Stern, Complexity of some problems from the theory of automata, Inform. Contr. 66(1985)163–176.
L. Stockmeyer, The polynomial time hierarchy, Theor. Comput. Sci. 3(1977)1–22.
L.J. Stockmeyer and A.R. Meyer, Word problems requiring exponential time: Preliminary report,Proc. 5th Annual ACM Symposium on the Theory of Computing (1977) pp. 1–9.
H. Straubing, Aperiodic homomorphisms and the concatenation product of recognizable sets, J. Pure Appl. Algebra 15(1979)319–327.
H. Straubing, Semigroups and languages of dot-depth two, Theor. Comput. Sci. 58(1988)361–378.
H. Straubing and D. Thérien, Partially ordered finite monoids and a theorem of I. Simon, J. Algebra 119(1985)393–399.
H. Straubing, D. Thérien and W. Thomas, Regular languages defined with generalized quantifiers,Proc. 15th ICALP, Lecture Notes in Computer Science 317 (Springer, 1988) pp. 561–575.
H. Straubing and P. Weil, On a conjecture concerning dot-depth two languages, Theor. Comput. Sci. 104(1992)161–183.
R. Szelepcsényi, The method of forced enumeration for nondeterministic automata, Acta Informatica 26(1988)279–284.
D. Thérien and A. Weiss, Graph congruences and wreath products, J. Pure Appl. Algebra 35(1985)205–215.
W. Thomas, Star-free regular sets of ω-sequences, Inform. Contr. 42(1979)148–156.
W. Thomas, A combinatorial approach to the theory of ω-automata, Inform. Contr. 48(1981)261–283.
W. Thomas, Classifying regular events in symbolic logic, J. Comput. Syst. Sci. 25(1982)360–375.
W. Thomas, Automata on infinite objects, in:Handbook of Theoretical Computer Science, Vol. B:Formal Models and Semantics (Elsevier, 1990) pp. 135–191.
W. Thomas, On logics, tilings, and automata,Proc. 18th ICALP, Madrid, eds. J. Leach Albert et al., Lecture Notes in Computer Science 510 (Springer, Berlin, 1991) pp. 441–454.
W. Thomas, On the Ehrenfeucht-Fraïssé game in theoretical computer science,TAPSOFT '93, eds. M.C. Gaudel and J.P. Jouannaud, Lecture Notes in Computer Science 668 (Springer, Berlin, 1993) pp. 559–568.
P. Weil, Inverse monoids and the dot-depth hierarchy, Ph.D. Dissertation, University of Nebraska, Lincoln (1988).
P. Weil, Inverse monoids of dot-depth two, Theor. Comput. Sci. 66(1989)233–245.
P. Weil, Some results on the dot-depth hierarchy, Semigroup Forum 46(1993)352–370.
T. Wilke, An Eilenberg theorem for ∞-languages, automata, languages and programming,Proc. 18th ICALP Conf., Lecture Notes in Computer Science 510 (Springer, Berlin, 1991) pp. 588–599.
Th. Wilke, An algebraic theory for regular languages of finite and infinite words, Int. J. Algebra Comput. 3(1993)447–489.
Th. Wilke, Locally threshold testable languages of infinite words,STACS 93, eds. P. Enjalbert, A. Finkel and K.W. Wagner, Lecture Notes in Computer Science 665 (Springer, Berlin, 1993) pp. 607–616.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Pin, JE. Logic, semigroups and automata on words. Ann Math Artif Intell 16, 343–384 (1996). https://doi.org/10.1007/BF02127803
Issue Date:
DOI: https://doi.org/10.1007/BF02127803