   Go backward to Closure and Hiding
Go up to Top
Go forward to Additional Temporal Operators

# Additional Temporal Operators

• $E$+v
• If $E$ ever becomes false, then state function $v$ stops changing.
• Behavior sigma satisfies $E$+v if either sigma satsfies $E$ or $E$ holds for the first $n$ states of sigmaand $v$ never changes form $\left(n+1\right)$-st state on.
• Proposition 3:
• |= (exists $x$: $Init$ and always [A]w)+v =
exists $x, s$: $Init$^ and always [A^]<w, v, s>
• $x$ tuple of variables not occuring in $v$.
• $s$ variable not occuring in $Init$, A, $w$, $v$, $x$.
• $Init$^ $<=>$ ($Init$ and ($s=0$)) or (not $Init$ and ($s=1$))
• A^ $<=>$(($s=0$) and((($s$'=0) and (A or($w\text{'} = w$)))
or (($s\text{'}$ = 1) and not (A or ($w\text{'} = w$)))))
or (($s$ = 1) and ($s\text{'}$ = 1) and ($v\text{'} = v$))
• Reasoning about $E$+v
• Calculate A($E$)+v = A($E$+v) 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   