| TR#: | MSC-2008-19 |
| Class: | MSC |
| Title: | Invariance Under Stuttering in Branching-Time Temporal Logic |
| Authors: | Ron Gross |
| Supervisors: | Michael Kaminski |
| MSC-2008-19.pdf | |
| Abstract: | Invariance under temporal stuttering is a useful and attractive feature of specifications and specification languages. Linear stuttering has been intensively studied, and several languages for expressing linear stutter-invariant properties are known from the literature. However, less work has been done on branching-time stuttering. A definition of branching-time stuttering was proposed by Browne, Clarke and Gr\"{u}mberg. It is arguable whether this definition is the "right" definition of branching-time stutter-equivalence.
We come up with an alternative definition of branching-time stuttering based on stuttering steps. We show that, for our definition, the "next-time" operator is required in order to express some stutter-invariant properties in the logic CTL*, using an Ehrenfeucht-Fra\"iss\'e game for CTL*. We then introduce BGTLA, a stutter-invariant extension of the Temporal Logic of Actions for branching time. Finally, we present some results on algorithmic testing of stutter equivalence, both for general temporal structures and for the special case of finite Kripke structures.
|
| Copyright | The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information |
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2008/MSC/MSC-2008-19), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.
To the list of the MSC technical reports of 2008
To the main CS technical reports page