ICAR Research Data Repository for Knowledge Management
DSpace at IIT Bombay
View Archive InfoMetadata
| Field | Value |
| Title | On minimal odd rankings for Buchi complementation |
| Names |
KARMARKAR, H
CHAKRABORTY, S |
| Date Issued | 2009 (iso8601) |
| Abstract | We study minimal odd rankings (as defined by Kupferman and Vardi[KV01]) for run-DAGs of words in the complement of a nondeterministic Buchi automaton. We present an optimized version of the ranking based complementation construction of Friedgut, Kupferman and Vardi [FKV06] and Schewe's[Sch09] variant of it, such that every accepting run of the complement automaton assigns a minimal odd ranking to the corresponding run-DAG. This allows us to determine minimally inessential ranks and redundant slices in ranking-based complementation constructions. We exploit this to reduce the size of the complement Buchi automaton by eliminating all redundant slices. We demonstrate the practical importance of this result through a set of experiments using the NuSMV model checker. |
| Genre | Proceedings Paper |
| Topic | Temporal Logic |
| Identifier | AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS,5799,228-243 |