Symbolic Controller Synthesis for Discrete and Timed Systems.
This paper presents algorithms for the symbolic
synthesis of discrete and real-time controllers. At the semantic level
the controller is synthesized by finding a winning strategy for certain
games defined by automata or by timed-automata. The algorithms for finding
such strategies need, this way or another, to search the state-space of
the system which grows exponentially with the number of components. Symbolic
methods allow such a search to be conducted without necessarily enumerating
the state-space. This is achieved by representing sets of states using
formulae (syntactic objects) over state variables. Although in the worst
case such methods are as bad as enumerative ones, many huge practical problems
can be treated by fine-tuned symbolic methods. In this paper the scope
of these methods is extended from analysis to synthesis and from purely
discrete systems to real-time systems.
We believe that these results will pave the way for the application of program synthesis techniques to the construction of real-time embedded systems from their specifications and to a solution of other related design problems associated with real-time systems in general and asynchronous circuits in particular.
In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid System II, volume 999 of Lecture Notes in Computer Science. Springer-Verlag, 1995.