Bounded Synthesis for Real-Time Systems

Summary

In bounded synthesis, we fix a bound on the size of the controller, restricting the solutions of interest to just those that meet the bound. Bounded synthesis is useful even if the size of the controller is not known in advance, because the bound can be increased incrementally, guiding the search to the minimal solutions. In this talk, we present recent results on bounded synthesis in the setting of real-time systems. We study the synthesis of timed controllers under partial observability with bounds on the discrete and timed resources of the controller. In addition to decidability and complexity results, indicating which bounds are helpful and which are useless from an algorithmic perspective, we present an effective synthesis algorithm for location-bounded discrete controllers, based on a symbolic fixed point computation.