Control and Diagnosis of Safety-Critical Complex Cyber-Physical Systems

---

This is the wiki for the NSF CPS Breakthrough project: Development of Novel Architectures for Control and Diagnosis of Safety-Critical Complex Cyber-Physical Systems

PI: Stéphane Lafortune

Co-PI: Necmiye Ozay

This project is developing novel architectures for control and diagnosis of complex cyber-physical systems subject to stringent performance requirements in terms of safety, resilience, and adaptivity. These ever-increasing demands necessitate the use of formal model-based approaches to synthesize provably-correct feedback controllers. The intellectual merit of this research lies in a novel combination of techniques from the fields of dynamical systems, discrete event systems, reactive synthesis, and graph theory, together with new advancements in terms of abstraction techniques, computationally efficient synthesis of control and diagnosis strategies that support distributed implementations, and synthesis of acquisition of information and communication strategies. The project’s broader significance and importance are demonstrated by the expected improvement of the safety, resilience, and performance of complex cyber-physical systems in critical infrastructures as well as the efficiency with which they are designed and certified.

The original approach being developed is based on the combination of multi-resolution abstraction graphs for building discrete models of the underlying cyber-physical system with reactive synthesis techniques that exploit a representation of the solution space in terms of a finite structure called a decentralized bipartite transition system. The concepts of abstraction graph and decentralized bipartite transition system are novel and open new avenues of investigation with significant potential to the formal synthesis of safe, resilient, and adaptive controllers. This methodology naturally results in a set of decentralized and asynchronous controllers and diagnosers, which ensures greater resilience and adaptivity. Overall, this research will significantly impact the Science of Cyber-Physical Systems and the Engineering of Cyber-Physical Systems.

Research supported by: NSF CPS program, award number: 1446298.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Publications

Journal Papers

• L. Yang, O. Mickelin, and N. Ozay, “On sufficient conditions for mixed monotonicity”, IEEE Transactions on Automatic Control, (to appear in December 2019).
• P. Nilsson and N. Ozay, “Control Synthesis for Permutation-Symmetric High-Dimensional Systems With Counting Constraints”, IEEE Transactions on Automatic Control, (to appear in February 2020).
• X. Yin and S. Lafortune, “Verification Complexity of a Class of Observational Properties for Modular Discrete Event Systems”, Automatica, vol. 83, pp. 199-205, September 2017.
• X. Yin and S. Lafortune, “On the Decidability and Complexity of Diagnosability for Labeled Petri Nets”, IEEE Transactions on Automatic Control, vol. 62, no. 11, pp. 5931-5938, November 2017.
• X. Yin and S. Lafortune, “Synthesis of maximally-permissive supervisors for the range control problem”, IEEE Transactions on Automatic Control, vol. 62, no. 8, pp. 3914-3929, August 2017.
• P. Nilsson, N. Ozay, and J. Liu, “Augmented Finite Transition Systems as Abstractions for Control Synthesis”, Journal of Discrete Event Dynamic Systems (Special issue on Formal Methods in Control), 27(2), 301-340, June 2017.
• X. Yin and S. Lafortune, “Decentralized supervisory control with intersection-based architecture”, IEEE Transactions on Automatic Control, vol. 61, no. 11, pp. 3644-3650, November 2016.
• J. Liu and N. Ozay, “Finite abstractions with robustness margins for temporal logic-based control synthesis”, Nonlinear Analysis: Hybrid Systems, Vol. 22: 1-15, November 2016.
• X. Yin and S. Lafortune, “A uniform approach for synthesizing property-enforcing supervisors for partially-observed discrete-event systems”, IEEE Transactions on Automatic Control, vol. 61, no. 8, pp. 2140-2154, August 2016.
• X. Yin and S. Lafortune, “Synthesis of maximally permissive supervisors for partially observed discrete event systems”, IEEE Transactions on Automatic Control, vol. 61, no. 5, pp. 1239-1254, May 2016.
• X. Yin and S. Lafortune, “Codiagnosability and coobservability under dynamic observations: Transformation and verification”, Automatica, vol. 61, pp. 241-252, 2015.

Conference Papers

• G. Chou, D. Berenson, and N. Ozay, “Learning Constraints from Demonstrations”, Proc. 13th International Workshop on the Algorithmic Foundations of Robotics (WAFR), Merida, Mexico, December 2018.
• L. Yang and N. Ozay, “Fault-tolerant output-feedback path planning with temporal logic constraints”, Proc. 57th IEEE Conference on Decision and Control (CDC), Miami Beach, FL, December 2018.
• Y. E. Sahin, N. Ozay, and S. Tripakis, “Multi-Agent Coordination Subject to Counting Constraints: A Hierarchical Approach“, Proc. Int. Symp. on Distributed Autonomous Robotic Systems (DARS), Boulder, CO, October 2018.
• O. Bulancea Lindvall, P. Nilsson, and N. Ozay, “Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings”, Proc. 6th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Oxford, UK, July 2018.
• Y. E. Sahin, P. Nilsson, and N. Ozay, “Synchronous and Asynchronous Multi-agent Coordination with cLTL+ Constraints”, Proc. 56th IEEE Conference on Decision and Control (CDC), Melbourne, Australia, December 2017.
• P. Nilsson and N. Ozay, “Maximizing the Time of Invariance for Large Collections of Switched Systems”, Proc. 56th IEEE Conference on Decision and Control (CDC), Melbourne, Australia, December 2017.
• R. Hill and S. Lafortune, “Scaling the Formal Synthesis of Supervisory Control Software for Multiple Robot Systems”, Proc. of the 2017 American Control Conference, pp. 3840-3847, July 2017.
• X. Yin, M. Morrison, S. Sheng, and S. Lafortune, “DPO-SYNT: Discrete Control Synthesis for Partially-Observed Systems”, Proceedings of the 20th IFAC World Congress, pp. 6026-6029, July 2017.
• Y. E. Sahin, P. Nilsson, and N. Ozay, “Provably-correct coordination of large collections of agents with counting temporal logic constraints”, 8th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Pittsburgh, April 2017.
• P. Nilsson and N. Ozay, “On a class of maximal invariance inducing control strategies for large collections of switched systems”, 20th International Conference on Hybrid Systems: Computation and Control (HSCC), Pittsburgh, April 2017.
• X. Yin and S. Lafortune, “On the maximally-permissive range control problem in partially-observed discrete event systems”, Proc. 55th IEEE Conference on Decision and Control (CDC), Las Vegas, NV, December 2016.
• R. Hill and S. Lafortune, “Hierarchical Planning within a Supervisory Control Context”, Proc. 55th IEEE Conference on Decision and Control (CDC), Las Vegas, NV, December 2016.
• S. Smith, P. Nilsson, and N. Ozay, “Interdependence quantification for compositional control synthesis with an application in vehicle safety systems”, Proc. 55th IEEE Conference on Decision and Control (CDC), Las Vegas, NV, December 2016.
• A. Wagenmaker and N. Ozay, “A bisimulation-like algorithm for abstracting control systems”, Proc. Allerton Conference on Communication, Control, and Computing, Monticello, IL, September 2016.
• Y. E. Sahin and N. Ozay, “SAT-based Distributed Reactive Control Protocol Synthesis for Boolean Networks”, Proc. Multi-conference on Systems and Control (MSC), Buenos Aires, September 2016.
• I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay, and R. M. Murray “Control design for hybrid systems with TuLiP: The temporal logic planning toolbox”, Proc. Multi-conference on Systems and Control (MSC), Buenos Aires, September 2016.
• P. Nilsson and N. Ozay, “Synthesis of separable controlled invariant sets for modular local control design”, Proc. American Control Conference (ACC), Boston, MA, July 2016.
• L. Yang, N. Ozay, and A. Karnik “Synthesis of Fault Tolerant Switching Protocols for Vehicle Engine Thermal Management”, Proc. American Control Conference (ACC), Boston, MA, July 2016.
• X. Yin and S. Lafortune, “On maximal permissiveness in partially-observed discrete event systems: Verification and synthesis”, Proc. 13th International Workshop on Discrete Event Systems (WODES), Xi’an, China, May 2016.
• P. Nilsson and N. Ozay, “Control synthesis for large collections of systems with mode-counting constraints”, 19th International Conference on Hybrid Systems: Computation and Control (HSCC), Vienna, April 2016.
• X. Yin and S. Lafortune, “A general approach for solving dynamic sensor activation problems for a class of properties”, Proc. 54th IEEE Conference on Decision and Control (CDC), Osaka, Japan, December 2015.
• X. Yin and S. Lafortune, “Minimization of sensor activation in decentralized fault diagnosis of discrete event systems”, Proc. 54th IEEE Conference on Decision and Control (CDC), Osaka, Japan, December 2015.
• X. Xu, N. Ozay, and V. Gupta, “Passivity degradation in discrete control implementations: An approximate bisimulation approach”, Proc. 54th IEEE Conference on Decision and Control (CDC), Osaka, Japan, December 2015.
• Y. Li, J. Liu, and N. Ozay, “Computing finite abstractions with robustness margins via local reachable set over-approximation”, Proc. 5th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Atlanta, GA, October 2015.
• X. Yin and S. Lafortune, “On the relationship between codiagnosability and coobservability under dynamic observations”, Proc. 2015 American Control Conference (ACC), Chicago, USA, July, pp. 390-395, 2015.

Book Chapters

• P. Nilsson and N. Ozay, “Provably-Correct Compositional Synthesis of Vehicle Safety Systems” in Safe, Autonomous and Intelligent Vehicles as part of Springer’s Unmanned System Technologies series, Yu, H., Li, X., Murray, R.M., Ramesh, S., Tomlin, C.J. (Eds.).