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
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
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)
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.
