Abstract
We introduce partially ordered two-way Büchi automata over infinite words. As for finite words, the nondeterministic variant recognizes the fragment Σ2 of first-order logic FO[<] and the deterministic version yields the Δ2-definable ω-languages. As a byproduct of our results, we show that deterministic partially ordered two-way Büchi automata are effectively closed under Boolean operations.
In addition, we have coNP-completeness results for the emptiness problem and the inclusion problem over deterministic partially ordered two-way Büchi automata.
This work was supported by the German Research Foundation (DFG), grant DI 435/5-1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proc. Int. Congr. for Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford Univ. Press, Stanford (1962)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Diekert, V., Kufleitner, M.: Fragments of first-order logic over infinite words. In: STACS 2009. Dagstuhl Seminar Proceedings, vol. 09001, pp. 325–336 (2009)
Kapoutsis, C.A.: Removing bidirectionality from nondeterministic finite automata. In: Jedrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 544–555. Springer, Heidelberg (2005)
Kufleitner, M., Lauser, A.: Partially ordered two-way Büchi automata. Technical report no. 2010/03, Universität Stuttgart, Informatik (2010)
Kupferman, O., Piterman, N., Vardi, M.Y.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 519–535. Springer, Heidelberg (2001)
Lodaya, K., Pandya, P.K., Shah, S.S.: Marking the chops: An unambiguous temporal logic. IFIP TCS 273, 461–476 (2008)
Lodaya, K., Pandya, P.K., Shah, S.S.: Around dot depth two. In: Gao, Y., Lu, H., Seki, S., Yu, S. (eds.) DLT 2010. LNCS, vol. 6224, pp. 305–316. Springer, Heidelberg (2010)
Pécuchet, J.-P.: Automates boustrophédon et mots infinis. Theoretical Computer Science 35, 115–122 (1985)
Pin, J.-É., Weil, P.: Polynomial closure and unambiguous product. Theory of Computing Systems 30(4), 383–422 (1997)
Schwentick, T., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 239–250. Springer, Heidelberg (2002)
Sistla, A.P., Vardi, M.Y., Wolper, P.L.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49(2-3), 217–237 (1987)
Thérien, D., Wilke, T.: Over words, two variables are as powerful as one quantifier alternation. In: STOC 1998, pp. 234–240 (1998)
Thomas, W.: Classifying regular events in symbolic logic. Journal of Computer and System Sciences 25, 360–376 (1982)
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kufleitner, M., Lauser, A. (2011). Partially Ordered Two-Way Büchi Automata. In: Domaratzki, M., Salomaa, K. (eds) Implementation and Application of Automata. CIAA 2010. Lecture Notes in Computer Science, vol 6482. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18098-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-18098-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18097-2
Online ISBN: 978-3-642-18098-9
eBook Packages: Computer ScienceComputer Science (R0)