Counterexample-guided synthesis of observation predicates

Abstract. We present a novel approach to the safety controller synthesis prob-lem with partial observability for real-time systems. This in general undecidable problem can be reduced to a decidable one by fixing the granularity of the con-troller: finite sets of clocks and constants in the guards. Current state-of-the-art methods are limited to brute-force enumeration of possible granularities or man-ual choice of a finite set of observations that a controller can track. We address this limitation by proposing a counterexample-guided method to successively re-fine a set of observations until a sufficiently precise abstraction is obtained. The size of the abstract games and strategies generated by our approach depends on the number of observation predicates and not on the size of the constants in the plant. Our experiments demonstrate that this results in better performance than the approach based on fixed granularity when fine granularity is necessary.