From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata
Tóm tắt
The topic of this paper is the determinization problem of
$$\omega $$
-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.
Tài liệu tham khảo
Babiak T, Blahoudek F, Duret-Lutz A, Klein J, Křetínský J, Müller D, Parker D, Strejček J (2015) The hanoi omega-automata format. In: Computer aided verification (CAV’15), LNCS. Springer
Baier C, Blahoudek F, Duret-Lutz A, Klein J, Müller D, Strejček J (2019) Generic emptiness check for fun and profit. In: Automated technology for verification and analysis (ATVA), LNCS. Springer
Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press
Baier C, Kiefer S, Klein J, Klüppelholz S, Müller D, Worrell J (2016) Markov chains and unambiguous Büchi automata. In: Computer aided verification (CAV), LNCS. Springer
Ben-Ari M (2008) Principles of the spin model checker. Springer-Verlag, London
Blahoudek F (2018) Automata for formal methods: little steps towards perfection. Ph.D. thesis, Masaryk University, Faculty of Informatics
Blahoudek F, Duret-Lutz A, Klokocka M, Kretínský M, Strejcek J (2017) Seminator: a tool for Semi-Determinization of Omega-Automata. In: International conference on logic for programming, artificial intelligence and reasoning (LPAR), EPiC Series in Computing
Blahoudek F, Duret-Lutz A, Strejček J (2020) Seminator 2 can complement generalized Büchi automata via improved semi-determinization. In: Lahiri SK, Wang C (eds) Computer aided verification. Springer International Publishing, Cham, pp 15–27
Blahoudek F, Major J, Strejček J (2019) LTL to smaller self-loop alternating automata and back. In: Theoretical aspects of computing (ICTAC), LNCS. Springer
Bloemen V, Duret-Lutz A, van de Pol J (2019) Model checking with generalized Rabin and Fin-less automata. Int J Soft Tools Technol Transf 21(3):307–324
Boker U (2018) Why these automata types? In: EPiC series in computing, 57, 143–163. EasyChair
Chatterjee K, Gaiser A, Křetínský J (2013) Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Computer aided verification (CAV), LNCS. Springer
Colcombet T (2015) Unambiguity in automata theory. In: J. Shallit, A. Okhotin (eds.) Descriptional complexity of formal systems, lecture notes in computer science, pp. 3–18. Springer International Publishing, Cham. https://doi.org/10.1007/978-3-319-19225-3_1
Courcoubetis C, Yannakakis M (1988) Verifying temporal properties of finite-state probabilistic programs. In: [Proceedings 1988] 29th annual symposium on foundations of computer science, pp. 338–345 . 10.1109/SFCS.1988.21950
Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857–907
Couvreur JM (1999) On-the-fly verification of linear temporal logic. In: Formal methods (FM), LNCS. Springer
Duret-Lutz A (2017) Contributions to LTL and \(\omega \)-automata for model checking. Habilitation thesis, Université Pierre et Marie Curie
Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault É, Xu L (2016) Spot 2.0–A framework for LTL and \(\omega \)-automata manipulation. In: Automated technology for verification and analysis (ATVA), LNCS. Springer
Duret-Lutz A, Poitrenaud D, Couvreur JM (2009) On-the-fly emptiness check of transition-based Streett automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer
Emerson EA, Lei CL (1987) Modalities for model checking: branching time logic strikes back. Sci Comput Program 8(3):275–306
Esparza J, Křetínský J, Sickert S (2018) One theorem to rule them all: a unified translation of LTL into \(\omega \)-Automata. In: logic in computer science (LICS). ACM
Giannakopoulou D, Lerda F (2002) From states to transitions: improving translation of LTL formulae to Büchi automata. In: Formal techniques for networked and distributed sytems (FORTE), LNCS. Springer
Hahn EM, Li G, Schewe S, Turrini A, Zhang L (2015) Lazy probabilistic model checking without determinisation. In: Concurrency theory (CONCUR)
Hahn EM, Perez M, Schewe S, Somenzi F, Trivedi A, Wojtczak D (2020) Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In: Tools and algorithms for the construction and analysis of systems (TACAS), LNCS. Springer
Jantsch S, Müller D, Baier C, Klein J (2019) From LTL to unambiguous Büchi automata via disambiguation of alternating automata. In: ter Beek MH, McIver A, Oliveira JN (eds) Formal methods–the next 30 years, LNCS. Springer International Publishing, Cham, pp 262–279
John T, Jantsch S, Baier C, Klüppelholz S (2021) Determinization and limit-determinization of emerson-lei automata. In: Z. Hou, V. Ganesh (eds.) Automated technology for verification and analysis (ATVA), pp. 15–31. Springer International Publishing, Cham . https://doi.org/10.1007/978-3-030-88885-5_2
John T, Jantsch S, Baier C, Klüppelholz S (2021) Determinization and limit-determinization of Emerson-Lei automata-supplementary material (ATVA’21). https://doi.org/10.6084/m9.figshare.14838654.v1
Klein J, Müller D, Baier C, Klüppelholz S (2014) Are good-for-games automata good for probabilistic model checking? In: Language and automata theory and applications (LATA), LNCS. Springer
Křetínský J, Meggendorfer T, Sickert S (2018) Owl: a library for \(\omega \)-words, automata, and LTL. In: Automated technology for verification and analysis, LNCS
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV), LNCS. Springer
Löding C, Pirogov A (2019) Determinization of Büchi automata: unifying the approaches of Safra and Muller-Schupp. In: International colloquium on automata, languages, and programming (ICALP), leibniz international proceedings in informatics (LIPIcs)
Major J, Blahoudek F, Strejček J, Sasaráková M, Zbončáková T(2019) ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: Automated technology for verification and analysis (ATVA)
Miyano S, Hayashi T (1984) Alternating finite automata on \(\omega \)-words. Theor Comput Sci 32(3):321-330
Müller D (2019) Alternative automata-based approaches to probabilistic model checking. Ph.D. thesis, Technische Universität Dresden
Müller D, Sickert S (2017) LTL to deterministic Emerson-Lei automata. In: Games, automata, logics and formal verification (GandALF), EPTCS
Muller DE, Schupp PE (1995) Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin. McNaughton and Safra. Theor Comput Sci 141(1):69–107
Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Symposium on principles of programming languages (POPL). Association for computing machinery (ACM), New York, NY, USA
Redziejowski RR (2012) An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3–4):393–406
Renkin F, Duret-Lutz A, Pommellet A (2020) Practical “Paritizing” of Emerson-Lei automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer
Safra S (1989) Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel
Safra S, Vardi MY (1989) On omega-automata and temporal logic. In: Symposium on theory of computing (STOC). Association for computing machinery (ACM), New York, NY, USA
Schewe S, Varghese T (2012) Tight bounds for the determinisation and complementation of generalised Büchi Automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer
Sickert S, Esparza J, Jaax S, Křetínský J (2016) Limit-deterministic Büchi automata for linear temporal logic. In: Computer aided verification (CAV), LNCS. Springer
Vardi MY (1985) Automatic verification of probabilistic concurrent finite state programs. In: Symposium on foundations of computer science (SFCS)