×

On infinite transition graphs having a decidable monadic theory. (English) Zbl 1019.68066

Summary: We define a family of graphs whose monadic theory is (in linear space) reducible to the monadic theory S2S of the complete ordered binary tree. This family contains strictly the context-free graphs investigated by Muller and Schupp, and also the equational graphs defined by Courcelle. Using words as representations of vertices, we give a complete set of representatives by prefix rewriting of rational languages. This subset of possible representatives is a boolean algebra preserved by transitive closure of arcs and by rational restriction on vertices.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] L. Boasson, M. Nivat, Centers of context-free languages, Internal Report LITP 84-44, 1984.; L. Boasson, M. Nivat, Centers of context-free languages, Internal Report LITP 84-44, 1984. · Zbl 0457.68082
[2] R. Büchi, Regular canonical systems, Archiv für Mathematische Logik und Grundlagenforschung 6 (1964) 91-111 [reprinted in: S. Mac Lane, D. Siefkes (Eds.), The collected works of J. Richard Büchi, Springer, New York, 1990, pp. 317-337].; R. Büchi, Regular canonical systems, Archiv für Mathematische Logik und Grundlagenforschung 6 (1964) 91-111 [reprinted in: S. Mac Lane, D. Siefkes (Eds.), The collected works of J. Richard Büchi, Springer, New York, 1990, pp. 317-337]. · Zbl 0129.26102
[3] D. Caucal, On the regular structure of prefix rewriting, CAAP 90, in: A. Arnold (Ed.), Lecture Notes in Computer Science, Vol. 431, Springer, Berlin, 1990, pp. 87-102 [a full version is in Theoret. Comput. Sci. 106 (1992) 61-86].; D. Caucal, On the regular structure of prefix rewriting, CAAP 90, in: A. Arnold (Ed.), Lecture Notes in Computer Science, Vol. 431, Springer, Berlin, 1990, pp. 87-102 [a full version is in Theoret. Comput. Sci. 106 (1992) 61-86]. · Zbl 0786.68047
[4] D. Caucal, Monadic theory of term rewritings, 7th IEEE Symposium, LICS 92, 1992, pp. 266-273.; D. Caucal, Monadic theory of term rewritings, 7th IEEE Symposium, LICS 92, 1992, pp. 266-273.
[5] D. Caucal, Bisimulation of context-free grammars and of pushdown automata, in: A. Ponse, M. de Rijke, Y. Venema (Eds.), CSLI Vol. 53, Modal Logic and Process Algebra, Stanford, 1995, pp. 85-106.; D. Caucal, Bisimulation of context-free grammars and of pushdown automata, in: A. Ponse, M. de Rijke, Y. Venema (Eds.), CSLI Vol. 53, Modal Logic and Process Algebra, Stanford, 1995, pp. 85-106.
[6] Courcelle, B., Graph rewriting: an algebraic and logic approach, (Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 193-242 · Zbl 0900.68282
[7] Courcelle, B., Monadic second-order definable graph transductionsa survey, Theoret. Comput. Sci., 126, 53-75 (1994) · Zbl 0805.68077
[8] Courcelle, B.; Walukiewicz, I., Monadic second-order logic, graph coverings and unfolding of transition systems, Ann. Pure Appl. Logic, 1, 35-62 (1998) · Zbl 0929.03036
[9] Muller, D.; Schupp, P., The theory of ends, pushdown automata, and second-order logic, Theoret. Comput. Sci., 37, 51-75 (1985) · Zbl 0605.03005
[10] Rabin, M., A simple method for undecidability proofs and some applications, (Bar-Hillel, Y., Logic, Methodology and Philosophy of Science (1965), North-Holland), 58-68 · Zbl 0192.05502
[11] Rabin, M., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031
[12] Semenov, A., Decidability of monadic theories, MFCS 84, (Goos, G.; Hartmanis, J., Lecture Notes in Computer Science, Vol. 176 (1984), Springer: Springer Berlin), 162-175
[13] Sénizergues, G., Formal languages and word-rewriting, (Comon, H.; Jouannaud, J.-P., French Sring School of Theoretical Computer Science. French Sring School of Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 909 (1975), Springer: Springer Berlin), 75-94
[14] Shelah, S., The monadic theory of order, Ann. Math., 102, 379-419 (1975) · Zbl 0345.02034
[15] J. Stupp, The lattice-model is recursive in the original model, Manuscript, The Hebrew University, 1975.; J. Stupp, The lattice-model is recursive in the original model, Manuscript, The Hebrew University, 1975.
[16] Thomas, W., Automata on infinite objects, (Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 135-191 · Zbl 0900.68316
[17] Thomas, W., On logics, tilings, and automata, ICALP 91, (Albert, L.; Monien, B.; Artalejo, R., Lecture Notes in Computer Science, Vol. 510 (1991), Springer: Springer Berlin), 191-231
[18] Thomas, W., Languages, automata, and logic, (Rozenberg, G.; Salomaa, A., Handbook of Formal Languages, Vol. 3 (1997), Springer: Springer Berlin), 389-456
[19] D. Caucal, On the transition graphs of Turing machines, MCU 2001, in: M. Margenstern, Y. Rogozhin (Eds.), Lecture Notes in Computer Sciences, Vol. 2055, pp. 177-189, a long version will appear in Theoret. Comput. Sci.; D. Caucal, On the transition graphs of Turing machines, MCU 2001, in: M. Margenstern, Y. Rogozhin (Eds.), Lecture Notes in Computer Sciences, Vol. 2055, pp. 177-189, a long version will appear in Theoret. Comput. Sci. · Zbl 0984.68073
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.