Abstract
We introduce and study three notions of typeness for automata on infinite words. For an acceptance-condition class γ (that is, γ is weak, Büchi, co-Büchi, Rabin, or Streett), deterministic γ -typeness asks for the existence of an equivalent γ-automaton on the same deterministic structure, nondeterministic γ-typeness asks for the existence of an equivalent γ-automaton on the same structure, and γ-powerset-typeness asks for the existence of an equivalent γ-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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador- Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic:A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Boigelot, B., Jodogne, S., Wolper, P.: Onthe use of weak automata for deciding linear arithmetic with integer and real variables. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 611–625. Springer, Heidelberg (2001)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pp. 1–12. Stanford University Press, Stanford (1962)
Kaminski, M.: A classification of ω-regular languages. Theoretical Computer Science 36, 217–229 (1985)
Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ω-automata vis-a-vis deterministic Büchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)
Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: from lineartime to branching-time. In: Proc. 13th IEEE Symp. on Logic in Computer Science, June 1998, pp. 81–92 (1998)
Kupferman, O., Vardi, M.Y.: Relating linear and branching model checking. In: IFIPWorking Conference on Programming Concepts and Methods, NewYork, June 1998, pp. 304–326. Chapman & Hall, Boca Raton (1998)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)
Landweber, L.H.: Decision problems for ω–automata. Mathematical Systems Theory 3, 376–384 (1969)
Löding, C.: Optimal bounds for the transformation of omega-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)
McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9, 521–530 (1966)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Michel, M.: Complementation is more difficult with automata on infinitewords. In: CNET, Paris (1988)
Maler, O., Staiger, L.: On syntactic congruences for ω-languages. Theoretical Computer Science 183(1), 93–112 (1997)
Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, Springer, Heidelberg (1986)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)
Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, White Plains, October 1988, pp. 319–327 (1988)
Safra, S., Vardi, M.Y.: On ω-automata and temporal logic. In: Proc. 21st ACMSymp. on Theory of Computing, Seattle, May 1989, pp. 127–137 (1989)
Thomas, W.: Automata on infinite objects. Handbook of Theoretical Computer Science, pp. 165–191 (1990)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 332–344 (1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Morgenstern, G., Murano, A. (2004). Typeness for ω-Regular Automata. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive