Beyond SafetyTest automata
Bounded Liveness Properties
F ::= F UNTIL<t P
F holds until P and P holds before t
Testing Automata TF UNT P
x<=t
bad
x:=0
x=t
‘P’
TF
Now
SYS sat F Unt<tP
iff
SYS | T sat
A[] not T.bad
TACAS98
Previous slide
Next slide
Back to first slide
View graphic version