Synthesis of Infinite State Systems
Ohad Drucker, Alexander Rabinovich
TL;DR
This paper systematically studies the synthesis of infinite state systems, focusing on MSO-definable parity games to find uniform memoryless winning strategies, extending classical finite state synthesis methods.
Contribution
It introduces a systematic approach for synthesizing infinite state systems using MSO-definable parity games, filling a gap in existing research.
Findings
Develops a method for synthesizing infinite state systems
Uses MSO logic to define parity games for synthesis
Provides a framework for uniform memoryless strategies
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · History and advancements in chemistry · Quantum Mechanics and Applications