Coinductive Algorithms for Büchi Automata

• Autorzy: Kuperberg Denis , Pinault Laureline , Pous Damien

Identyfikatory

DOI

10.3233/FI-2021-2046

• Języki publikacji: EN

Abstrakty

EN

We propose a new algorithm for checking language equivalence of non-deterministic Büchi automata. We start from a construction proposed by Calbrix, Nivat and Podelski, which makes it possible to reduce the problem to that of checking equivalence of automata on finite words. Although this construction generates large and highly non-deterministic automata, we show how to exploit their specific structure and apply state-of-the art techniques based on coinduction to reduce the state-space that has to be explored. Doing so, we obtain algorithms which do not require full determinisation or complementation.

Słowa kluczowe

EN

Büchi automata; language equivalence; coinduction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 180, nr 4
• Strony: 351--373
• Opis fizyczny: Bibliogr. 27 poz., rys., tab.

Twórcy

autor

Kuperberg Denis

• CNRS, ENS de Lyon, UCB Lyon 1, LIP, France

autor

Pinault Laureline

• CNRS, ENS de Lyon, UCB Lyon 1, LIP, France

autor

Pous Damien

• CNRS, ENS de Lyon, UCB Lyon 1, LIP, France

Bibliografia

• [1] Büchi JR. On a Decision Method in Restricted Second Order Arithmetic. In: Mac Lane S, Siefkes D (eds.), The Collected Works of J. Richard Büchi, pp. 425-435. Springer New York, New York, NY, 1990.
• [2] Vardi MY. An automata-theoretic approach to linear temporal logic. In: Logics for concurrency, pp. 238-266. Springer, 1996.
• [3] Gastin P, Oddoux D. Fast LTL to Büchi automata translation. In: CAV. Springer, 2001 pp. 53-65.
• [4] Gurumurthy S, Kupferman O, Somenzi F, Vardi MY. On complementing nondeterministic Büchi automata. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer, 2003 pp. 96-110.
• [5] Abdulla PA, Chen Y, Clemente L, Holík L, Hong C, Mayr R, Vojnar T. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In: CAV, volume 6174 of Lecture Notes in Computer Science. Springer, 2010 pp. 132-147. doi:10.1007/978-3-642-14295-6\_14.
• [6] Hutagalung M, Lange M, Lozes E. Revealing vs. concealing: More simulation games for Büchi inclusion. In: LATA. Springer, 2013 pp. 347-358.
• [7] Wulf MD, Doyen L, Henzinger TA, Raskin JF. Antichains: A New Algorithm for Checking Universality of Finite Automata. In: CAV, volume 4144 of Lecture Notes in Computer Science. Springer, 2006 pp. 17-30. doi:10.1007/11817963_5.
• [8] Abdulla PA, Chen YF, Holík L, Mayr R, Vojnar T. When Simulation Meets Antichains. In: TACAS, volume 6015 of Lecture Notes in Computer Science. Springer, 2010 pp. 158-174. doi:10.1007/978-3-642-12002-2_14.
• [9] Doyen L, Raskin JF. Antichain Algorithms for Finite Automata. In: TACAS, volume 6015 of Lecture Notes in Computer Science. Springer, 2010 doi:10.1007/978-3-642-12002-2_2.
• [10] Bonchi F, Pous D. Checking NFA equivalence with bisimulations up to congruence. In: POPL. ACM. ISBN 978-1-4503-1832-7, 2013 pp. 457-468. doi:10.1145/2429069.2429124.
• [11] Hopcroft JE, Karp RM. A Linear Algorithm for Testing Equivalence of Finite Automata. Technical Report 114, Cornell Univ., 1971. URL http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR71-114.
• [12] Fogarty S, Vardi MY. Büchi Complementation and Size-Change Termination. In: TACAS, volume 5505 of Lecture Notes in Computer Science. Springer, 2009 pp. 16-30. doi:10.1007/978-3-642-00768-2\_2.
• [13] Fogarty S, Vardi MY. Efficient Büchi Universality Checking. In: TACAS, volume 6015 of Lecture Notes in Computer Science. Springer, 2010 pp. 205-220. doi:10.1007/978-3-642-12002-2\_17.
• [14] Doyen L, Raskin J. Antichains for the Automata-Based Approach to Model-Checking. Logical Methods in Computer Science, 2009. 5(1). doi:10.2168/LMCS-5(1:5)2009.
• [15] Calbrix H, Nivat M, Podelski A. Ultimately Periodic Words of Rational w-Languages. In: MFPS, volume 802 of Lecture Notes in Computer Science. Springer, 1993 pp. 554-566. doi:10.1007/3-540-58027-1\_27.
• [16] Perrin D, Pin JÉ. Semigroups and automata on infinite words. NATO ASI Series C Mathematical and Physical Sciences-Advanced Study Institute, 1995. 466:49-72.
• [17] Knaster B. Un théorème sur les fonctions d’ensembles. Annales de la Société Polonaise de Mathématiques, 1928. 6:133-134.
• [18] Tarski A. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 1955. 5(2):285-309.
• [19] Hopcroft JE. An N log N algorithm for Minimizing in a Finite Automaton. In: International Symposium of Theory of Machines and Computations. Academic Press, NY, USA, 1971 pp. 189-196.
• [20] Tarjan RE. Efficiency of a Good But Not Linear Set Union Algorithm. Journal of the ACM, 1975. 22(2):215-225. doi:10.1145/321879.321884.
• [21] Conway JH. Regular algebra and finite machines. Chapman and Hall, 1971.
• [22] Kozen D. A Completeness Theorem for KLeene Algebras and the Algebra of Regular Events. Information and Computation, 1994. 110(2):366-390. doi:10.1006/inco.1994.1037.
• [23] Pous D. Coinduction All the Way Up. In: LICS. ACM, 2016 pp. 307-316. doi:10.1145/2933575.2934564.
• [24] Abdulla PA, Chen Y, Clemente L, Holík L, Hong C, Mayr R, Vojnar T. Advanced Ramsey-Based Büchi Automata Inclusion Testing. In: CONCUR, volume 6901 of Lecture Notes in Computer Science. Springer, 2011 pp. 187-202. doi:10.1007/978-3-642-23217-6\_13.
• [25] Mayr R, Clemente L. Advanced automata minimization. In: POPL, 2013. ACM, 2013 pp. 63-74. doi:10.1145/2429069.2429079.
• [26] Kupferman O, Vardi MY. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2001. 2(3):408-429. doi:10.1145/377978.377993.
• [27] Doyen L, Raskin J. Improved Algorithms for the Automata-Based Approach to Model-Checking. In: TACAS, volume 4424 of Lecture Notes in Computer Science. Springer, 2007 pp. 451-465. doi:10.1007/978-3-540-71209-1\_34.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).