×

The monadic second-order logic of graphs. IX: Machines and their behaviours. (English) Zbl 0872.03026

Summary: For the previous parts see [Zbl 0722.03008; Zbl 0694.68043; Zbl 0754.03006; Zbl 0731.03006; Zbl 0754.68065; Zbl 0809.03005; Zbl 0831.03001; Zbl 0809.03006; Zbl 0830.03016].
We establish that every monadic second-order property of the behaviour of a machine (transition systems and tree automata are typical examples of machines) is a monadic second-order property of the machine itself. In this way, we clarify the distinction between “dynamic” properties of machines (i.e., properties of their behaviours), and their “static” properties (i.e., properties of the graphs or relational structures representing them). It is important for program verification that the dynamic properties that one wants to verify can be formulated statically, in the simplest possible way. As a corollary of our main result, we also obtain that the monadic theory of an algebraic tree is decidable.

MSC:

03D05 Automata and formal grammars in connection with logical questions
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68R10 Graph theory (including graph drawing) in computer science
03B25 Decidability of theories and sets of sentences
03B15 Higher-order logic; type theory (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arnold, A., Systèmes de transitions finis et sémantique des processus communicants, (Finite Transition Systems (1994), Prentice Hall: Prentice Hall Englewood Cliffs, NJ), English translation
[2] Arnold, A.; Niwinski, D., Fixed-point characterization of weak monadic logic definable sets of trees, (Nivat, M.; Podelski, A., Tree Automata and Languages (1992), Elsevier: Elsevier Amsterdam), 159-188 · Zbl 0794.03054
[3] Courcelle, B., A representation or trees by languages, Theoret. Comput. Sci., 7, 25-55 (1978) · Zbl 0428.68088
[4] Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013
[5] Courcelle, B., Equivalences and transformations of regular systems, Theoret. Comput. Sci., 42, 1-122 (1986) · Zbl 0636.68104
[6] Courcelle, B., The monadic second-order logic of graphs II: Infinite graphs of bounded width, Math. Systems Theory, 21, 187-222 (1989) · Zbl 0694.68043
[7] Courcelle, B., The monadic second-order logic of graphs I: Recognizable sets of finite graphs, Inform. and Comput., 85, 12-75 (1990) · Zbl 0722.03008
[8] Courcelle, B., The monadic second-order logic of graphs IV: Definability properties of equational graphs, Ann. Pure Appl. Logic, 49, 193-255 (1990) · Zbl 0731.03006
[9] B. Courcelle, The monadic second-order logic of graphs X: Linear orders, Theoret. Comput. Sci.; B. Courcelle, The monadic second-order logic of graphs X: Linear orders, Theoret. Comput. Sci. · Zbl 0877.68087
[10] Courcelle, B., Monadic second order graph transductions: A survey, Theoret. Comput. Sci., 126, 53-75 (1994) · Zbl 0805.68077
[11] Courcelle, B.; Walukiewicz, I., Coverings of graphs, behaviours of transition systems and monadic second-order logic (October 1994), manuscript
[12] Dam, M., \(CTL^∗\) and E \(CTL^∗\) as fragments of the modal μ-calculus, Theoret. Comput. Sci., 126, 77-96 (1994) · Zbl 0798.03018
[13] Emerson, A., Temporal and modal logics, (Van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 995-1072 · Zbl 0900.03030
[14] Gallier, J., Corrigendum, 19, 229 (1982) · Zbl 0483.68048
[15] Gecseg, F.; Steinby, M., Tree Automata (1984), Academie Kiado: Academie Kiado Budapest · Zbl 0396.68041
[16] Hopcroft, J.; Ullman, J., Introduction to Automata Theory, Languages and Computation (1990), Addison-Wesley: Addison-Wesley Reading, MA
[17] Mezei, J.; Wright, J., Algebraic automata and context-free sets, Inform. and Control, 11, 3-29 (1967) · Zbl 0155.34301
[18] Niwinski, D., On fixed point clones, (Proc 13th ICALP. Proc 13th ICALP, Lecture Notes in Computer Science, Vol. 226 (1986), Springer: Springer Berlin), 464-473
[19] Niwinski, D., Fixed points vs. infinite generation, (Proc
[20] Rabin, M., A simple method for undecidability proofs and some applications, (Bar-Hillel, Y., Logic, Methodology and Philisophy of Science II (1965), North-Holland: North-Holland Amsterdam), 58-68 · Zbl 0192.05502
[21] Thomas, W., Automata on infinite objects, (Van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 133-192 · Zbl 0900.68316
[22] Thomas, W., On logics, tillings and automata, (Proc. · Zbl 0769.68100
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.