Taming Fairness in Two-Player Games

 

Two-player games over finite graphs arise from many core computational problems in the context of correct-by-construction synthesis of reactive software or hardware. In particular, they have been extensively used in the context of cyber-physical system design to build correct-by-construction control software for temporal logic objectives.
Fairness, on the other hand, is a property that widely occurs in this context – both as a desired property to be enforced (e.g., requiring a synthesized scheduler to fairly serve its clients), as well as a common assumption on the behavior of other components (i.e., assuming the network to always eventually deliver a data packet).
While strong fairness encoded by a Streett condition necessarily incurs a high additional cost in synthesis we show in this line of work that strong transition fairness (a local version of fairness) can be handled efficiently in game solving, with almost no additional computational overhead.

Group Members Involved:

Collaborators:

Tools:

Publications:

  • D. Hausmann, N. Piterman, I. Sağlam, A.-K. Schmuck. Fair omega-Regular Games. exp. 2024. FoSSaCS (to appear, Axiv preprint)
  • ® A.-K. Schmuck, K.S. Thejaswini, I. Sağlam, S.P. Nayak. Solving Two-Player Games
    under Progress Assumptions.     2024. VMCAI. (PDF, extended version)
  • I. Saglam, A.-K. Schmuck. Solving Odd-Fair Parity Games. 2023. FST&TCS. (PDF, extended version)
  • R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani. A Flexible  Toolchain for Symbolic Rabin Games under Fairness and Stochastic Uncertainties. 2023. CAV’23. (PDF, HSCC poster)
  • T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani. Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness. 2022. TheoretiCS. (PDF, ArXiv Preprint) (Acceptance rate: 12,5%)

all publications either list authors in alphabetic or randomized order.