DocumentCode
1579987
Title
Beyond Vacuity: Towards the Strongest Passing Formula
Author
Chockler, Hana ; Gurfinkel, Arie ; Strichman, Ofer
Author_Institution
IBM Haifa Res. Lab., Haifa
fYear
2008
Firstpage
1
Lastpage
8
Abstract
Given an LTL formula phi in negation normal form, it can be strengthened by replacing some of its literals with FALSE. Given such a formula and a model M that satisfies it, vacuity and mutual vacuity attempt to find one or a maximal set of literals, respectively, with which phi can be strengthened while still being satisfied by M. We study the problem of finding the strongest LTL formula that satisfies M and is in the Boolean closure of strengthened versions of phi as defined above. This formula is stronger or equally strong to any formula that can be obtained by vacuity and mutual vacuity. We present our algorithms in the framework of lattice automata.
Keywords
Boolean functions; automata theory; formal verification; Boolean closure; LTL formula; lattice automata; mutual vacuity; negation normal form; Automata; Boolean functions; Data structures; Formal verification; Hardware; Information systems; Lattices; Logic; Software engineering; Systems engineering and theory;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Methods in Computer-Aided Design, 2008. FMCAD '08
Conference_Location
Portland, OR
Print_ISBN
978-1-4244-2735-2
Electronic_ISBN
978-1-4244-2736-9
Type
conf
DOI
10.1109/FMCAD.2008.ECP.28
Filename
4689187
Link To Document