Go backward to Additional Temporal Operators
Go up to Top
Go forward to References
Further Propositions
- safety properties:
- -|>+ -|>+ ( containing all
free varaibles of )
- _|_ ( and ) -|>+ (
or )
- Proposition 4
- , , safety properties.
- containing all free variables of .
- (|= and ) and (|=
_|_ ) imply (|= and ).
- Use orthogonality to remove .
- Proposition 5
- Assume |= A() = and always [A]
- Assume |= A() = and always [A]
- Then |= (exists : or exists : )
and (,)
A(exists : ) _|_ A(exists : )
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine