Title: Beyond Vacuity: Towards the Strongest Passing Formula

Ofer  Strichman (Technion)

Abstract:
Given an LTL formula \varphi 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 \varphi 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 \varphi as defined above. This formula
is stronger or equally strong to any formula that can be obtained by vacuity
and mutual vacuity.
Joint work with Hana Chockler and Arie Gurfinkel