Sloth, Christoffer1; Wisniewski, Rafael5; Pappas, George J.8
1 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN2 The Faculty of Engineering and Science (TECH), Aalborg University, VBN3 Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University, VBN4 Distributed Systems and Semantics, The Technical Faculty of IT and Design, Aalborg University, VBN5 Aalborg University Space Center, The Technical Faculty of IT and Design, Aalborg University, VBN6 Automation & Control, The Technical Faculty of IT and Design, Aalborg University, VBN7 Department of Electronic Systems, The Technical Faculty of IT and Design, Aalborg University, VBN8 University of Pennsylvania, Department of Electrical and Systems Engineering
This paper provides a necessary and sufficient condition for the compositional verification of a continuous system with additively separable barrier functions. The compositional safety verification enables the verification of an interconnection of subsystems. The idea behind the compositional analysis is to allow the verification of systems with a high dimension, by the verification of multiple lower dimensional subproblems. In the compositional safety analysis, a particular structure is imposed on the barrier certificate, restricting the applicability of the method. We show an example of a system that cannot be verified using the compositional method, but can be verified using a centralized method. This example highlights how not to decompose systems, and should be used to guide the decomposition of a system into appropriate subsystems. Finally, we provide a second condition for the compositional safety analysis that enables the verification of the counterexample, by imposing a less restrictive structure of the barrier function. This shows that the counterexample can be solved with a compositional method, but at an increased computational complexity.
I E E E Conference on Decision and Control. Proceedings, 2012, p. 4580-4585
Main Research Area:
51st IEEE Conference on Decision and Control (CDC), 2012