Semantic Vacuity

The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the s...

Full description

Saved in:
Bibliographic Details
Main Authors: Maretic, Grgur Petric, Dasthi, Mohammad Torabi, Basin, David
Format: Conference Proceeding
Language:English
Subjects:
Automata
Cognition
Complexity theory
Computational modeling
Model checking
Semantics
Syntactics
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the syntax of a temporal logic. They are therefore syntactic: whether a model vacuously satisfies a formula is affected by semantics-preserving changes to the formula. This leads to inconsistent and counter-intuitive results. We propose an alternative: a semantic definition of vacuity for LTL where either two semantically equivalent LTL formulas are both satisfied vacuously in a model, or neither of them are. Our definition is based on a syntactic-invariant separation of LTL formulas, which gives rise to an algorithm for detecting semantic vacuity using trap properties. We also propose an alternative algorithm for Buchi automata, which can be used to detect the vacuous satisfaction of omega-regular properties as well as LTL formulas. We analyze this algorithm's worst-case complexity and, using real-world examples, demonstrate that semantic vacuity can be efficiently decided in practice.
ISSN:1530-1311
2332-6468
DOI:10.1109/TIME.2015.14