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.
This is a preview of subscription content, log in via an institution to check access.
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)