Coinductive algorithms for Büchi automata

DOI10.3233/FI-2021-2046MaRDI QIDQ5158653zbMATH OpenFDO

Authors Denis Kuperberg, Laureline Pinault, Damien Pous

Publication date 25 October 2021

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/FI-2021-2046

zbMATH Keywords

Büchi automatacoinductionlanguage equivalence

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Coinductive algorithms for Büchi automata
• Coalgebraic up-to techniques
• Equivalence of infinite behavior of finite automata
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Coinductive proof techniques for language equivalence

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• A lattice-theoretical fixpoint theorem and its applications
• Advanced automata minimization
• Antichain algorithms for finite automata
• Antichains for the Automata-Based Approach to Model-Checking
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Büchi Complementation and Size-Change Termination
• Checking NFA equivalence with bisimulations up to congruence
• Coinduction All the Way Up
• Efficiency of a Good But Not Linear Set Union Algorithm
• Efficient Büchi universality checking
• scientific article; zbMATH DE number 988807 (Why is no real title available?)
• scientific article; zbMATH DE number 44695 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• On complementing nondeterministic Büchi automata
• Revealing vs. concealing: more simulation games for Büchi inclusion
• Ultimately periodic words of rational ω-languages
• Weak alternating automata are not that weak
• When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)

Cited in

(7)

• Coinductive algorithms for Büchi automata
• Coalgebraic up-to techniques
• Brzozowski's and up-to algorithms for must testing
• Coinductive proof techniques for language equivalence
• FORQ-Based Language Inclusion Formal Testing
• A robust measure on FDFAs following duo-normalized acceptance
• Proving language inclusion and equivalence by coinduction

Describes a project that uses

Uses Software

• Antichains
• LTL2BA

This page was built for publication: Coinductive algorithms for Büchi automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5158653)