Robust Vacuity for Branching Temporal Logic

Details Robust Vacuity for Branching Temporal Logic Robust Vacuity for Branching Temporal Logic

2010-02-24

arxiv.org/abs/1002.4616v2

Computer Science

Logic in Computer Science

Scientific paper

There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventually followed by an acknowledgment" is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. There are several existing definitions of vacuity. Originally, Beer et al. formalized vacuity as insensitivity to syntactic perturbation. However, this definition is only reasonable for vacuity in a single occurrence. Armoni et al. argued that vacuity must be robust -- not affected by semantically invariant changes, such as extending a model with additional atomic propositions. They show that syntactic vacuity is not robust for LTL, and propose an alternative definition -- trace vacuity. In this article, we continue this line of research. We show that trace vacuity is not robust for branching time logic. We refine it to apply uniformly to linear and branching time logic and to not suffer from the common pitfalls of prior definitions. Our new definition -- bisimulation vacuity -- is a proper non-trivial extension of both syntactic and trace vacuity. We discuss the complexity of detecting bisimulation vacuity, and give efficient algorithms to detect vacuity for several practically-relevant subsets of CTL*.

Affiliated with

Also associated with

No associations

Rating

Robust Vacuity for Branching Temporal Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Robust Vacuity for Branching Temporal Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Robust Vacuity for Branching Temporal Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-378740