|
|
|||||
|
Complex software-controlled physical systems such as robots are fundamentally hybrid in character, in that their state or configuration exhibits both discrete dynamics - step-wise or event-driven changes of state, occurring at discrete points in time, and also continuous dynamics - evolution in continuous time according to the laws of motion or other dynamic laws modelled by differential equations. This hybrid phenomena is manifested in a huge diversity of engineering applications, including air traffic control systems, unmanned vehicles, industrial process control, and everyday items like cars and consumer electronics. It is the combination and interaction of the discrete and continuous that makes this emerging area a particularly challenging field of research.
A digital control program for a hybrid system must decide which of a finite number of continuous control actions are to be effected on an underlying physical process, based on discrete input data recording which of a finite number of regions contain the current process state. The task of a synthesis procedure is to construct a control program so that the resulting closed-loop hybrid system is guaranteed to satisfy a given specification of desired behaviour.
Previous logic-based work on hybrid systems has almost exclusively focused on the problem of "after-the-fact" verification that a completed system design satisfies a specification. In this project, we use the framework of modal logic to formalise the steps in the process of building a solution control program, with the direct benefit that we can give a formal proof within logic that our solutions are correct with respect to their given specifications. The key idea is to exploit the semantic correspondence between modal logic formulas and regions of the system state space.
Davoren, J.M., Coulthard, V., Moor, T., Gore, R.P., Nerode, A.: Topological semantics for Intuitionistic modal logics, and spatial discretisation by A/D maps, Intuitionistic Modal Logic and Aplications (IMLA) at The 2002 Federated Logic Conference (FLoC), Copenhagen, Denmark, 2002.
Moor, T., Davoren, J.M.: Robust controller synthesis for hybrid systems using modal logic, in Di Benedetto, M. D., Sangiovanni-Vincentelli, A. (eds) Hybrid Systems: Computation and Control (HSCC 2001), LNCS 2034, pp. 433-446, Springer-Verlag, 2001. [PDF] (© Springer-Verlag)
From an engineering perspective, there is a natural interest in the design of hybrid systems. Consider the case in which the continuous dynamics are given and the task is to synthesise a discrete-event supervisor that enforces a certain performance specification. A nearby approach to this type of problem is to substitute the continuous plant dynamics by a discrete-event abstraction. In our earlier work, we prove that any supervisor that enforces the specification on the abstraction level will also do so when interconnected with the original hybrid plant. This effectively reduces the hybrid design problem to the construction of a discrete abstraction. However, there are a number of open questions.
Clearly, for a too coarse abstraction there will exist no supervisor that enforces the specification. On the other hand, the finer an abstraction one wants to construct, the more computationally involved one expects this enterprise to be. We ask: given plant and closed-loop specification, does there exist an abstraction that is just fine enough to allow for successful supervisory synthesis? how can one successively refine an abstraction while learning about the aspects of the plant that are most relevant for the particular control problem at hand?
The computational construction of abstractions is based on reachability analysis under state constraints. The latter is well understood only for the most trivial continuous dynamics, and, in general, intractable for higher order or nonlinear systems. However, in an engineering context, it is reasonable to assume that the continuous dynamics model not only a physical, biological or chemical plant but also suitable low-level continuous controllers. How can one exploit this fact in the reachability analysis? How can one design the continuous controller to facilitate the reachability analysis without compromising the continuous closed-loop performance?
Moor T., Schmidt K., Wittmann Th.: Abstraction-based control for not necessarily closed behaviours, Preprints of the 18th IFAC World Congress Milano (Italy), pp. 6988-6993, 2011. [PDF] (technical report incl. proofs available on request).
Moor, T., Davoren, J.M., Raisch, J.: Strategic refinements in abstraction based supervisory control of hybrid systems, Proc. 6th International Workshop on Discrete Event Systems (WODES), pp. 329-334, Zaragoza, Spain, 2002. [PDF]
Moor, T., Raisch, J.: Abstraction based supervisory controller synthesis for high order monotone continuous systems. In Engell, S., Frehse, G., Schnieder, E. (Eds): Modelling, Analysis, and Design of Hybrid Systems, LNCIS 279, pp. 247-265, Springer-Verlag, 2002. [PDF] (© Springer-Verlag)
The computational resources that are required for the (off-line) design of a hybrid control system are quite considerable, and one can argue that most real-world application would be intractable. A promising strategy is to investigate particular control architectures and thereby to divide the overall design task into a number of feasible subproblems and to compose their individual solutions. Configurations that are common in large scale engineering systems are based on a hierarchical and/or modular composition of subsystems. Although these architectures have been investigated for discrete-event systems, there remain many open questions [see also: here] and only very little is known about compositional properties of hybrid systems that could be exploited in a systematic design.
Modular control architectures aim for a largely independent discussion of individual components. How and under which conditions can multiple controllers be combined in order to achieve the individual control objectives simultaneously? When a discrete supervisor is meant to control a number of continuous subsystems, how can one efficiently combine individual abstractions of the continuous subsystems rather than first combining the subsystems and then seeking for an abstraction?
On each level in a hierarchical control architecture, a controller implements control objectives based on the services provided by the controller on the level below. The key questions are: is there a systematic way to derive suitable levels of abstraction, or is one left with engineering intuition? how can on extract control objectives for the individual levels from an overall specification? how can one solve the resulting control problems on the individual levels?
For an illustration, see our [case study: delivery service]
Moor, T., Raisch, J., Davoren, J.M.: Admissibility criteria for a hierarchical design of hybrid control systems, Proc. ADHS, Saint Malo, France, 2003. [PDF]
Moor, T., Raisch, J., Davoren, J.M.: Computational advantages of a two-level hybrid control architecture, Proc. 40th IEEE Conference on Decision and Control, pp. 358-363, Orlando, USA, 2001. [PDF]