Advertisement
Published in:
2006 | OriginalPaper | Chapter
Minimizing Generalized Büchi Automata
Authors : Sudeep Juvekar, Nir Piterman
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We consider the problem of minimization of generalized Büchi automata. We extend fair-simulation minimization and delayed-simulation minimization to the case where the Büchi automaton has multiple acceptance conditions. For fair simulation, we show how to efficiently compute the fair-simulation relation while maintaining the structure of the automaton. We then use the fair-simulation relation to merge states and remove transitions. Our fair-simulation algorithm works in time
O
(
mn
3
k
2
) where
m
is the number of transitions,
n
is the number of states, and
k
is the number of acceptance sets. For delayed simulation, we extend the existing definition to the case of multiple acceptance conditions. We show that our definition can indeed be used for minimization and give an algorithm that computes the delayed-simulation relation. Our delayed-simulation algorithm works in time
O
(
mn
3
k
). We implemented the two algorithms and report on experimental results.