Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems

Fair discrete systems (FDSs) are a computational model of concurrent programs where fairness assumptions are specified in terms of sets of states. The analysis of fair discrete systems involves a non-trivial interplay between fairness and well-foundedness (ranking functions). This interplay has been an obstacle for automation. The contribution of this paper is a new analysis of temporal properties of FDSs. The analysis uses a domain of binary relations over states labeled by sets of indices of compassion requirements. The use of labeled relations separates the reasoning on well-foundedness and fairness.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Amir Pnueli, Andreas Podelski, Andrey Rybalchenko
• Keywords: Algorithms, Fair Discrete Systems, Fairness Assumptions, Non-trivial Interplay, TACAS 2005