Technical Report MSC-2008-19

Title: Invariance Under Stuttering in Branching-Time Temporal Logic
Authors: Ron Gross
Supervisors: Michael Kaminski
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.

CopyrightThe 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 (, rather than to the URL of the PDF 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

Computer science department, Technion