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:

• Satya Prakash Nayak
• Irmak Sağlam
• Anne-Kathrin Schmuck

Current Collaborators:

• D. Hausmann (Chalmers, Sweden)
• N. Piterman (Chalmers, Sweden)

Past Collaborators:

• Rupak Majumdar (MPI-SWS)
• Kaushik Mallik (IST Austria)
• Mateusz Rychlicki (University of Leeds)
• Sadegh Soudjani (Newcastle University)
• K.S. Thejaswini (IST Austria)

Tools:

• A flexible Toolchain for Symbolic Rabin Games

Publications:

• * D. Hausmann, N. Piterman, I. Sağlam, A.-K. Schmuck. Fair omega-Regular Games. 2024. FoSSaCS’24 (PDF, extended version)
• ® 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 list authors either in alphabetic (indicated by a pink *) or in randomized (indicated by a purple ®) order, with their publicly verifiable record of the randomization available here.