Temporal Synthesis for Bounded Systems and Environments

Orna Kupferman, Yoad Lustig, Moshe Y. Vardi & Mihalis Yannakakis
Temporal synthesis is the automated construction of a system from its temporal specification. It is by now realized that requiring the synthesized system to satisfy the specifications against all possible environments may be too demanding, and, dually, allowing all systems may be not demanding enough. In this work we study bounded temporal synthesis, in which bounds on the sizes of the state space of the system and the environment are additional parameters to the synthesis...