×

Typeness for \(\omega\)-regular automata. (English) Zbl 1098.68073

Summary: We introduce and study three notions of typeness for automata on infinite words. For an acceptance-condition class \(\gamma\) (that is, \(\gamma\) is weak, Büchi, co-Büchi, Rabin, or Streett), deterministic \(\gamma\)-typeness asks for the existence of an equivalent \(\gamma\)-automaton on the same deterministic structure, nondeterministic \(\gamma\)-typeness asks for the existence of an equivalent \(\gamma\)-automaton on the same structure, and \(\gamma\)-powerset-typeness asks for the existence of an equivalent \(\gamma\)-automaton on the (deterministic) powerset structure–one obtained by applying the subset construction. The notions are helpful in studying the complexity and complication of translations between the various classes of automata. For example, we prove that deterministic Büchi automata are co-Büchi type; it follows that a translation from deterministic Büchi to deterministic co-Büchi automata, when exists, involves no blow up. On the other hand, we prove that nondeterministic Büchi automata are not co-Büchi type; it follows that a translation from a nondeterministic Büchi to nondeterministic co-Büchi automata, when exists, should be more complicated than just redefining the acceptance condition. As a third example, by proving that nondeterministic co-Büchi automata are Büchi-powerset type, we show that a translation of nondeterministic co-Büchi to deterministic Büchi automata, when exists, can be done applying the subset construction. We give a complete picture of typeness for the weak, Büchi, co-Büchi, Rabin, and Streett acceptance conditions, and discuss its usefulness.

MSC:

68Q45 Formal languages and automata
Full Text: DOI

References:

[1] DOI: 10.1016/0304-3975(85)90043-X · Zbl 0565.68076 · doi:10.1016/0304-3975(85)90043-X
[2] DOI: 10.1007/3-540-58325-4_202 · doi:10.1007/3-540-58325-4_202
[3] DOI: 10.1145/1055686.1055689 · Zbl 1367.68195 · doi:10.1145/1055686.1055689
[4] DOI: 10.1145/333979.333987 · Zbl 1133.68376 · doi:10.1145/333979.333987
[5] Kurshan R. P., Computer Aided Verification of Coordinating Processes (1994) · Zbl 0822.68116
[6] DOI: 10.1007/BF01691063 · Zbl 0182.02402 · doi:10.1007/BF01691063
[7] DOI: 10.1016/S0304-3975(96)00312-X · Zbl 0911.68145 · doi:10.1016/S0304-3975(96)00312-X
[8] DOI: 10.1016/S0019-9958(66)80013-X · Zbl 0212.33902 · doi:10.1016/S0019-9958(66)80013-X
[9] DOI: 10.1016/0304-3975(84)90049-5 · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5
[10] Rabin M. O., Transaction of the AMS 141 pp 1–
[11] Rabin M. O., IBM Journal of Research and Development 3 pp 115–
[12] W. Thomas, Handbook of Theoretical Computer Science (1990) pp. 165–191.
[13] DOI: 10.1006/inco.1994.1092 · Zbl 0827.03009 · doi:10.1006/inco.1994.1092
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.