Automata; Emptiness Test; Linear Orderings; Rational Domain; Reachability; Real Domain
Abstract :
[en] Automata have been defined to recognize languages of words indexed by linear orderings, which generalize the usual notions of finite, infinite, and ordinal words. The reachability problem for these automata has already been solved for scattered linear orderings. In this paper, we design an analogous procedure that solves reachability over the specific domains R and Q. Given an automaton on linear orderings, this procedure decides in polynomial time whether this automaton accepts at least one word indexed by R or by Q. We claim that this algorithm constitutes an essential step to designing effective decision procedures for the first-order monadic theory of order interpreted over R or Q.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Informatique
Fontaine, Pascal ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Systèmes informatiques distribués
Vergain, Baptiste ; Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science
Language :
English
Title :
Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals
Publication date :
03 September 2024
Event name :
28th International Conference, CIAA 2024, Akita, Japan, September 3–6, 2024
Event place :
Akita, Japan
Event date :
03-09-2024 => 06-09-2024
Audience :
International
Main work title :
Implementation and Application of Automata - 28th International Conference, CIAA 2024, Proceedings
Editor :
Fazekas, Szilárd Zsolt
Publisher :
Springer Science and Business Media Deutschland GmbH
Bedon, N., Bès, A., Carton, O., Rispal, C.: Logic and rational languages of words indexed by linear orderings. Theory Comput. Syst. 46, 737–760 (2010)
Bès, A., Carton, O.: A Kleene theorem for languages of words indexed by linear orderings. Int. J. Found. Comput. Sci. 17(03), 519–541 (2006)
Bruyère, V., Carton, O.: Automata on linear orderings. J. Comput. Syst. Sci. 73(1), 1–24 (2007)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, 1960 (1962)
Büchi, J.R.: Transfinite automata recursions and weak second order theory of ordinals. In: Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science, 1965 (1965)
Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic 26(2), 115–128 (1985)
Cantor, G.: Über unendliche, lineare Punktmannichfaltigkeiten. Math. Ann. 20(1), 113–121 (1882)
Cantor, G.: Beiträge zur Begründung der transfiniten Mengenlehre. Math. Ann. 46, 481–512 (1895)
Carton, O.: Accessibility in automata on scattered linear orderings. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 155–164. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45687-2_12
Choueka, Y.: Finite automata, definable sets, and regular expressions over \(\omega ^n\)-tapes. J. Comput. Syst. Sci. 17(1), 81–97 (1978)
Cristau, J.: Automata and temporal logic over arbitrary linear time. In: Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science. LIPIcs, vol. 4, pp. 133–144 (2009)
DiBenedetto, E.: Real Analysis. Springer, Cham (2002)
Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fundam. Math. 59(1), 109–116 (1966)
Muller, D.E.: Infinite sequences and finite machines. In: Proceedings of the Annual Symposium on Switching Circuit Theory and Logical Design, pp. 3–16. IEEE Computer Society (1963)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)
Rabinovich, A.: Temporal logics over linear time domains are in PSPACE. Inf. Comput. 210, 40–67 (2012)
Reynolds, M.: The complexity of temporal logic over the reals. Ann. Pure Appl. Logic 161(8), 1063–1096 (2010)
Rosenstein, J.G.: Linear Orderings. Academic Press, Cambridge (1982)
Shelah, S.: The monadic theory of order. Ann. Math. 102(3), 379–419 (1975)
