Beyond Vacuity: Towards the Strongest Passing Formula

Hana Chockler; Arie Gurfinkel; Ofer Strichman

Beyond Vacuity: Towards the Strongest Passing Formula

Hana Chockler, Arie Gurfinkel, Ofer Strichman

Research output: Contribution to journal › Article › peer-review

5 Citations (Scopus)

33 Downloads (Pure)

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.

Original language	English
Pages (from-to)	552-571
Number of pages	20
Journal	FORMAL METHODS IN SYSTEM DESIGN
Volume	43
Issue number	3
Publication status	Published - 29 Aug 2013

Access to Document

strongest

Cite this

@article{e448eea1bc164aa2a609de8c4f8ab4a9,

title = "Beyond Vacuity: Towards the Strongest Passing Formula",

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.",

author = "Hana Chockler and Arie Gurfinkel and Ofer Strichman",

year = "2013",

month = aug,

day = "29",

language = "English",

volume = "43",

pages = "552--571",

journal = "FORMAL METHODS IN SYSTEM DESIGN",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - Beyond Vacuity: Towards the Strongest Passing Formula

AU - Chockler, Hana

AU - Gurfinkel, Arie

AU - Strichman, Ofer

PY - 2013/8/29

Y1 - 2013/8/29

N2 - 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.

AB - 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.

M3 - Article

SN - 0925-9856

VL - 43

SP - 552

EP - 571

JO - FORMAL METHODS IN SYSTEM DESIGN

JF - FORMAL METHODS IN SYSTEM DESIGN

IS - 3

ER -