An Efficient Subclass of Fairness in Games on Graphs: Theory and Gadget-Based Algorithms

Two-player games on finite graphs are a central modeling tool in formal 
verification and synthesis, particularly for designing reactive software 
and hardware systems. They enable the finite abstraction of infinite 
computational behaviors, where the challenge often lies in capturing 
realistic assumptions without overcomplicating the model.

Fairness constraints serve this purpose by encoding assumptions about 
the environment’s behaviour to avoid unrealistic scenarios. Fairness, in 
the general sense, ensures that if certain actions (e.g. edges) remain 
perpetually available, then certain other actions (e.g. edges) are 
eventually taken. This general form of fairness is represented by 
Streett conditions. However, games with Streett conditions are known to 
be coNP-complete, or even harder when added to existing objectives.

In this talk, I will introduce strong transition fairness, a syntactic 
restriction of Streett fairness that retains significant modeling power 
while allowing for a much more efficient algorithmic treatment. Strong 
transition fairness ensures that certain actions (e.g. edges) that 
remain perpetually available are eventually taken. This form of fairness 
appears naturally across a range of domains, including model checking, 
scheduler synthesis, resource management, cyber-physical system design 
and robot motion planning. We show that strong transition fairness can 
be added to many commonly studied objectives—such as safety, 
reachability, Büchi, parity, Rabin, mean-payoff, and energy—without 
changing their complexity class. This makes it both a practical and 
theoretically appealing tool for system design.

We will introduce gadget-based techniques that reduce games with strong 
transition fairness to games with simpler objectives, without blowing up 
the state space. These reductions underpin the theoretical results 
mentioned above. Furthermore, using these gadgets, we obtain 
progress-measure-based algorithms for games under strong transition 
fairness. We will show the efficiency and relevance of such algorithms 
for Büchi and co-Büchi games under strong transition fairness.