Discrete Controller Synthesis for Infinite State Systems

In relation with my work on control techniques for clouds management, discrete controller synthesis techniques needed to be augmented so as to handle quantitative aspects of managed systems (e.g., power consumption, workloads), as well as to be able to enforce properties about such quantities. In effect, existing techniques and tools performing discrete controller synthesis on synchronous programs (Sigali) need to be extended in order to handle infinite state systems (e.g., programs comprising real or integer variables). I worked (and am still working) on such extensions with Hervé Marchand.

These investigations have led to the development of the tool ReaX. It is distributed as part of the Reactive Systems Verification and Synthesis ToolKit (ReaTK), available in my OPAM repository.


General Search Techniques for Discrete Controller Synthesis