Minimizing generalized Buchi automata
DSpace at IIT Bombay
View Archive InfoField | Value | |
Title |
Minimizing generalized Buchi automata
|
|
Creator |
JUVEKAR, S
PITERMAN, N |
|
Subject |
fair simulation
model checking |
|
Description |
We consider the problem of minimization of generalized Buchi automata. We extend fair-simulation minimization and delayed-simulation minimization to the case where the Buchi 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 Tn 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.
|
|
Publisher |
SPRINGER-VERLAG BERLIN
|
|
Date |
2011-10-23T20:52:48Z
2011-12-15T09:11:01Z 2011-10-23T20:52:48Z 2011-12-15T09:11:01Z 2006 |
|
Type |
Article; Proceedings Paper
|
|
Identifier |
COMPUTER AIDED VERIFICATION, PROCEEDINGS,4144,45-58
3-540-37406-X 0302-9743 http://dspace.library.iitb.ac.in/xmlui/handle/10054/15232 http://hdl.handle.net/100/1799 |
|
Source |
18th International Conference on Computer Aided Verification,Seattle, WA,AUG 17-20, 2006
|
|
Language |
English
|
|