Example Properties for TLC

Example Properties for TLC

• Invariant : It is never the case that both the highway and farm road have green simultaneously. The CTL formula saying this is

• If a car is waiting on the farm road, then eventually the farm road light turns green. The CTL formula saying this is

AG(!(hwy_light = green * farm_light = green))

AG(car_waiting -> AF(farm_light = green))

Previous slide

Next slide

Back to the first slide

View Graphic Version