Record Details

On minimal odd rankings for Buchi complementation

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title On minimal odd rankings for Buchi complementation
 
Creator KARMARKAR, H
CHAKRABORTY, S
 
Subject temporal logic
automata
 
Description 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.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-24T01:56:34Z
2011-12-15T09:11:22Z
2011-10-24T01:56:34Z
2011-12-15T09:11:22Z
2009
 
Type Proceedings Paper
 
Identifier AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS,5799,228-243
978-3-642-04760-2
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15300
http://hdl.handle.net/100/2023
 
Source 7th International Symposium on Automated Technology for Verification and Analysis,Macao, PEOPLES R CHINA,OCT 13-16, 2009
 
Language English