Strategy Repair on Parity Games using Semantic Information and Machine Learning

Tereza Kinská

Masaryk University

LTL-Synthesis [4],i.e. the problem of automatically constructing a correct-by-construction controller from a given specification in Linear Temporal Logic [3], is a fundamental problem in formal methods with applications in the design of safety-critical systems.

One of the established state-of-the-art tools for LTL Synthesis is SemML [2]. The synthesis pipeline of SemML starts with an LTL formula, which is translated into an automaton and subsequently into a parity game [1]. Solving the game then yields a winning strategy. The first step, i.e. translating an LTL formula into an automaton, is one of the standard approaches in LTL synthesis [6]. However, the usual approaches used determinisation procedures, e.g. by Safra [5], to obtain a desired deterministic parity automaton, which can be up to doubly exponential in the size of the input LTL formula. SemML, on the other hand, uses a direct translation that follows the logical structure of the formula, which results in a more compact automaton and keeps the semantical information by construction.

When computing winning regions during the strategy synthesis from the parity game, since synthesising the whole strategy directly is expensive and in some cases infeasible, SemML explores the important game parts and builds the strategy on the fly, achieving better scalability. However, heuristic-guided synthesis does not guarantee optimality in the initial attempt, and the resulting strategy may require repair or refinement.

In our ongoing work with Jan Křetínský and Max Prokop, we focus on the problem of strategy repair: given a suboptimal strategy, we aim to improve it using semantic information gathered during synthesis and ML techniques. By exploiting this information, we seek to identify the regions of the strategy that are likely suboptimal and focus repair efforts on those areas, directing the optimal strategy search and saving resources.

  1. Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy. In: FoCS’91: The 32nd Annual Symposium on Foundations of Computer Science, pp. 368–377. IEEE Computer Society Press (1991)
  2. Křetínský, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: SemML: Enhancing automata-theoretic LTL synthesis with machine learning. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 233–253. Springer (2025)
  3. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pp. 46–57. IEEE Computer Society (1977)
  4. Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, pp. 652–671. Springer (1989)
  5. Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, pp. 319–327 (1988)
  6. Thomas, W.: On the synthesis of strategies in infinite games. In: 12th Annual Symposium on Theoretical Aspects of Computer Science, pp. 1–13. Springer (1995)