Building bridges in abstraction-based controller synthesis
Anne-Kathrin Schmuck · DepositOnce · 2015
Abstraction based controller synthesis is a well established two-step procedure to solve complex control problems involving discrete valued quantities. First, a symbolic abstraction of the system to be controlled is generated providing a discrete time model with a finite, discrete valued signal space and finitely many states. Second, a symbolic controller for a desired symbolic specification is constructed using the previously generated symbolic model. This controller synthesis approach is usually used in two different settings. Either (i) the specification is naturally given by a Linear Temporal Logic (LTL) or a Computation Tree Logic (CTL) formula over a finite set of symbols, which can only be encountered by symbolic controller synthesis techniques. Or (ii) the system to be controlled is naturally equipped with a finite set of external symbols through which it interacts with its environment, e.g., the controller. For each of the two settings specific approaches to solve the synthesis problem have been proposed independently. In Part I of this thesis we will investigate the abstraction step of two different approaches, namely quotient based abstractions (QBA) and strongest asynchronous l-complete approximations (SAlCA), tailored to setting (i) and (ii), respectively. It will be shown that the resulting abstractions are generally incomparable. We will therefore derive necessary and sufficient conditions on the original system which allow for a detailed comparison. This builds our first bridge between the computer science community, which inspired the construction of QBA and the control systems community, where SAlCA were developed. When the second setting is considered where the use of abstraction based controller synthesis is motivated by the symbolic input-output structure of the system, the desired specification might not naturally be symbolic. However, to apply supervisory control theory (SCT), a framework for symbolic controller synthesis commonly used in combination with SAlCA, the specification is required to be modelled by a deterministic finite automaton (DFA). This motivates the investigation of larger specification classes to enrich the applicability of abstraction based controller synthesis in setting (ii). In Part II of this thesis we show that SCT can be extended to handle specifications realized by deterministic pushdown automata (DPDA). This builds our second bridge between the computer science community, where different automata models, such as DFA and DPDA, are formalized and the control systems community, where SCT was developed.