SCIENCE@home

Events in linear-time properties

Dimitrie O. Paun,M. Chechik

Published 1999 in Proceedings IEEE International Symposium on Requirements Engineering (Cat. No.PR00188)

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. 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.

PUBLICATION RECORD

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-29 of 29 references · Page 1 of 1

CITED BY

Showing 1-27 of 27 citing papers · Page 1 of 1