The Complexity of Bounded Synthesis for Timed Control with Partial Observability
Hans-Jörg Peter and Bernd Finkbeiner
We revisit the synthesis of timed controllers with partial observability. Bouyer et al. showed that timed control with partial observability is undecidable in general, but can be made decidable by fixing the granularity of the controller, resulting in a 2ExpTime-complete problem. We refine this result by providing a detailed complexity analysis of the impact of imposing a bound on the size of the controller, measured in the number of locations. Our results identify which types of bounds are useful (and which are useless) from an algorithmic perspective. While bounding the number of locations without fixing a granularity leaves the problem undecidable, bounding the number of locations and the granularity reduces the complexity to NExpTime-complete. If the controller is restricted to be a discrete automaton, the synthesis problem becomes PSpace-complete, and, for a fixed granularity of the plant, even NP-complete. In addition to the complexity analysis, we also present an effective synthesis algorithm for location-bounded discrete controllers, based on a symbolic fixed point computation. Synthesis of bounded controllers is useful even if the bound is not known in advance. By iteratively increasing the bound, the synthesis algorithm finds the smallest, and therefore often most useful, solutions first.
10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2012).