Computer Science – Software Engineering
Scientific paper
1999-06-28
Proceedings of 4th IEEE International Symposium on Requirements Engineering, June 1999, pp. 123-132
Computer Science
Software Engineering
10 pages, 4 figures
Scientific paper
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.
Chechik Marsha
Paun D.
No associations
LandOfFree
Events in Linear-Time Properties 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 Events in Linear-Time Properties, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Events in Linear-Time Properties will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-681461