A Contract Theory for Layered Control Architectures

TL;DR

This paper develops a formal theory for layered control architectures in autonomous systems, enabling compositional analysis and design of hybrid systems with discrete and continuous components.

Contribution

It introduces a novel contract-based framework for layered control systems, allowing modular design and analysis of complex hybrid architectures.

Findings

Formalizes layered control architectures as hybrid systems.

Defines contracts to specify interfaces between layers.

Enables compositional verification of system-wide specifications.

Abstract

Autonomous systems typically leverage layered control architectures with a combination of discrete and continuous models operating at different timescales. As a result, layered systems form a new class of hybrid systems composed of systems operating on a diverse set of continuous and discrete signals. This paper formalizes the notion of a layered (hierarchical) control architecture through a theory of relations between its layers. This theory enables us to formulate contracts within layered control systems -- these define interfaces between layers and isolate the design of each layer, guaranteeing that composition of contracts at each layer results in a contract capturing the desired system-wide specification. Thus, the proposed theory yields the ability to analyze layered control architectures via a compositional approach.