Current Science

Open Access Open Access  Restricted Access Subscription Access

Omega Automata and its Classes


Affiliations
1 Thapar Institute of Engineering and Technology, Patiala 147 003, India
 

ω-automata is a variant of finite automata which accepts infinite strings. It represents the behaviour of the infinite systems (hardware, operating system and control systems) which are not expected to end. A variety of conditions are used to represent the set of accepting strings in ω-automata. This paper summarizes various types of ω-automata, their transition functions and accepting conditions. In addition, this paper also summarizes the applicability of omega automata in various interdisciplinary fields.

Keywords

Büchi Automata, Co-Buchi Automata and Muller Automata, Rabin Automata, Streett Automata.
User
Notifications
Font Size

  • Kupferman, O., Morgenstern, G. and Murano, A., Typeness for ω-regular automata. Int. J. Found. Comput. Sci., 2004, 17(4), 324– 338.

  • Tao, Y., Infinity problems and countability problems for ω-automata. Inf. Proc. Lett., 2006, 100, 151–153.

  • Chen, Z., On the generative power of ω-grammars and ω-automata. Fundam. Infor., 2011, 111(2), 119–145.

  • Redziejowski, R. R., An improved construction of deterministic omega-automaton using derivatives. Fundam. Inform., 2012, 119(3–4), 393–406.

  • Kupferman, O. and Vardi, M. Y., Complementation constructions for nondeterministic automata on infinite words. 11th International Conference on Tools and Algorithms for the Constructions and Analysis of Systems (TACAS 2005). LNCS, 2005, 3440, 206–221.

  • Giannakopoulou, D. and Lerda, F., Efficient translation of LTL formulae into Büchi automata. RAICS Technical Report, Research Institute for Advanced Computer Science (RIACS), 1, 2001.

  • Fritz, C. and Wilke, T., Simulation relations for alternating Büchi automata. Theoret. Comput. Sci., 2005, 338(1–3), 275–314.

  • Carton, V and Michel, M., Unambiguous Büchi automata. Theoret. Comput. Sci., 2003, 297(1), 37–81.

  • Sheridan, D., Bounded model checking with SNF, alternating automata, and Büchi automata. Electron. Notes Theoret. Comput. Sci., 2005, 119(2), 83–101.

  • Boker, U. and Kupferman, O., Translating to co-Büchi made tight, unified and useful. ACM Trans. Comput. Logic (TOCL), 2012, 13(4), 29.

  • Piterman, N., From nondeterministic Büchi and Streett automata to deterministic parity automata. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), Seattle WA, USA, 12–15 August 2006, 3(3), 255–264.

  • Zeng, B. and Tan, L., Test reactive systems with Büchi automata: acceptance condition coverage criteria and performance evaluation. IEEE International Conference on Information Reuse and Integration (IRI), San Francisco, CA, USA, 13–15 August 2015, pp. 380–387.

  • Baier, C., Bertrand, N. and Großer, M., On decision problems for probabilistic Büchi automata. Int. Conference on Foundations of Software Science and Computational Structures (FoSSaCS2008), LNCS, 2008, 4962, 287–301.

  • Safra, S., On the complexity of omega automata. Proceedings of the 29th Annual Symposium on Foundations of ComputerScience (SFCS’88), Washington, DC, USA, 24–26 October 1988, pp. 319– 327.

  • Giannakis, K. and Andronikos, T., Querying linked data and Büchi automata. 9th International Workshop on Semantic and Social Media Adaptation and Personalization, 9th International Workshop of IEEE, Corfu, Greece, 6–7 November 2014, pp. 110–114.

  • Thiemann, P. and Sulzmann, M., From omega-regular expressions to Büchi automata via partial derivatives. Int. Conf. Language Automata Theory Appl., LATA, LNCS, 2015, 8977, 287–298.

  • Brzozowski, J. A., Derivatives of regular expressions. J. ACM, 1964, 11(4), 481–494.

  • Esik, Z. and Ivan, S., Büchi context-free languages. Theoret. Comput. Sci., 2011, 412(8–10), pp. 805–821.

  • Tsay, Y. K., Tsai, M. H., Chang, J. S., Chang, Y. W. and Liu, C. S., Büchi store: an open repository of omega-automata. Int. J. Software Tools for Technol. Transf., 2013, 15(2), 109–123.

  • Thomas, W., Automata on infinite objects. Handbook of Theoretical Computer Science, MIT Press Cambridge. MA, USA, 1990, 133–187.

  • Büchi, J. R., On a decision method in restricted second order arithmetic. Proc. International Congress on Logic, Method, and Philosophy of Science, Stanford, Stanford University Press, 1962, pp. 1–12.

  • Nitsche, U. U., A power-set construction for reducing Büchi automata to non-determinism degree two. Inf. Proc. Lett., 2007, 101(3), 107–111.

  • Colcombet, T. and Zdanowski, K., A tight lower bound for determinization of transition labeled Büchi automata. International Colloquium on Automata, Languages, and Programming, ICALP 2009, LNCS 5556, 2009, pp. 151–162.

  • Shan, L., Du, X. and Qin, Z., Efficient approach of translating LTL formulae into Büchi automata. Front. Comput. Sci., 2015, 9(4), 511–523.

  • Büchi, J. R., Decision methods in the theory of ordinals. Bull. Am. Math. Soc., 1965, 71, 767–770.

  • Wang, G., Mishchenko, A., Brayton, R. D. and Sangiovanni Vincentelli, A., Sequential Synthesis with Co-Büchi Specifications, ERL Technical Report, EECS Dept., UC Berkeley, 2006.

  • Rabin, M. O., Decidability of second-order theories and finite automata on infinite trees. Trans. Am. Math. Soc., 1969, 141, 1–35.

  • Muller, D. E., Infinite sequences and finite machines. 4th Annual Symposium on Switching Circuit Theory and Logical Design (SWCT), 1963, pp. 3–16.

  • Streett, R. S., Propositional dynamic logic of looping and converse. Inform. Control., 1982, 54, 121–141.

  • Henzinger, M. R. and Telle, J. A., Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. Scandinavian Workshop on Algorithm Theory, SWAT1996, LNCS, 1996, 1097, 16–27.

  • McNaughton, R. and Yamada, H., Regular expressions and state graphs for automata. IRE Tran. Electron. Comput., 1960, EC-9(1), 39–47.

  • Ginzburg, A., A procedure for checking equality of regular expressions. J. ACM, 1967, 14(2), 355–362.

  • Kumar, A. and Verma, A. K., Conversion of parallel regular expressions to non-deterministic finite automata using partial derivatives. Chiang Mai J. Sci., 2014, 41(5.2), 1409–1418.

  • Garhwal, S. and Jiwari, R., Parallel fuzzy regular expression and its conversion to epsilon-free fuzzy automaton. Comput. J., 2016, 59(9), 1383–1391.

  • Yan, Q., Lower bounds for complementation of ω-automata via the full automata technique. International Colloquium on Automata Languages and Programming (ICALP2006), LNCS, 2006, pp. 589–600.

  • Loding, C. and Thomas, W., Alternating automata and logics over infinite words. IFIP Int. Conf. Theoret. Comput. Sci. LNCS, 2000, 1872, 521–535.

  • Miyano, S. and Hayashi, T., Alternating finite automata on ωwords. Theoret. Comput. Sci., 1984, 32(3), 321–330.

  • Baier, C. and Grosser, M., Recognizing ω-regular languages with probabilistic automata. 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05), 2005, pp. 137–146.

  • Park, D., Concurrency and automata on infinite sequences. Theor. Comput. Sci., LNCS, 1981, 104, 167–183.

  • Staiger, L., Finite-state ω-languages. J. Comput. Syst. Sci., 1983, 1, 27(3), 434–448.

  • Redziejowski, R. R., Infinite-word languages and continuous mappings. Theor. Comput. Sci., 1986, 1(43), 59–79.

  • Tsay, Y. K., Chen, Y. F., Tsai, M. H., Wu, K. N. and Chan, W. C., Goal: a graphical tool for manipulating Büchi automata and temporal formulae. Int. Conf. Tools Algorithms Construct. Anal. Syst. LNCS, 2007, 4424, 466–471.

  • Angluin, D. and Fisman, D., Learning regular omega languages. Theor. Comput. Sci., 2016, 650, 57–72.

  • Chaturvedi, N., Olschewski, J. and Thomas, W., Languages versus ω-languages in regular infinite games. Int. J. Found. Comput. Sci., 2012, 23(5), 985–1000.

  • Selivanov, V. L., Fine hierarchy of regular aperiodic ω-languages. International Conference on Developments in Language Theory, DLT 2007, LNCS, 2007, 4588, 399–410.

  • d’Amorim, M. and Roşu, G., Efficient monitoring of ω-languages. International Conference on Computer Aided Verification. LNCS, 2005, 3576, 364–378.

  • Finkel, O., Closure properties of locally finite ω-languages. Theoret. Comput. Sci., 2004, 322(1), 69–84.

  • Thomas, W., Infinite trees and automaton-definable relations over ω-words. Ann. Symposium on aspects of Theoretical Computer Science (STACS 1990). LNCS, 1990, 415, 263–277.

  • Thistle, J. G. and Wonham, W., Control of omega-automata, Church’s problem, and the emptiness problem for tree omegaautomata. 5th Workshop on Computer Science Logic (CSL’91), 1991, 367–381.

  • Thistle, J. G. and Wonham, W. M., Control of infinite behavior of finite automata. SIAM J. Control Opt., 1994, 32(4), 1075–1097.

  • Maler, O. and Staiger, L., On syntactic congruencies for ω-languages. 10th Annual Symposium on Theoretical Computer Science. LNCS, 1993, 665, 586–594.

  • Thistle, J. G. and Malhame, R. P., Control of ω-automata under state fairness assumptions. Syst. Control Lett., 1998, 33(4), 265– 274.

  • Berry, G. and Sethi, R., From regular expressions to deterministic automata. Theor. Comput. Sci., 1986, 48(1), 117–126.

  • Owens, S., Reppy, J. and Turon, A., Regular-expression derivatives re-examined. J. Funct. Program., 2009, 19(2), 173–190.

  • Redziejowski, R. R., Construction of a deterministic ω-automaton using derivatives. RAIRO-Theoret. Inform. Appl., 1999, 33(2), 133–158.

  • Antimirov, V. M., Rewriting regular inequalities. 10th International Symposium on Fundamentals of Computation Theory, 1995, 116–125.

  • Antimirov, V., Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci., 1996, 155(2), 291– 319.

  • Caron, P., Champarnaud, J. M. and Mignot, L., Partial derivatives of an extended regular expression. International Conference on Language and Automata Theory and Applications, LATA, 2011. LNCS, 1996, 6638, 179–191.

  • Kumar, A. and Verma, A. K., A novel algorithm for the conversion of parallel regular expressions to non-deterministic finite automata. Appl. Math. Inform. Sci., 2014, 8(1), 95–105.

  • Brzozowski, J. A. and Leiss, E., On equations for regular languages, finite automata, and sequential networks. Theor. Comput. Sci., 1980, 10(1), 19–35.

  • Carton, O., Perrin, D. and Pin, J. E., Automata and semigroups recognizing infinite words. Logic and Automata, History and Perspectives, Amsterdam University Press, 2007.

  • Singh, N. and Kumar, A., Modelling finite and infinite behavior of cancer stages using Büchi and Finite Automata. Curr. Sci., 2018, 115(4), 1–5.

  • Vardi, M. Y. and Wolper, P., An automata-theoretic approach to automatic program verification. Proc. First Symp. Logic Comput. Sci., 1986, 322–331.

  • Sistla, A. P., Vardi, M. Y. and Wolper, P., The complementation problem for Büchi automata with applications to temporal logic. Theoret. Comput. Sci., 1987, 49(2–3), 217–237.

  • Clarke, E., Kroening, D., Ouaknine, J. and Strichman, O., Completeness and complexity of bounded model checking. International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004, LNCS, 2004, 2937, 85–96.

  • Young, S., Spanjol, D. and Garg, V. K., Control of discrete event systems modeled with deterministic Büchi automata. American Control Conference, IEEE, 2814–2818, 1992.

  • Jalan, S., Kumar, P. and Das, S., Formalization of digital forensic theory by using Büchi automaton. Third International Conference on Image Information Processing (ICIIP). IEEE, 2015, 102–108.

  • Fogarty, S., Kupferman, O. and Wilke, T., Profile trees for Büchi word automata with application to determinization. Inf. Comput., 2015, 245, 136–151.

  • Alfaro, L. D. and Henzinger, T. A., Concurrent omega-regular games. 15th Annual IEEE Symposium on Logic in Computer Science, 26–29 June 2000, pp. 141–154.

  • Zhao, L., Zhang, J. and Yang, J., Advances in on-the-fly emptiness checking algorithms for Büchi automata. 5th International Conference on Advanced Computational Intelligence (ICACI), IEEE, Nanjing China, 18–20 October 2012, pp. 113–118.

  • Etessami, K., Wilke, T. and Schuller, R. A., Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput., 2005, 34(5), 1159–1175.

  • Giannakis, K. and Andronikos, T., Use of Büchi automata and randomness for the description of biological processes. Int. J. Sci. World, 2015, 3(1), 113–123.

  • Serre, O., Parity games played on transition graphs of one-counter processes. International conference on foundations of software science and computation structures. LNCS, 2006, 3921, 337–351.

  • Alur, R. and Dill, D. L., A theory of timed automata. Theor. Comput. Sci., 1994, 126, 183–235.

  • Bollig, B. and Kuske, D., Muller message-passing automata and logics. Inf. Comput., 2008, 206(9–10), 1084–1094.

  • Henzinger, M. R. and Telle, J. A., Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. Scan. Workshop Algorithm Theory. LNCS, 1996, 1097, 16–27.


Abstract Views: 387

PDF Views: 136




  • Omega Automata and its Classes

Abstract Views: 387  |  PDF Views: 136

Authors

Natasha Singh
Thapar Institute of Engineering and Technology, Patiala 147 003, India
Ajay Kumar
Thapar Institute of Engineering and Technology, Patiala 147 003, India

Abstract


ω-automata is a variant of finite automata which accepts infinite strings. It represents the behaviour of the infinite systems (hardware, operating system and control systems) which are not expected to end. A variety of conditions are used to represent the set of accepting strings in ω-automata. This paper summarizes various types of ω-automata, their transition functions and accepting conditions. In addition, this paper also summarizes the applicability of omega automata in various interdisciplinary fields.

Keywords


Büchi Automata, Co-Buchi Automata and Muller Automata, Rabin Automata, Streett Automata.

References





DOI: https://doi.org/10.18520/cs%2Fv115%2Fi11%2F2042-2051