Synthesis of succinct systems

摘要

Synthesis of correct by design systems from specifications has recently attracted a lot of attention. The theoretical results imply that this problem is highly intractable. For example, synthesizing a system is 2EXPTIME-complete for an LTL specification and EXPTIME-complete for CTL. An argument in favour of synthesis is that temporal specifications are highly compact, and the complexity reflects the large size of the system constructed. A careful observation reveals that the size of the system is presented in such arguments as the size of its state space. This view is slightly biased, in that the state space can be exponentially larger than the size of a reasonable implementation like a circuit or program. This raises the question if there exists a small bound on the circuits or programs. We show that small succinct model theorems depend on the collapse of complexity classes, e.g., of PSPACE and EXPTIME for CTL.