Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata

2005 ◽  
Vol 34 (5) ◽  
pp. 1159-1175 ◽  
Author(s):  
Kousha Etessami ◽  
Thomas Wilke ◽  
Rebecca A. Schuller
Keyword(s):  
State Space ◽  
Space Reduction ◽  
Büchi Automata ◽  
Parity Games ◽  
Simulation Relations ◽  
Buchi Automata ◽  
State Space Reduction

scholarly journals Coinductive Algorithms for Büchi Automata

2021 ◽  
Vol 180 (4) ◽  
pp. 351-373
Author(s):  
Denis Kuperberg ◽  
Laureline Pinault ◽  
Damien Pous
Keyword(s):  
State Space ◽  
State Of The Art ◽  
The State ◽  
Specific Structure ◽  
Büchi Automata ◽  
Deterministic Automata ◽  
Buchi Automata ◽  
Language Equivalence ◽  
Art Techniques

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.

Sign in / Sign up

Export Citation Format

Share Document