טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentGross Ron
SubjectInvariance under Stuttering in Branching-Time Temporal Logic
DepartmentDepartment of Computer Science
Supervisor Professor Michael Kaminski
Full Thesis textFull thesis text - English Version


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