Synthesis of Implementable Control Strategies for Lazy Linear Hybrid Automata

In the last few years hybrid automata have been widely applied in the modeling and verification of hybrid systems, but their related formal verification techniques usually rely on un-implementable assumptions to which a concrete control strategy cannot adhere. For this reason, once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to derive a correct-by-construction implementable control strategy for such a model. This work discusses a new methodology and a corresponding toolchain that allows to synthesize an implementable control strategy for the class of hybrid automata named Lazy Linear Hybrid Automata (LLHA). LLHA model the discrete time behavior of control systems containing finite-precision sensors and actuators interacting with their environment under bounded delays.