×

On minimal odd rankings for Büchi complementation. (English) Zbl 1258.68085

Liu, Zhiming (ed.) et al., Automated technology for verification and analysis. 7th international symposium, ATVA 2009, Macao, China, October 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04760-2/pbk). Lecture Notes in Computer Science 5799, 228-243 (2009).
Summary: We study minimal odd rankings (as defined by O. Kupferman and M. Y. Vardi [ACM Trans. Comput. Log. 2, No. 3, 408–429 (2001; Zbl 1171.68551)]) for run-DAGs of words in the complement of a nondeterministic Büchi automaton. We present an optimized version of the ranking-based complementation construction of E. Friedgut [Int. J. Found. Comput. Sci. 17, No. 4, 851–867 (2006; Zbl 1096.68081)] and S. Schewe’s [LIPICS – Leibniz Int. Proc. Inform. 3, 661–672 (2009; Zbl 1236.68176)] 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 Büchi automaton by eliminating all redundant slices. We demonstrate the practical importance of this result through a set of experiments using the NuSMV model checker.
For the entire collection see [Zbl 1176.68012].

MSC:

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

NuSMV
PDFBibTeX XMLCite
Full Text: DOI