LTL model checking under fairness in ProB

Abstract

Model checking of liveness properties often results in unrealistic, unfair infinite behaviors as counterexamples. Fairness is a notion where the search is constrained to infinite paths that do not ignore infinitely the execution of a set of enabled actions. In this work we present an implementation for efficient checking of LTL formulas under strong and weak fairness in ProB, available for model checking B, Event-B, Z, CSP and CSP‖B models. The fairness checking algorithm can cope with both weak and strong fairness conditions, where the respective fairness conditions can be joined by means of the logical operators for conjunction and disjunction, which makes setting up and checking fairness to a property more flexible. We evaluate the implementation on various CSP models and compare it to t he fairness implementation of the PAT tool.