Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis

TL;DR

This paper introduces semantic labelling to enhance parity game solving in LTL synthesis, leading to better initial strategies, smaller solutions, and competitive learning-based methods, thereby improving the efficiency of strategy synthesis.

Contribution

It presents a novel semantic labelling technique that provides additional information for parity game states, improving initialization and learning-based strategy improvement methods in LTL synthesis.

Findings

Semantic labelling improves initial strategy quality.

It results in smaller parity game solutions.

Q-learning with semantic information becomes competitive to strategy improvement.

Abstract

We propose "semantic labelling" as a novel ingredient for solving games in the context of LTL synthesis. It exploits recent advances in the automata-based approach, yielding more information for each state of the generated parity game than the game graph can capture. We utilize this extra information to improve standard approaches as follows. (i) Compared to strategy improvement (SI) with random initial strategy, a more informed initialization often yields a winning strategy directly without any computation. (ii) This initialization makes SI also yield smaller solutions. (iii) While Q-learning on the game graph turns out not too efficient, Q-learning with the semantic information becomes competitive to SI. Since already the simplest heuristics achieve significant improvements the experimental results demonstrate the utility of semantic labelling. This extra information opens the door to more advanced learning approaches both for initialization and improvement of strategies.