Events in Linear-Time Properties

TL;DR

This paper explores the properties of linear-time temporal logic (LTL), focusing on stuttering invariance, and introduces new theoretical tools for syntactic reasoning about these properties to improve formal verification methods.

Contribution

It introduces the concept of edges in LTL and provides theorems for syntactic analysis of stuttering closure, relaxing previous restrictions for better expressiveness.

Findings

Edges in LTL enable better analysis of properties.

Theorems for syntactic reasoning about stuttering closure.

Relaxation of restrictions improves property expressiveness.

Abstract

For over a decade, researchers in formal methods tried to create formalisms that permit natural specification of systems and allow mathematical reasoning about their correctness. The availability of fully-automated reasoning tools enables more non-specialists to use formal methods effectively --- their responsibility reduces to just specifying the model and expressing the desired properties. Thus, it is essential that these properties be represented in a language that is easy to use and sufficiently expressive. Linear-time temporal logic is a formalism that has been extensively used by researchers for specifying properties of systems. When such properties are closed under stuttering, i.e. their interpretation is not modified by transitions that leave the system in the same state, verification tools can utilize a partial-order reduction technique to reduce the size of the model and thus analyze larger systems. If LTL formulas do not contain the ``next'' operator, the formulas are closed under stuttering, but the resulting language is not expressive enough to capture many important properties, e.g., properties involving events. Determining if an arbitrary LTL formula is closed under stuttering is hard --- it has been proven to be PSPACE-complete. In this paper we relax the restriction on LTL that guarantees closure under stuttering, introduce the notion of edges in the context of LTL, and provide theorems that enable syntactic reasoning about closure under stuttering of LTL formulas.