Active Topics

Hybrid control systems are complex dynamical systems which are composed of both continuous and discrete dynamics. Within such systems, continuous dynamics mainly capture the behavior of physical systems while discrete ones capture the behavior of computational components. Due to versatility and generality of such modeling framework, methods for analysis and design of those systems carry great promises in many safety-critical applications including traffic network, autonomous transportation, building management systems, power networks, energy distribution, air traffic control, and chemical process.

The main research direction of the HyConSys lab focuses on formal verification and synthesis of large-scale hybrid control systems. Here, we list in details the research themes currently active in the lab.

Symbolic control for deterministic hybrid systems

Symbolic models (a.k.a. finite abstractions) play an important role in the verification and control of hybrid systems.They provide abstract descriptions of the continuous-space systems in whicheach discrete state and input correspond to an aggregate of continuous states and inputs of the original system,respectively.

Since symbolic models have finite sets of states and inputs, they allow us to use automata-theoreticmethods to design controllers for hybrid systems with respect to complex logic specifications such as thoseexpressed as linear temporal logic (LTL) formulae. One of the main drawbacks of using symbolic models is the computational complexity due to discretizing sets of states and inputs. In the past few years, we approached this issue using compositionality techniques.[read more].

Automated Verification and Synthesis of Stochastic Cyber-Physical Systems

Decomposition and in(finite) abstractions are two key tools for theanalysis and control of large-scale stochastic systems. Automated controller synthesis forcomplex stochastic systems to achieve some high-level specifications, e.g. those expressedas 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 a replacement inthe 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 analysisand 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 ofits abstraction is well-quantified, one can guarantee that the concrete system also satisfies thesame specifications as the abstract one with guaranteed error bounds.

The computational complexity in synthesizing controllers for large-scale stochastic systemscan be alleviated via abstractions in two consecutive stages. In the first phase, one can abstractthe original system by a simpler one with a lower dimension (infinite abstraction). Then one canconstruct a finite abstraction 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 applicableto synthesize controllers enforcing complex properties over the concrete systems.[read more].

Information-based control

Networked cyber-physical systems often involve digital componentsconnected via communication networks to regulate physical processes inan ongoing interaction of measurement, data processing, and actuation.Use of digital channel (finite bandwidth) between sensor and controllerprevents the instantaneous transmission of an infinite amount of stateinformation. One of the most fundamental research questions in thiscontext is: what is the minimal data rate of the channel so that a givencontrol goal is achievable? Or equivalently: what is the amount of stateinformation (measured in bits per sampling-time) necessarily availableto any controller that enforces a given control task in the closed loop?

In this context information measures, which are known from the theory ofdynamical systems and which are often referred to as entropy, haveproven to be extremely useful. For example, the invariance entropy ofdeterministic control systems characterizes the minimal data rate of acommunication channel between the sensor and the controller, which isnecessary to control a given subset of the state space invariant withrespect to the system behavior. Previous theories have been limited tolinear control systems and deterministic, nonlinear control systems.Data rate constraints for nondeterministic, nonlinear control systemsthat take model uncertainties and disturbances into account cannot beexplained with those theories so far.[read more]

Verification and synthesis of (stochastic) hybrid systems using barrier certificates

Barrier certificates help to provide analysis of the safety of different classes of dynamical systems.Barrier certificates play the analogical role for safety to that of Lyapunov functions for stability.Such certificates have the potential to resolve the issue of so-called curse of dimensionality (i.e.,computational complexity grows exponentially with the dimension of the state set) in formal verificationand synthesis of dynamical systems using discretization-based techniques.

In recent years, there have been many results providing formal verification and synthesis for safety properties.In HyConSys lab, we are interested in utilizing barrier certificate for formalverification and synthesis of (stochastic) hybrid systems against more general classes of high-levelspecifications (e.g. those expressed as linear temporal logic formulae).[read more].

Formal synthesis of networked control systems

Networked control systems (NCS) combine physical components, computing devices,and communication networks all in one system forming a complex and heterogeneousclass of so-called cyber-physical systems (CPS). NCS have attracted significantattentions in the past decade due to their flexibility of deployment and maintenance(especially when using wireless communications). Numerous technical challenges are presentin NCS design and implementation due to the wide ranges of uncertainties withincommunication channels.

Network imperfections in NCS include time-varying communication delays,packet dropouts, time-varying sampling/transmission intervals, and communicationconstraints (e.g. scheduling protocols). The main challenge here is to design controllers enforcing complex objectives over physical plants by taking into account those uncertainties in the communications channels. In HyConSys lab, we are interested insynthesizing formally-verified controllers for NCS. More precisely, we are interestedin designing, algorithmically, controllers for NCS, which are certified-by-construction.[read more]

Secure-by-construction cyber-physical systems

Cyber-physical systems (CPS) are technological backbone of the increasingly interconnected and smartworld where design fault or security vulnerability can be catastrophic. Autonomous vehicles, wearableand implantable medical devices, smart infrastructure and connected communities are some of the highprofile examples that underscore privacy and safety concerns of modern CPS. In the last decade, safetyconcerns have received considerable attention in the design of CPS, while security analysis is left as anafterthought for the later stages. This existing paradigm results in costly and lengthy development of CPSdue to very high security verification and validation costs.

In HyConSys lab, we advocate a paradigm shift in the development of safe and secure CPS by proposing a secure-by-construction controller synthesis scheme by generalizing existing correct-by-constructionsynthesis methods by considering privacy properties in addition to safety ones during the design process.[read more]