Coinductive Algorithms for Büchi Automata

DOI10.3233/FI-2021-2046zbMath1497.68272MaRDI QIDQ5158653

Denis Kuperberg, Laureline Pinault, Damien Pous

Publication date: 25 October 2021

Published in: Fundamenta Informaticae (Search for Journal in Brave)

zbMATH Keywords

language equivalenceBüchi automatacoinduction

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Uses Software

• LTL2BA
• Antichains

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A completeness theorem for Kleene algebras and the algebra of regular events
• A lattice-theoretical fixpoint theorem and its applications
• Advanced automata minimization
• Checking NFA equivalence with bisimulations up to congruence
• Weak alternating automata are not that weak
• Antichain Algorithms for Finite Automata
• When Simulation Meets Antichains
• Efficient Büchi Universality Checking
• Büchi Complementation and Size-Change Termination
• Antichains for the Automata-Based Approach to Model-Checking
• Efficiency of a Good But Not Linear Set Union Algorithm
• Coinduction All the Way Up
• Revealing vs. Concealing: More Simulation Games for Büchi Inclusion
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Ultimately periodic words of rational ω-languages
• Correct Hardware Design and Verification Methods