Go backward to Closure and Hiding
Go up to Top
Go forward to Additional Temporal Operators
Additional Temporal Operators
-
- If ever becomes false, then state function stops changing.
- Behavior sigma satisfies if either sigma satsfies
or holds for the first states of sigmaand never changes form
-st state on.
- Proposition 3:
- |= (exists : and always [A]) =
exists : ^ and always [A^]
- tuple of variables not occuring in .
- variable not occuring in , A, , , .
- ^ ( and ()) or (not
and ())
- A^ (() and((('=0)
and (A or()))
or (( = 1) and not (A or ()))))
or (( = 1) and ( = 1) and ())
- Reasoning about
- Calculate A() = A() applying
Prop. 3.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine