Progress, Justness and Fairness in Modal $\hat{I}¼$-Calculus Formulae

Myrthe Spronck, Bas Luttik, Tim Willemse

When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic execut…