zbMATH — the first resource for mathematics

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.

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)
Full Text: DOI
[1] Arnold, A.; Arnold, A., Systèmes de transitions finis et sémantique des processus communicants, (), (1992), Masson Paris, English translation
[2] Arnold, A.; Niwinski, D., Fixed-point characterization of weak monadic logic definable sets of trees, (), 159-188 · Zbl 0794.03054
[3] Courcelle, B.; Courcelle, B., A representation or trees by languages, Theoret. comput. sci., 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., to appear. · 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 ECTL∗ as fragments of the modal μ-calculus, Theoret. comput. sci., 126, 77-96, (1994) · Zbl 0798.03018
[13] Emerson, A., Temporal and modal logics, (), 995-1072 · Zbl 0900.03030
[14] Gallier, J.; Gallier, J., DPDAS’s in atomic normal form and applications to equivalence problems, Theoret. comput. sci., Corrigendum, 19, 229-186, (1982) · Zbl 0483.68048
[15] Gecseg, F.; Steinby, M., Tree automata, (1984), Academie Kiado Budapest · Zbl 0396.68041
[16] Hopcroft, J.; Ullman, J., Introduction to automata theory, languages and computation, (1990), 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, (), 464-473
[19] Niwinski, D., Fixed points vs. infinite generation, (), 402-409
[20] Rabin, M., A simple method for undecidability proofs and some applications, (), 58-68
[21] Thomas, W., Automata on infinite objects, (), 133-192 · Zbl 0900.68316
[22] Thomas, W., On logics, tillings and automata, (), 441-454 · 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. 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.