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 heterogeneous class of so-called cyber-physical systems (CPS). NCS have attracted significant attentions in the past decade due to their flexibility of deployment and maintenance (especially when using wireless communications). Nmerous technical challenges are present in NCS design and implementation due to the wide range of uncertainties within communication channels in NCS.

Network imperfections in NCS include time-varying communication delays, packet dropouts, time-varying sampling/transmission intervals, and communication constraints (e.g. scheduling protocols). The main challenge in NCS, compared to non-networked systems, is to control remotely located systems through unreliable communication channels. In HyConSys, we are interested in studying and analyzing NCS from the point view of formal methods. More preciesly, we are interested in designing algorithmically controllers for NCS, which are certified-by-construction.

The following are the main components constituting NCS:

• a control system (a.k.a. plant) representing a physical process to be controlled;

• two non-ideal communication channels: a sensor-to-controller channel that transfers sampled and quantized state information, and a controller-to-actuator channel that transfers control inputs; and

• a remote digital controller enforcing some complex specifications on the plant in NCS by taking into account the imperfections of the communication channels.

One promising approach to algorithmically synthesize formally-verified controllers for NCS enforcing complex high-level specifications is based on so-called symbolic models. For NCS, we need to construct those symbolic models by taking into account not only the description of the plants but also the network characteristics.

Active lab members

The following lab members are actively working on this topic:

• Mahmoud Khaled

• Majid Zamani

Related publications

The following publications are related to this active topic:

• M. Zamani, M. Mazo Jr, M. Khaled, and A. Abate. Symbolic abstractions of networked control systems. IEEE Transactions on Control of Network Systems, 5(4), pp. 1622-1634, December 2018. (Preprint)

• M. Khaled, M. Rungger, and M. Zamani. Abstraction-based synthesis of networked control systems. Electronic Proceedings in Theoretical Computer Science (EPTCS), 272, pp. 65-78, June 2018.

• M. Khaled, M. Rungger, and M. Zamani. Symbolic models of networked control systems: A feedback refinement relation approach. The 54th Annual Allerton Conference on Communication, Control, and Computing, pp. 187-193, September 2016

• M. Zamani, M. Mazo Jr, and A. Abate. Finite abstractions of networked control systems. The 53rd IEEE Conference on Decision and Control, pp. 95-100, December 2014. (Invited paper)

Related software

The following software tools are related to this active topics:

• SENSE: A tool for abstraction-based contoller synthesis for networked control systems.