Abstract
ω-automata are finite state automata that accept infinite strings. The class of ω-regular languages is exactly the set accepted by nondeterministic Buchi and L- automata, and deterministic Müller, Rabin, and Streett automata. The languages accepted by deterministic Buchi automata (DBA) form a strict subset of the class of ω-regular languages. Landweber characterized deterministic Ω-automata whose languages are realizable by DBA. We provide an alternative proof of Landweber's theorem and give polynomial time algorithms to check if a language ℒ specified as a deterministic Muller, L-, Streett, or Rabin automaton can be realized as a DBA. We identify a sub-class of deterministic Müller, L-, Streett, and Rabin automata, called Buchi-type automata, which can be converted to an equivalent DBA on the same transition structure in polynomial time. For this subset of Ω-automata, our transformation yields the most efficient algorithms for checking language inclusion-important for computer verification of reactive systems. We prove that a deterministic L- (DLA) or Rabin automaton (DRA), unlike deterministic Muller or Streett automata, is Buchi-type if and only if its language is realizable as a DBA. Therefore, for languages that are realizable as DBA, DBA are as compact as DRA or DLA.
supported by DARPA grant JFBI90-073, Fujitsu, and California MICRO program
supported NSF grant ECS 9111907 and California PATH program
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B.Alpern and F.B. Schneider. Recognizing Safety and Liveness. Distributed Computing, 2(3):117–126, 1987.
E. A. Emerson and C. L. Lei. Modalities for Model Checking: Branching Time Logic Strikes Back. Science of Computer Programming, 8(3):275–306, June 1987.
A. Aziz et al. HSIS: A BDD-Based Environment for Formal Verification. In Proc. of the Design Automation Conf., 1994. To Appear.
S. C. Krishnan, A. Puri, and R. K. Brayton. Deterministic Ω-automata vis-a-vis Deterministic Buchi Automata. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720. preprint.
R. P. Kurshan. Complementing Deterministic Büchi Automata in Polynomial Time. Journal of Computer and System Sciences, 35:59–71, 1987.
R. P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, 1993. To appear.
M.O. Rabin and D.Scott. Finite Automata and their Decision Problems. In IBM Journal of Research and Development, volume 3, pages 115–125, 1959.
Shmuel Safra. Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel, March 1989.
W. Thomas. Automata on Infinite Objects. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 133–191. Elsevier Science, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krishnan, S.C., Puri, A., Brayton, R.K. (1994). Deterministic Ω automata vis-a-vis deterministic Buchi automata. In: Du, DZ., Zhang, XS. (eds) Algorithms and Computation. ISAAC 1994. Lecture Notes in Computer Science, vol 834. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58325-4_202
Download citation
DOI: https://doi.org/10.1007/3-540-58325-4_202
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58325-7
Online ISBN: 978-3-540-48653-4
eBook Packages: Springer Book Archive