Beyond Vacuity: Towards the Strongest Passing Formula

Hana Chockler*, Arie Gurfinkel, Ofer Strichman

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter

10 Citations (Scopus)

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.

Original languageEnglish
Title of host publication2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN
EditorsA Cimatti, RB Jones
Place of PublicationNEW YORK
PublisherIEEE
Pages188-195
Number of pages8
ISBN (Print)978-1-4244-2735-2
DOIs
Publication statusPublished - 2008
Event8th International Conference on Formal Methods in Computer-Aided Design - Portland, United Kingdom
Duration: 17 Nov 200820 Nov 2008

Conference

Conference8th International Conference on Formal Methods in Computer-Aided Design
Country/TerritoryUnited Kingdom
CityPortland
Period17/11/200820/11/2008

Keywords

  • MODEL-CHECKING

Cite this