A Contract Theory for Layered Control Architectures

TL;DR

This paper formalizes the notion of a layered (hierarchical) control architecture through a theory of relations between its layers, and yields the ability to analyze layered control architectures via a compositional approach.

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.

Figures (5)

• Figure 1: Sampler, Quantizer, and Eventifier diagram. The diagram commutes up to containment as the inverse transducers are proper.
• Figure 2: Transducer commutative diagram up to (alternating) simulation. $\mathcal{H}$ and $\mathcal{J}$ denote signal spaces related through the transducer $\mathcal{F}:\mathcal{H}\to\mathcal{J}$, and $\mathcal{B}(\cdot)$ is the space of systems defined over the corresponding signal space.
• Figure 3: Systems, transducers, and relations diagram.
• Figure 4: Illustration of a layer abstracted for the layer above. For $\mathcal{F}_u:\mathcal{U}^i\to\mathcal{U}^{i+1}$, $\hat{u}^{i+1}\in\mathcal{U}^{i+1}$, $u^i\subseteq 2^{\mathcal{U}^i}$,$\mathcal{F}_y:\mathcal{Y}^i\to\mathcal{Y}^{i+1}$, $\hat{y}^{i}\in\mathcal{Y}^{i}$, $\hat{y}^{i+1}\in\mathcal{Y}^{i+1}$.
• Figure 5: Executing the proposed hierarchical controller. Here, the different colored rectangles represent different propositions from \ref{['eq:LTL-example']}, where the blue rectangle corresponds to $\mathrm{base}$, the green rectangle to $\mathrm{gather}$, the yellow rectangles to $\mathrm{recharge}$ and the red rectangles to $\mathrm{danger}$. Arrows encode the FSM's solution to the LTL spec, dots show the MPC plan, and the curve is the path followed by the robot.

Theorems & Definitions (46)

• Example 2.1
• Definition 2.2: Periodic Sampler
• Definition 2.3: Linear Periodic Interpolator
• Definition 2.4: $(\epsilon,\delta)-T$ Inverse Sampler
• Definition 2.5: Quantizer
• Definition 2.6: $P$ Inverse Quantizer
• Definition 2.7: Eventifier
• Definition 2.8: $\ell$ Inverse Eventifier
• Definition 2.9: Signal relations
• Definition 2.10: Proper inverses