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