Contract composition for dynamical control systems: Definition and verification using linear programming

Miel Sharf*, Bart Besselink, Karl Henrik Johansson

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

11 Downloads (Pure)

Abstract

Designing large-scale control systems to satisfy complex specifications is hard in practice, as most formal methods are limited to systems of modest size. Contract theory has been proposed as a modular alternative, in which specifications are defined by assumptions on the input to a component and guarantees on its output. However, current contract-based methods for control systems either prescribe guarantees on the state of the system, going against the spirit of contract theory, or are not supported by efficient computational tools. In this paper, we present a contract-based modular framework for discrete-time dynamical control systems. We extend the definition of contracts by allowing the assumption on the input at a time k to depend on outputs up to time k−1, which is essential when considering feedback systems. We also define contract composition for arbitrary interconnection topologies, and prove that this notion supports modular design, analysis and verification. This is done using graph theory methods, and specifically using the notions of topological ordering and backward-reachable nodes. Lastly, we present an algorithm for verifying vertical contracts, which are claims of the form “the conjunction of given component-level contracts implies given contract on the integrated system”. These algorithms are based on linear programming, and scale linearly with the number of components in the interconnected network. A numerical example is provided to demonstrate the scalability of the presented approach, as well as the modularity achieved by using it.

Original languageEnglish
Article number111637
Number of pages15
JournalAutomatica
Volume164
Early online date29-Mar-2024
DOIs
Publication statusPublished - Jun-2024

Keywords

  • Contracts
  • Formal methods
  • Graph theory
  • Interconnection topology
  • Linear programming
  • Modular design

Fingerprint

Dive into the research topics of 'Contract composition for dynamical control systems: Definition and verification using linear programming'. Together they form a unique fingerprint.

Cite this