Symbolic Control for Deterministic Hybrid Systems

Symbolic models (a.k.a. finite abstractions) play an important role in the control of hybrid systems. They provide abstract descriptions of the continuous-space systems in which each discrete state and input corresponds to an aggregate of continuous states and inputs of the original system, respectively. Since symbolic models are finite, they allow us to use automata-theoretic methods to design controllers for hybrid systems with respect to logic specifications such as those expressed as linear temporal logic (LTL) formulae. In general, there exist two types of symbolic models: sound ones whose behaviors (approximately) contain those of the concrete systems and complete ones whose behaviors are (approximately) equivalent to those of the concrete systems. Remark that existence of complete symbolic models results in a sufficient and necessary guarantee in the sense that there exists a controller enforcing the desired specifications on the symbolic model if and only if there exists a controller enforcing the same specifications on the original system. On the other hand, a sound symbolic model provides only a sufficient guarantee in the sense that failing to find a controller for the desired specifications on the symbolic model does not prevent the existence of a controller for the original system.

As the complexity of constructing symbolic models grows exponentially in the number of state variables in the concrete system, the existing monolithic approaches on the construction of symbolic models are unfortuntaely limited to only low-dimensional hybrid systems. Motivated by the above limitation, we currently aim at proposing a compositional framework for constructing symbolic models for interconnected hybrid systems. Our methodology is based on a divide-and-conquer scheme. In particular, we first (1) partition the overall concrete system into a number of concrete subsystems and construct symbolic models of them individually; (2) then establish a compositional scheme that allows us to construct a symbolic model of the overall network using those of individual ones. One can leverage the overall constructed symbolic models to synthesize controllers monolithically or also compositionally to achieve some high-level properties. In particular, once symbolic models are constructed for given concrete subsystems, one can design local controllers also compositionally for those symbolic models, and then refine them to the concrete subsystems provided that the given global specification for the overall network is decomposable. Particularly, based on the assume-guarantee reasoning approach, the local controllers are synthesized by assuming that the other subsystems meet their local specifications.

Active group members

The following group members are actively working on this topic:

  • Mahmoud Khaled

  • Abdalla Swikir

  • Majid Zamani

Related publications

The following publications are related to this active topic:

  • A. Swikir and M. Zamani. Compositional synthesis of symbolic models for networks of switched systems. IEEE Control Systems Letters, 3(4), pp. 1056 - 1061, June 2019. (Link),(Preprint).

  • A. Swikir and M. Zamani. Compositional Abstractions of Interconnected Discrete-Time Switched Systems. European Control Conference, 2019, to appear.

  • A. Swikir and M. Zamani. Compositional synthesis of finite abstractions for networks of systems: A small-gain approach. Automatica, 107, pp. 551 - 561, September 2019. (Link),(Preprint).

  • N. Noroozi, A.Swikir, M. Zamani, F. R. Wirth. Compositional construction of abstractions via relaxed small-gain conditions Part II: discrete case. European Control Conference, July 2018, (Link).

  • A. Saoud, P. Jagtap, M. Zamani, and A. Girard. Compositional abstraction-based synthesis for cascade discrete-time control systems. IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), 51(16), pp. 13-18, July 2018.

  • A. Swikir, A. Girard, and M. Zamani. From dissipativity theory to compositional synthesis of symbolic models. The 4th Indian Control Conference, January 2018, to appear. (Best student paper award finalist). (Link).

Related software

The following software tools are related to this topic:

  • SCOTS: A Tool for the Synthesis of Symbolic Controllers.

  • QUEST: A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers.