k-counting automata
Allred, Joël ; Ultes-Nitsche, Ulrich
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012), p. 461-478 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)

In this paper, we define k-counting automata as recognizers for ω-languages, i.e. languages of infinite words. We prove that the class of ω-languages they recognize is a proper extension of the ω-regular languages. In addition we prove that languages recognized by k-counting automata are closed under Boolean operations. It remains an open problem whether or not emptiness is decidable for k-counting automata. However, we conjecture strongly that it is decidable and give formal reasons why we believe so.

Publié le : 2012-01-01
DOI : https://doi.org/10.1051/ita/2012021
Classification:  68Q45,  20F10 
@article{ITA_2012__46_4_461_0,
     author = {Allred, Jo\"el and Ultes-Nitsche, Ulrich},
     title = {$k$-counting automata},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {46},
     year = {2012},
     pages = {461-478},
     doi = {10.1051/ita/2012021},
     zbl = {1279.68126},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_2012__46_4_461_0}
}

Allred, Joël; Ultes-Nitsche, Ulrich. $k$-counting automata. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) pp. 461-478. doi : 10.1051/ita/2012021. http://gdmltest.u-ga.fr/item/ITA_2012__46_4_461_0/

[1] B. Alpern and F.B. Schneider, Defining liveness. Inf. Process. Lett. 21 (1985) 181-185. | MR 815216 | Zbl 0575.68030

[2] M. Bojanczyk, Beyond ω-regular languages, in Proc. STACS, LIPIcs, edited by J.-Y. Marion and T. Schwentick. Schloss Dagstuhl - Leibniz-Zentrum für Informatik 5 (2010) 11-16. | MR 2853905 | Zbl 1230.68124

[3] M. Bojanczyk and T. Colcombet, Boundedness in languages of infinite words. Unpublished manuscript. Extended version of M. Bojanczyk and T. Colcombet, Bounds in ω-Regularity, in LICS (2006) 285-296.

[4] M. Bojańczyk, C. David, A. Muscholl, T. Schwentick and L. Segoufin, Two-variable logic on data words. ACM Trans. Comput. Logic 12 (2011) 27 :1-27 :26. | MR 2820102

[5] J.R. Büchi, On a decision method in restricted second order arithmetic, in Proc. of the International Congress on Logic, Methodology and Philosophy of Science 1960, edited by E. Nagel et al. Stanford University Press (1962) 1-11. | MR 183636 | Zbl 0147.25103

[6] H. Fernau and R. Stiebe, Blind counter automata on ω-words. Fundam. Inform. 83 (2008) 51-64. | MR 2389126 | Zbl 1147.68038

[7] P.C. Fischer, Turing machines with restricted memory access. Inf. Control 9 (1966) 364-379. | MR 199061 | Zbl 0145.24205

[8] K. Hashiguchi, Algorithms for determining relative star height and star height. Inf. Comput. 78 (1988) 124-169. | MR 955580 | Zbl 0668.68081

[9] J.E. Hopcroft, R. Motwani and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison Wesley, Pearson Education (2006). | MR 645539 | Zbl 0426.68001

[10] R.M. Karp and R.E. Miller, Parallel program schemata. J. Comput. Syst. Sci. 3 (1969) 147-195. | MR 246720 | Zbl 0198.32603

[11] R.P. Kurshan, Computer-Aided Verification of Coordinating Processes, 1st edition. Princeton University Press, Princeton, New Jersey (1994). | MR 1313501 | Zbl 0822.68116

[12] E.W. Mayr, An algorithm for the general petri net reachability problem, in Proc of the 13th Annual ACM Symposium on Theory of Computing, STOC'81. New York, USA, ACM (1981) 238-246. | Zbl 0563.68057

[13] R. Mcnaughton, Testing and generating infinite sequences by a finite automaton. Inf. Control 9 (1966) 521-530. | MR 213241 | Zbl 0212.33902

[14] M.L. Minsky, Recursive unsolvability of post's problem of “tag” and other topics in theory of turing machines. Ann. Math. 74 (1961) 437-455. | MR 140405 | Zbl 0105.00802

[15] D.E. Muller, Infinite sequences and infinite machines, in AIEE Proc. of the 4th Annual Symposium on Switching Theory and Logical Design (1963) 3-16.

[16] C.A. Petri, Kommunikation mit Automaten. Ph.D. thesis, Rheinisch-Westfälisches Institut für instrumentelle Mathematik an der Universität Bonn (1962). | MR 158806

[17] H.G. Rice, Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc. 74 (1953) 358-366. | MR 53041 | Zbl 0053.00301

[18] W. Thomas, Automata on infinite objects, in Formal Models and Semantics, edited by J. van Leeuwen. Handbook of Theoret. Comput. Sci. B (1990) 133-191. | MR 1127189 | Zbl 0900.68316

[19] U. Ultes-Nitsche, A power-set construction for reducing Büchi automata to non-determinism degree two. Inform. Process. Lett. 101 (2007) 107-111. | MR 2287328 | Zbl 1185.68402

[20] U. Ultes-Nitsche and S.St. James, Improved verification of linear-time properties within fairness - weakly continuation-closed behaviour abstractions computed from trace reductions. Software Testing, Verification and Reliability 13 (2003) 241-255.

[21] M.Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, in Proc. of the 1st Symposium on Logic in Computer Science. Cambridge (1986).

[22] M.Y. Vardi and P. Wolper, Reasoning about infinite computations. Inform. Comput. 115 (1994) 1-37. | MR 1303019 | Zbl 0827.03009