Synthesis of Infinite State Systems
It provides a systematic solution to the synthesis of infinite state systems, which is a foundational problem for verification and control of reactive systems.
The paper tackles the synthesis of infinite state systems, a problem that had no complete or systematic solution, by presenting a systematic study involving the synthesis of MSO-definable parity games and finding MSO-definable uniform memoryless winning strategies.
The classical Church synthesis problem, solved by Buchi and Landweber, treats the synthesis of finite state systems. The synthesis of infinite state systems, on the other hand, has only been investigated few times since then, with no complete or systematic solution. We present a systematic study of the synthesis of infinite state systems. The main step involves the synthesis of MSO-definable parity games, which is, finding MSO-definable uniform memoryless winning strategies for these games.