Coinductive Algorithms for Büchi Automata
| Autor: | Denis Kuperberg, Laureline Pinault, Damien Pous |
|---|---|
| Přispěvatelé: | Preuves et Langages (PLUME), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Plume, ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016), Pous, Damien, Community of mathematics and fundamental computer science in Lyon - - MILYON2010 - ANR-10-LABX-0070 - LABX - VALID, Coinduction for Verification and Certification - CoVeCe - - H20202016-04-01 - 2021-03-31 - 678157 - VALID, Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
050101 languages & linguistics
Algebra and Number Theory [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] Computer science 05 social sciences Coinduction Structure (category theory) Büchi automaton [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 02 engineering and technology 0102 computer and information sciences 01 natural sciences Theoretical Computer Science Automaton Computational Theory and Mathematics 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Equivalence (formal languages) Algorithm Equivalence (measure theory) Computer Science::Formal Languages and Automata Theory Information Systems |
| Zdroj: | Fundamenta Informaticae Fundamenta Informaticae, 2021, 180 (4), pp.351-373. ⟨10.3233/FI-2021-2046⟩ Developments in Language Theory Developments in Language Theory, Aug 2019, Varsovie, Poland Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2021, 180 (4), pp.351-373. ⟨10.3233/FI-2021-2046⟩ Lecture Notes in Computer Science Lecture Notes in Computer Science-Developments in Language Theory Developments in Language Theory ISBN: 9783030248857 DLT |
| ISSN: | 0169-2968 0302-9743 1611-3349 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|