Go backward to Additional Temporal Operators
Go up to Top
Go forward to Additional Temporal Operators
Additional Temporal Operators
- -|>
- holds at least as long as does.
- Behavior sigma satisfies -|> iff it satisfies
and if rho satisfies then rho satisfies
(for every finite prefix rho of sigma).
- -|> (A() -|> A()
and ( ).
- -|>+
- is guaranteed under assumption .
- holds at least one step longer as does.
- sigma satisfies -|>+ iff
it satisfies and if holds for the first states of
sigma, then holds for the first states of sigma.
- -|>+ (A() -|>+ A()
and ( ).
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine