Fig. 1. A typical layered control architecture, whereby MCL contracts enable independently designed controllers to meet system-level specifications.

using the properties of each layer. We introduce a new logic, Multiclock Logic (MCL), to be able to express properties from the local point of view of a processor running on its own clock-capturing the multi-rate nature of layered control systems. We use MCL to abstract layers into assume-guarantee contracts, which are formal specifications that capture what a component guarantees and requires from its environment to be able to deliver its guarantees [6]. We use the algebra of contracts to compositionally relate the local stability properties of control algorithms with the system-level properties of their interconnection. While multi-rate control architectures were first studied in [10], the problem of compositionally writing and analyzing formal specifications for control systems made from layers that operate on distinct time bases has not been studied.

This letter is organized as follows. Section II introduces our motivating example. Section III presents the syntax and semantics of MCL. Section IV shows how to express contract specifications for a multilayer controller using MCL, and to prove system-level stability properties from the properties of the control layers. An extended version of this letter [7] contains background on behavioral modeling and contracts.

To illustrate our compositional analysis of a layered architecture, we will consider the design of a control strategy for the pendulum shown in Figure 1. Our objective will be for the system to satisfy a top-level stability objective expressed as contract C. We will understand the controller for such as system as an architecture consisting of a high-level and a lowlevel control layers interconnected by a network. Each control layer will be assumed to be implemented on a processor operating on its own clock, as is common in practice. We will identify contracts C HL for the high-level layer, C LL for the low-level layer, C Est for state estimation, and C Tmg for the networking between the layers. As these contracts need to state formal properties over multiple clocks, they will be expressed in MCL in Section IV. The property of these contracts is that their composition is a refinement of the desired stability contract C. This means that we will be free to independently implement these aspects of the functionality, and the procedure will be guaranteed to yield a system that satisfies the systemlevel objective C. Afterwards, we will implement each of these control blocks independently.

We now consider the details of this case study. The configuration space of the system is given by θ ∈ Q S 1 , and the associated state by x = (θ, θ) ∈ TQ. We can write the dynamics in control-affine form as ẋ = f (x) + g(x)u, with control input u ∈ R, continuously differentiable drift vector f : TQ → R 2 , and actuation matrix g : TQ → R 2 . We will be concerned with the high level task of reaching some neighborhood of the goal state x g = 0, the unstable upright equilibrium. Low-level controllers alone struggle to simultaneously enforce state and input constraints while ensuring progress to the goal is being made [3]-this motivates the use of a hierarchy for achieving this control task. Our hierarchy will consist of two layers-a high-level controller and a low-level controller-running on different clocks.

1) Low-Level Controller Design: To actuate the system, we use a feedback controller which is able to track a desired trajectory x d . We begin by defining an output y : X → R as y(x) = θ , whereby we can construct error coordinates e(x, t) = y(x) L f y(x)y(x d (t)) ẏ(x d (t)) , with L f y(x) denoting the Lie derivative of y with respect to f . Then, a feedback control law can be created to stabilize the outputs. For example, the control law can be the feedback linearizing controller

which exponentially stabilizes the output coordinates for elementwise positive vector K ∈ R 2 . Given bounded additive disturbances to the dynamics, there exists a robust invariant set E ⊂ R n such that applying k fbl results in bounded tracking error, i.e.,

2) High-Level Controller Design: This controller will be concerned with producing the pieces of trajectories x d which make progress towards the goal x g for the low-level controller to track. In order to do so, we set up the following MPC program:

and g a linear approximations of the dynamics, x ∈ X an estimate of the system state, E ⊂ R n a robust invariant set of the low level controller, and x(t) and u(t) the continuous-time state and input of the low-level system.

Combining MPC with a low-level controller is a popular technique which is extensible to stabilizing complex nonlinear systems [5], [10]. When deploying such an architecture, however, the underlying approximations of convexification and discretization are often not explicitly reasoned about, leaving practitioners hoping rather than knowing that the closedloop system will work. Common assumptions include: i) the estimate of the state x is "close enough" to the true state x; ii) the MPC runs "fast enough" and produces solutions which are "close enough" to the system dynamics; and iii) the low-level controller runs "fast enough" and can track "well enough." The aim of this letter is to construct a pipeline whereby these assumptions are made explicit, with an eye towards automating the system verification process for layered control systems.

In this section, we introduce Multiclock Logic (MCL), a framework to reason about layered control operating on multiple clocks. First we define the behaviors over which the logic makes predicates, then introduce the logic. MCL will allow us to express properties from the local point of view of each control block in our design without burdening the syntax with synchronization over the multiple clocks present in the system. While some of these properties can be expressed intuitively, MCL is a formal language and so can be manipulated by a machine. This is necessary in order to automate formal system-level design.

1) System-Level Behaviors: The fundamental notion of system-modeling is the variable. We understand a variable as a tuple (v, X v , D v ), where v is the name for the variable, X v is the value space (a topological space where the variable takes values), and D v is a totally-ordered Abelian group called the clock, giving a notion of a progression of values. Whether a variable is discrete/continuous/constant depends on the clock that we assign to it: R/N/{•}, respectively. We model clocks as totally-ordered Abelian groups because we need order to compare values of a clock and define intervals, and the group structure to add and subtract these values.

Suppose we have a set C of clocks and that a set Vars of variables shares clock c ∈ C. The joint behaviors of these variables will be given by maps c → v∈Vars X v , as in the tagged signal model [9]. In order to isolate the value of a variable u ∈ Vars from those of the other variables in the same clock, we will use the projection maps that come with the definition of the product, i.e., π u : v∈Vars X v → X u .

Stating certain predicates may require us to use a clock to read the values of variables belonging to another clock. Suppose c, d ∈ C. To read the value of a d-variable in the clock c, we will assume the existence of a map τ d c : c → d. The τ maps, which we may call synchronization maps, determine the index of the target clock that is used when reading variables from a given clock. e.g., to read the value of a variable x clocked by d from the clock c at time t ∈ c, we would get the value of x at time τ d c (t). The synchronization maps capture the amount of delay incurred by reading data from a clock from which the data does not originate.

Suppose that we build a system that comprises a set of variables Vars and a set of clocks C. For each variable v, we let C(v) be the clock corresponding to v ∈ Vars. The inverse of this map, C -1 (c), yields the set of variables corresponding to clock c ∈ C.

Definition 1: A system-level behavior is an object Components, as usual, are defined as sets of behaviors. The following definition will be useful to give semantics to the eventual modality ♦ of the logic.

Definition 2:

The only difference between β and β t c is that in β t c the clock c is anticipated by t units.

2) MCL Syntax: Assume we have access to a set Vars of variables, a set C of clocks, and a set F of formulas of various arities. We let P be the set of symbols d d , where d and d denote clocks. The syntax of MCL is

We think of the formulas φ as the global syntax of MCL, and of the formulas as the local syntax that applies to a clock. The global syntax supports propositional logic. The syntax φ = ρc. indicates that a global formula φ is created by binding a local formula to the clock c. The local syntax supports propositional logic and the eventual modality. It also supports the enunciation of predicates involving multiple variables evaluated at the indicated times t i ∈ c. The syntax also supports the enunciation of predicates on clocks c ∈ C and on clock pairs c d ∈ P. The use of clocks and clock pairs c d ∈ P in formulas allows us to express timing constraints in our systems. Observe that the logic leaves abstract the formulas F used to define the predicates. The formulas are functions that evaluate to Boolean values.

3) MCL Semantics: The semantics of an MCL formula apply to a system behavior. Let β = (b d ) d∈C × (τ d d ) d,d ∈C be a system behavior. We have the following global semantics:

Formulas at the global level are either created by Boolean connectives, or they are local formulas that are assigned to a clock in the system. The symbol "|= c " stands for satisfaction in the local semantics of MCL, defined as follows:

•

, where

In addition to the formation of local formulas using Boolean connectives and the eventual modality ♦, MCL local formulas can be formed by making a predicate over a set of symbols λ i and a set of values t i of the clock c. In general, the meaning of the formula P(λ 1 (t 1 ), . . . , λ n (t n )) is the evaluation of the n-ary formula P for the values that each symbol λ i takes when the value of the clock c is τ c c (t i ). For example, the predicate ρc. x(0) > 2 for a variable x means that we will evaluate the value of x when c = τ c c (0). If x is clocked by c, we simply extract the value of x at time τ c c (0); if it is clocked by d = c, we would return its value at time τ d c (0). We recall that the local semantics can anticipate the value of c by t time units-see Definition 2.

The formula ρc.

This statement is true at ticks of clock c for which the index of clock d that c uses to read the data of d is larger than K + T. This type of predicate can be used as a precondition that ensures that the clock d has issued sufficient ticks. The semantics of a formula of the form ρc. r(0)

It states that the difference in r time units between a tick of c and the tick of d from which c reads the data of d must be less than T. This kind of statement is useful to bound the maximum allowed time for data to have existed in its local clock d before it is read by another clock c.

The notion of satisfaction is extended from system behaviors to components as follows: we say that a component M satisfies an MCL formula φ if β |= φ for all β ∈ M.

We extend the given syntax and semantics in the standard way to support all Boolean connectives and the modality , or "globally." Finally, when stating a formula of the form ρc. P(λ i (t i )) i , we will sometimes omit the t i arguments. In that case, the parameter should be understood as 0.

We now continue the analysis of the archetypal layered architecture described in Section II. Our goal is to specify the high-level and low-level control blocks independently and carry out system-level analysis using these specifications. The objective of our system-level analysis is to show that the system reaches and remains inside a neighborhood of the goal state x g . To do so, we assume we have a cost function V that maps the state x of the system to a well-ordered set. The value of V is zero in a neighborhood of x g . The function V will be further specified when we consider the implementations of component contracts in Section IV-C. As a well-order does not have infinite descending chains, the fact that the codomain of V is a well-order means that any process that decreases the cost V will eventually reach the minimum cost V(x) = 0 in a finite number of iterations.

The system has three clocks: m = N, which runs the high-level block; ℓ = N, which runs the low-level and estimation blocks; and r = R ≥0 , the physical time. The system state is denoted by the variable (x, X , r), i.e., its behaviors are functions from the physical clock to the state space X . The high-level block outputs a variable (x d , X r , m), which contains the trajectory in the state space that the system is to follow. Observe that the behaviors of this variable are functions from m to functions from r to X . Thus, at any tick of the clock m, the high-level controller will provide a function for the low-level controller. This means that x d will be doubly-indexed in our formulas. The first index corresponds to the clock evaluation, and the second to the time argument of the trajectory. For example, the ℓ formula ρℓ. x d (0)(T) < K evaluates to x d (τ m ℓ (0))(T) < K. Finally, an estimation block running on clock ℓ will output a state estimate (x, X , ℓ). Our system's objective is ρℓ. ♦ (V(x) = 0), i.e., our cost will stabilize at zero.

We consider the contracts for each layer in the system. 1) High-Level Controller: We consider the specification of the high-level controller running on a dedicated processor with clock m. The high layer has an input x, the state estimate coming from another control layer, and a single output x d , which is a trajectory that the low-level controller has to follow.

On a given tick of the clock m, the high-level block will assume that the state estimate is an accurate approximation of the state. The high-level controller uses this to compute a trajectory in the next tick of m. Finally, the high layer will guarantee that the trajectories it generates either decrease the cost V or keep it equal to zero. We can represent the high-level controller contract C HL = (A HL , G HL ) as follows:

fresh φ HL sensor : ρm. Close x, x; δ HL sensor φ HL bound_var : ρm. BoundedVariation(x; D x ) G HL : φ HL G_init ∧ φ HL rsp_dyn ∧ φ HL dynamics ∧ φ HL traj_bound_var ∧ φ HL progress φ HL G_init : ρm. Close x d (0)(0), x i ; δ HL G_init φ HL rsp_dyn : ρm. RespectDynamics(x d ) φ HL dynamics : ρm. Close x d (0) T m avg , x d (1)(0); δ HL dynamics φ HL traj_bound_var : ρm. BoundedVariation(x d ; D d ) φ HL progress : ρm.

HL sensor captures the requirement that the sensor produces values that are close to the real state x at the time when m ticks. The predicate Close(v, v ; δ) indicates that two symbols v, v are evaluated to quantities that are close up to a parameter δ for some notion of distance (taken to be ℓ 2 for the case study). HL bound v ar assumes that the state x has bounded variation. HL timing requires the clock period of m to lie between T m min and T m max ; (we also assume that the nominal m period T m avg lies between these bounds); the assumption also requires the difference in physical time between a tick of m and the tick of ℓ from which m reads ℓ's data to be less than T m fresh . This means that the data from ℓ that is read from m cannot be too old. HL A_init requires x to be close to a value x i at the beginning of the system execution.

With respect to guarantees, HL G_init means that the first trajectory output by the high-level block will start close to x i . HL rsp_dyn is a predicate stating that the high-level controller will always generate trajectories x d that should be within the competence of the low-level block to follow. In the context of this letter, we require that the produced trajectories are dynamically feasible, i.e., there exists a feedback controller which is able to track the generated trajectories. HL dynamics states that the beginning of every new trajectory provided by the high-level block has to be close to the value of the previous trajectory at time T m avg . HL traj b ound v ar is a promise that the trajectories provided by the high-level controller will have bounded variation.

Finally, in order to be able to promise that the system will make progress towards its objective, the high-level block will make use of the cost function V. The high-level controller makes a guarantee HL progress which says that either the cost at the beginning of a trajectory x d is larger than the cost at the beginning of the next trajectory x d , or that all points that are close to the trajectory have a cost of zero. The function Inflate(A, δ) takes a set A and returns the set of all points that are δ-close to any point of A. That is, each trajectory either improves the cost or stays fixed at cost equal to zero.

2) Low-Level Controller: The low-level controller takes as inputs trajectories x d that the system's state x has to follow and promises that it can make the system follow these trajectories with a given accuracy. We have the following contract C LL = (A LL , G LL ) for the low-level controller:

The assumptions of this contract are as follows. φ LL timing assumes that ℓ's period is bounded below and above, and that the data read from clock m is not too old. φ LL rsp_dyn requires trajectories received from m to respect certain physical limits, i.e., that they satisfy the state and input constraints used in the analysis of the low level controller. φ LL dynamics makes sure that when ℓ detects the generation of a new trajectory x d from m, then the starting point of that trajectory should be close to the value of the state. φ LL bound v ar requires the state x to have bounded variation.

Regarding guarantees, φ LL upd is a helper statement that defines the variable upd. This variable contains the last value of ℓ when a new trajectory was received from m. φ LL tracking guarantees that the low-level controller will make the system follow the given trajectory x d . Observe that φ LL tracking is enforced for all values of the trajectory x d , except its first point. For the first point of the trajectory, the low level controller makes the assumption φ LL dynamics on the state. T ℓ avg is the nominal period of ℓ and respects the bounds of φ HL timing .

3) Estimator: The estimator will guarantee that the state estimates are always accurate on the clock ticks of ℓ, yielding the contract C Est = (A Est , G Est ), where A Est : ρℓ. True and G Est : φ Est sensor , with φ Est sensor : ρℓ. Close(x, x; δ Est sensor ). 4) Timing Design: We understand the timing component of the system as "network design" in the sense that enforcing timing constraints is implemented by applying networking and clock synchronization technologies. This component will have the following contract C Tmg = (A Tmg , G Tmg ):

We have component-level contracts for all layers in our system. The following result connects these specifications with the desired top-level stability objective.

Theorem 1: Consider a two-layer control system formed by a high-level controller and a low-level controller. If each layer satisfies contracts C HL and C LL , respectively, the estimator satisfies C Est , and their interconnection satisfies C Tmg , then the top-level system will satisfy the top level contract (A, G), where

provided that the following conditions hold:

where

Proof: Contract composition yields the specification formed by interconnecting the components whose specifications we have available. Our system-level specification is C Sys = C HL C LL C Est C Tmg , which we compute by applying the ContractComposition routine of [8]. We now verify how this composition yields a system satisfying the assumptions of all components. a) High-Level Controller: We consider the assumptions: φ HL init is an assumption on the initial state that we need to conserve at the system-level. φ HL bound_var is also a system-level assumption. φ HL timing is satisfied by φ Tmg m-timing of our timing design. φ HL sensor needs to be analyzed. We observe that

foot_1 φ Est sensor φ Tmg m-timing φ HL bound_var ρm.Close x, x; δ Est sensor + T m fresh D x We need the relation (3) to hold in order to satisfy φ HL sensor . b) Low-Level Controller: φ LL timing is satisfied by φ Tmg ℓ-timing

of the timing design. φ LL bound_var is an assumption on the dynamics of the physical system and should therefore be a system-level assumption. φ LL rsp_dyn is satisfied by the guarantee φ HL rsp_dyn . The satisfaction of φ LL dynamics requires an inductive argument. For the proof that relation ( 4) is required for φ LL dynamics to hold in the initial case and that φ LL dynamics holds inductively when ( 5) is true, please see Section VI-B2 of the extended version of this letter [7].

c) Progress: Our analysis indicates that the composition of all contracts so far defined yields a situation in which all contracts have their assumptions met-provided the system parameters meet conditions (3), (4), and ( 5). Now we verify whether the system makes progress towards its goal. We observe that the fact that V takes values in a well order means that we can carry out the following deductions:

provided that (6) holds.

Theorem 1 shows that if we implement control layers adhering to the specifications introduced in Section IV-A and satisfying constraints (3)-( 6), the system will satisfy the desired stability property (2). These constraints impose timing requirements in the system. For instance, (5) imposes a limit on the maximum compute time of the high-level controller. This means that constraints (3)-( 6) can be used to increase the robustness of the design by ensuring that they are satisfied with margin. Now we verify that each implementation of our control layers satisfies its own contract.

1) Low-Level Controller: In order to use the methods presented in [4] which combine a low level controller with (1), we begin by showing that applying zero order held inputs, i.e., with ρℓ. (ū = k fbl (x, ℓupd)), results in bounded exogenous disturbance to the error dynamics. For the following discussion, let x (t) denote the solution to the system dynamics with continuous time control applied, and x(t) the solution with zero order held inputs. Plugging in the solution to the differential equation with x (0) = x(0) and adding and subtracting g(x (τ ))ū yields

where L f and L g represent the local Lipschitz constants of the drift vector and actuation matrix, respectively. From the perspective of the low level controller, we assume via φ LL rsp_dyn that u(t) ≤ U and that x(t) ∈ X , a compact set. These will be necessary for the analysis, and will be explicitly enforced in the proposed MPC formulation. From these constraints, we know that there exists a G > 0 such that g(x (τ )) < G and that all local Lipschitz constants are global over X . Combining these facts and using the Bellman-Gronwall Lemma [11] leads to x(t)x (t) ≤ UGt 2 e (L f +L g U)t tρ(t), where ρ ∈ K ∞ , a class K infinity function. Next, let e (t)

x (t)x d (t) denote the error dynamics with continuous time control applied, whereby the feedback linearizing controller k fbl yields ė (t) = A cl e for A cl a stable matrix. Taking e(t) = x(t)x d (t) to be the error with zero order held inputs, we have ė = w(t) + A cl e, where w(t) = d dt (xx ) + A cl (xx). Plugging in the terms developed in (7)

. As this bound is a composition of class-K functions in time, for all δ w > 0 there exists an > 0 such that T ℓ max < results in w(t) ≤ δ w . Fixing an allowable δ w and thereby upper bounding T ℓ max , by integrating the error dynamics and using the comparison lemma we have e(t) ≤ x(0)x d (0) Me -λt + T ℓ max δ w , for some M, λ > 0 as determined by the convergence rate of the low level controller. Therefore, in order to produce the guarantee of φ LL tracking , we must enforce that δ LL dynamics Me -λT ℓ min + T ℓ max δ w ≤ δ LL tracking . 2) MPC: Lemma 2 in [4] demonstrates that the trajectories produced by (1) are dynamically feasible, i.e., able to be exactly tracked via the feedback linearizing controller k fbl , implying satisfaction of φ r sp_dyn HL . As the MPC program produces solutions to a linear system with bounded state and control inputs, we have that the resulting desired trajectory x d will have bounded variation, satisfying φ HL traj_bound_var . Next, we ensure that the above MPC program is recursively feasible, which requires showing that the enforced set E is a robust invariant for the system. Choosing E such that B(0, δ LL tracking ) ⊂ E results in a set that can be rendered invariant by the low level controller, even during sampling. Therefore, we choose E to meet this condition as well as the design requirements imposed by the system analysis in Section IV-B. We then appeal to the results in [4] to prove recursive feasibility of the MPC algorithm used therein.

Finally, let V : X → R denote the sum of the running and terminal cost of MPC, often used as a Lyapunov function in stability proofs. As we have effectively transformed our nonlinear MPC program to a linear one, we can use standard MPC results [3] to state that ρm. (V(x d (1)(0)) < V(x d (0)(0))). Since the guarantees of the MPC contract involve V, which takes values in a well-order, we can define V by quantizing the function V. Then we can choose a vicinity around x g and define V(p) = 0 for p ∈ E. In that case, V takes values in a well-order, and the MPC block satisfies φ HL progress .

3) Simulation Results: We investigate the use of MCL contracts as a design tool towards achieving stability and state constraint satisfaction for an architecture consisting of a highlevel and a low-level control block designed in isolation. In both cases, the same control architecture and time delay of T ℓ fresh = T m max = T m min was used, i.e., the time delay is equal to one m clock cycle, and the m clock does not have jitter. In the first case shown in Figure 2(a), the MPC and FBL controllers were independently implemented, but their interconnection was not verified against formal specifications. Therefore, our analysis did not yield any guarantees of system behavior, and indeed we find that our system violates the desired state constraints x(t) ∈ X . In Figure 2(b), the margin E was modified such that (5) holds with equality. As a result of adhering to the MCL contracts, the composite control hierarchy maintains the desired system-level specification in (2) despite having independently designed components.

We considered an effective way of specifying control layers running on multiple clocks using MCL. Once the specifications were expressed, we used MCL contracts to prove system-level stability properties using the local properties of each layer. Our framework is extensible to systems with additional layers. We showed in the case study how to verify that each control block satisfies its own specification. Our simulation results showed that a violation of the system-level constraints led to failure. Future work involves applications to more complex systems, such as bipedal robots.