On the existence of compositional barrier certificates

Christoffer Sloth*, Rafael Wisniewski, George J. Pappas

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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.

Original languageEnglish
Title of host publicationIEEE Annual Conference on Decision and Control (CDC)
Publication date2012
Publication statusPublished - 2012
Externally publishedYes
SeriesIEEE Conference on Decision and Control. Proceedings


Dive into the research topics of 'On the existence of compositional barrier certificates'. Together they form a unique fingerprint.

Cite this