|M.Sc Student||Gross Ron|
|Subject||Invariance under Stuttering in Branching-Time Temporal Logic|
|Department||Department of Computer Science||Supervisor||Professor Michael Kaminski|
|Full Thesis text|
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 Grumberg. 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-Fraisse 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.