Input-based Three-valued Abstraction Refinement

Jan Onderka, Stefan Ratschan

Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algo…