Name
Abstract | ||
|---|---|---|
Abstract—Given an LTL formula ' 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 ' 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 ' 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. I. I NTRODUCTION In finite-state model checking [CE81], [QS82], [LP85] we |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/s10703-013-0192-6 | Formal Methods in Computer-Aided Design |
Keywords | Field | DocType |
strengthened version,mutual vacuity attempt,mutual vacuity,boolean closure,lattice automaton,negation normal form,ltl formula,model m,strongest ltl formula,model checking | Boolean function,Data structure,Discrete mathematics,Automata theory,Maximal set,Negation normal form,Model checking,Lattice (order),Computer science,Algorithm,Theoretical computer science | Journal |
Volume | Issue | ISSN |
43 | 3 | 0925-9856 |
ISBN | Citations | PageRank |
978-1-4244-2736-9 | 6 | 0.46 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hana Chockler | 1 | 482 | 38.31 |
| Arie Gurfinkel | 2 | 939 | 55.15 |
| Ofer Strichman | 3 | 1071 | 63.61 |