Automated Verification and Synthesis of Stochastic Cyber-Physical Systems

Automated controller synthesis for complex stochastic systems to achieve some high-level specifications, e.g. those expressed as linear temporal logic (LTL) formulae, is inherently very challenging. To reduce this complexity, one promising approach is to employ (in)finite abstractions of given systems as replacements in the controller synthesis procedure. In this regard, one can first abstract the original (concrete) system by a simpler one (with possibly lower dimension or finite state set), then perform analysis and synthesis over the abstract model, and finally carry the results back (via an interface map) over the concrete system. Since the mismatch between outputs of the original system and that of its abstraction is well-quantified, one can guarantee that the concrete system also satisfies the same specifications as the abstract one with guaranteed error bounds.

The computational complexity in synthesizing controllers for large-scale stochastic systems can be alleviated via abstractions in two consecutive stages. In the first phase, one can abstract the original system by a simpler one with a lower dimension (infinite abstraction). Then one can construct a finite abstraction as an approximate description of the (reduced-order) system in which each discrete state corresponds to a collection of continuous states of the (reduced-order) system. Since the final abstractions are finite, algorithmic machineries from computer science are applicable to synthesize controllers enforcing complex properties over the concrete systems.

Unfortunately, construction of (in)finite abstractions for large-scale stochastic systems in a monolithic manner suffers severely from the curse of dimensionality. To mitigate this issue, our proposed solution is to consider the large-scale stochastic system as an interconnected system composed of several smaller subsystems, and provide a compositional framework for the construction of (in)finite abstractions for the given system using abstractions of smaller subsystems.

Active Group Members

The following group members are actively working on this topic:

  • Abolfazl Lavaei

  • Majid Zamani

Related Publications

The following publications are related to this active topic: