On-the-fly controller synthesis for discrete and dense-time systems

Abstract

We present novel techniques for efficient controller synthesis for untimed and timed systems with respect to invariance and reachability properties. In the untimed case, we give algorithms for controller synthesis in the context of finite graphs with controllable and uncontrollable edges, distinguishing between the actions of the system and its environment, respectively. The algorithms are on-the-fly, since they return a controller as soon as one is found, which avoids the generation of the whole state space. In the timed case, we use the model of timed automata extended with controllable and uncontrollable discrete transitions. Our controller-synthesis method here is only half on-the-fly, since it relies on the a-priori generation of a finite model (graph) of the timed automaton, as quotient of the time-abstracting bisimulation. The quotient graph is essentially an untimed graph, upon which we can apply the untimed on-the-fly algorithms to compute a timed controller.