Formal Synthesis of Autonomous Cyber-Physical Systems: Resilience and Security

The ubiquitous development of information technology (IT) infrastructures has greatly enhanced the technological evolution from automated to autonomous Cyber-Physical Systems (CPSs), such as networked mobile robots, autonomous vehicles, intelligent transportation systems, flexible manufacturing systems and so on. Increasing demands for safety, resilience, security and operational efficiency of CPSs have motivated us to pursue a correct-by-construction design methodology. This dissertation is devoted to the study of the resilient and secure coordination and control problems of a class of CPSs that consist of multiple heterogeneous subsystems performing under uncertain environments, and contributions are made to both the theory and designs of provably correct local control policies and coordination rules to achieve complex goals.

By characterizing the cyber logical behaviors of the CPSs as Discrete Event Systems (DESs), we start our study with the supervisory control problems of DESs whose complete plant models are not necessarily given a priori. By modifying L* learning algorithm, we develop learning-based supervisor synthesis algorithms over unknown plant under both complete and partial observation. Furthermore, automatic synthesis methods of decentralized supervisors when the plant is unknown is also considered, and a learning-based algorithm that solves the decentralized supervisory control problem is proposed in terms of language controllability and co-normality. The correctness and finite convergence of the proposed algorithm are proved.

We then investigate the formal coordination and control problem of cooperative multi-agent systems for a regular language specification. We propose an automatic synthesis framework to synthesize appropriate local mission plans and corresponding motion plans for each agent by integrating supervisory control theory and compositional verification techniques. Furthermore, by presenting a modified L* learning algorithm, we are able to reconfigure the synthesized motion plans whenever the real environment is different from the idealized prior knowledge.

Next, the resilience of the proposed coordination and control framework in the presence of potential sensor and/or actuator faults is investigated. The sensor fault tolerant control scheme involves local supervisor reconfiguration upon the detection of the sensor faults, which are captured by permanent loss of observability of certain sensor reading events; while for the actuator faults that are modeled as loss of controllability of local events, a controller switching mechanism is developed for each agent after the detection of the faults. An assume-guarantee post-fault coordination among different subsystems is applied so that fault tolerance can be achieved.

Apart from the high-level performances, we take the dynamics of the robots into consideration and study the path planning problem with application to robotic systems. Based on the mu-tangency conditions, a computationally efficient path planning approach is presented to derive the existence conditions and computationally efficient construction for a class of sub-optimal continuous-curvature paths for nonholonomic mobile robots. The proposed approach not only allows fast determination of the existence of a continuous curvature path, but also guarantees to construct the desired continuous curvature path.


Finally, we also study a confidentiality notion named opacity that characterizes the information-flow between the cyber and the physical parts of an autonomous cyber-physical system within the DES formalism. More specifically, an enforcement mechanism based on the implementation of insertion functions is developed to assure decentralized and joint opacity properties if the system can be observed by multiple intruders either with or without coordination.

The results on simulations on some illustrative examples are given to show that the theory established is correct and the proposed algorithms are efficient.