Chapter 4. Symbolic Synthesis for Cyber-Physical Systems

Matthias Rungger, Antoine Girard, and Paulo Tabuada

Cyber-physical systems (CPS) consist of cyber and physical components interacting through sensors and actuators. Consequently, the behavior of a CPS is described by the combination of discrete dynamics accounting for the behavior of cyber components (e.g., software and digital hardware) and continuous dynamics accounting for the behavior of physical components (e.g., temporal evolution of temperatures, positions, and velocities). The terms discrete and continuous refer to the domains where the quantities of interest live. For example, the quantities used to model cyber components typically live in finite sets, while the quantities used to model physical components are typically real values and, therefore, live in infinite sets. This hybrid nature is one of the main reasons why the modeling, analysis, and design of CPS are so difficult.

In this chapter we take the view that it is easier to design correct CPS than to verify the correctness of CPS. The key insight is that at design time we can make judicious choices that lead to predictable and correct systems. However, when the time comes to perform verification, such choices have already been made—and if incorrectly made, they may lead to undecidable or computationally hard verification problems. The approach we follow relies on abstracting the physical components so that they can be described by the same models used to describe cyber components. Once this is done, we can leverage the existing work on reactive synthesis of cyber systems to synthesize controllers enforcing the desired specifications. Throughout this chapter we will present this approach along with its assumptions and limitations.

Early ideas on the construction of symbolic models of continuous systems that are adequate for controller design can be found in [Caines98, Förstner02, Koutsoukos00, Moor02]. For example, in [Koutsoukos00, Moor02], supervisory control techniques are employed on the abstract level to design the controller for the symbolic model. The correctness of the design procedure is ensured by exploiting certain properties of the symbolic model. A more modern approach to ensure the correctness of the synthesis method is based on so-called simulation or alternating simulation relations [Alur98, Milner89]. Instead of proving the correctness directly, one shows that the symbolic model and the original CPS are related by an alternating simulation relation, from which the correctness of the controller refinement follows [Tabuada09]. We follow this line of reasoning in this chapter.

We denote the closed, open, and half-open intervals in by [a, b], ]a, b [a, b[, and ]a, b[ respectively. Intervals in are respectively denoted by [a;b], ]a;b[, [a;b[, and ]a;b[.

Given a function f: A → B and A′ ⊆ A, we define f(A′):= {f(a) ∈ B|a ∈ A′} as the image of A′ under f. A set-valued function or mapping f from A to B is denoted by . Each set-valued map defines a binary relation on A × B; that is, (a, b) ∈ f if b ∈ f(a). The inverse mapping f⁻¹ and the domain domf of a set-valued map f are defined by f^–1(b) = {a ∈ A|b ∈ f(a)} and domf = {a ∈ A|f (a) ≠ Ø}, respectively. We use id to denote the identity function; that is, id: A → A with id(a) = a for all a ∈ A.

Given a subset A ⊆ X of a metric space (X, d) with metric d, we use to denote the inflated set {x ∈ X|∃_a∈A:d(a, x)≤ε}. The boundary of a set A is denoted by ∂A and the set difference of two sets A and B is denoted, as usual, by .

Given a sequence a : [0;T] → A in some set A, we use a_t to denote its t-th element and a_[0,t] to denote its restriction to the interval [0, t]. The set of all finite sequences is denoted by A*. The set of all infinite sequences is denoted by A^ω. If A is equipped with a metric d, and B is a subset of A^ω, then we use to denote the set .

Definition 1: A system S is a tuple S = (X, X₀, U, →, Y, H) consisting of the following:

• Set of states X

• Set of initial states X₀ ⊆ X

• Set of inputs U

• Transition relation →⊆X × U × X

• Set of outputs Y

• Output map H:X → Y

An internal behavior ξ of S is an infinite sequence ξ ∈ X^ω for which there exists an infinite sequence ν ∈ U^ω, such that ξ₀ ∈ X₀ and (ξ_t, ν_t, ξ_t+1) ∈→ (also denoted by ) holds for all . Every internal behavior ξ of S induces an external behavior ζ of S—that is, an infinite sequence in Y that satisfies ζ_t = H(ξ_t) for all . We use B(S) to denote the set of all external behaviors of S.

Definition 2: Alternatively, we say that a system S is metric if Y is a metric space, or the system S is finite if X and U are finite sets. Otherwise, we say that S is an infinite system.

Following are two examples that illustrate the usefulness of the introduced notion of a system. We start with a finite state system, as given in Section 1.3 of [Tabuada09].

This behavior is illustrated by the finite state automaton shown in Figure 4.1. The circles denote the states and the arrows denote the transitions. The upper part of each circle is labeled by the state and the lower part is labeled by the output. The transitions are labeled by the inputs.

A message can be transmitted either successfully or unsuccessfully over the communication channel. If the received message is correct, the receiver sends a confirmation message to acknowledge the error-free message; otherwise, a repeat request is sent to the sender. The dynamic behavior of the receiver is illustrated in Figure 4.2.

The overall system S is given by the composition of the two systems. We do not provide details on how to compose systems, but rather refer the interested reader to [Tabuada09]. It is clear that S is a finite system. Some possible external behaviors of the sender are given by the following:

idle_s → tx_s/rx_s → ack_s → get_s → ...

idle_s → tx_s/rx_s → repeat_s → tx_s/rx_s → ...

Now we show that our mathematical system model is also adequate for continuous control systems, such as switched systems.

When the switch is closed, electrical energy is stored in terms of a magnetic field in the inductor. When the switch is open, the inductor acts as a second source and its voltage adds up to the source voltage on the load side. DC-DC boost converters have been extensively studied in the literature, often from a hybrid control perspective (see, for example, [Beccuti06, Buisson05, Senesky03]), and also in the context of abstraction-based controller design [Girard10, Girard12, Reißig13].

The state of the system is given by x(t) = [i_l(t), υ_c(t)]^T, where i_l(t) and υ_c(t) denote the current through the inductor and the voltage across the capacitor at time t, respectively. The dynamic behavior is described by the switched linear system:

In this system , i ∈[1; 2], and b are given as follows:

The system matrices A_i are used to describe the evolution of the state, depending on the position of the switch g(t) ∈ [1;2].

In Section 4.2.4, we design a state-dependent controller to regulate the voltage across the load; it is implemented in a sample-and-hold manner with sampling time . Moreover, we restrict our attention to a subset of the state space around the desired setpoint. We cast the sampled dynamics of Equation (4.1) on K as the following system:

The transition relation is defined as follows:

Here ξ_x,g(τ) is the solution of the differential equation (4.1) at time τ for the switch position g∈[1;2]. The system S_τ is a metric system. The external behavior coincides with the internal behavior and corresponds to the sampled continuous-time behavior defined by Equation (4.1).

We do not provide further examples, but refer the interested reader to [Tabuada09] and some recent articles in which the notion of a system according to Definition 1 is employed to describe networked control systems [Borri12] and stochastic control systems [Zamani14].

Intuitively, the atomic propositions represent the sets that are relevant for the particular desired system behavior.

Formally, a specification of the desired system behavior is given in terms of an LTL¹ formula φ, which is composed of propositional connectives (and “∧”, negation “¬”) with the addition of the temporal operator’s next “X”, always “G”, and eventually “F” over the set of atomic propositions P. An LTL formula is evaluated over infinite sequences π in 2^p. A sequence π is said to satisfy Xφ, Gφ, or Fφ if φ holds true in the next time step, in every time step, or at some future time step(s), respectively. A precise definition of a sequence π satisfying a given LTL formula φ is given in Chapter 6, “Logical Correctness for Hybrid Systems,” and can be found in several references, including [Baier08, Vardi96].

1. For the sake of brevity of the presentation, we omit the until operator U and focus on a fragment of full LTL.

A sequence ζ in Y is said to satisfy a formula φ, denoted by if the sequence hoζ, with h(y) = {P ∈ P|y ∈ P}, satisfies φ. The set of all sequences in Y that satisfy an LTL formula is denoted as follows:

We say that a system S satisfies an LTL formula φ, denoted by , if every external behavior of S satisfies φ:

Next we illustrate some widely used specifications and interpret their meaning in terms of the external behavior of a given system.

φ=GP

In this formula, P⊆Y is the set of safe outputs. The bad system states are given by YP. Given that a system S satisfies GP, the always G operator implies that every external behavior ζ∈B(S) remains in the good states for all times; that is, ζ_t∈P for all .

Let us revisit the previously introduced example of the communication protocol. We can use the following safety formula:

φ=G¬(ack_s ∧ repeat_r)

This expresses the requirement that the sender should never “believe” that a message was transmitted successfully while the receiver responded with a repeat request; that is, the sender and the receiver should never be in the states with outputs ack_s and repeat_r simultaneously.

φ=FP

This expression indicates that the set P⊆Y should be reached after a finite number of steps; that is, every external behavior ζ∈B(S) satisfies ζ_t∈P for some . For example, if S represents a computer program and P⊆Y corresponds to the termination condition—that is, H(x)∈P means that the program terminated—then implies that S terminates eventually.

φ=FGQ

This implies that every behavior ξ of a system S satisfying φ eventually reaches Q and stays in Q afterward; that is, there exists such that for all t′≥t we have ξ_t′∈Q. In addition to this property, we can easily impose certain constraints P⊆Y during the transient system behavior, implying that ξ_t∈P for all , by the following expression:

φ = FGQ∧GP

φ = FGQ∧GP

The safety constraint serves two purposes. First, using the safety property, we ensure that certain physical limitations of the DC-DC converter are never exceeded during the transient behavior. For example, with GP we ensure that the current always stays within [0.65, 1.65]. The second purpose of the safety constraint is to restrict the problem domain to a bounded subset of the state space, which facilitates the computation of finite symbolic models.

Here, P and Q are subsets of Y. For those specifications, it is well known that a memoryless or state-feedback controller exists [Tabuada09]. We define a controller C for a system S as the set-valued map:

This controller is used to restrict the possible inputs of the system S. The closed-loop system S/C follows from the composition of S with C by the following expression:

The modified state space X_C = X ∩ domC, X_0,C = X₀ ∩ domC and the modified transition relation are given by the following expression:

The closed-loop system is illustrated in Figure 4.4. At sampling times tτ, , the controller provides the valid inputs ν_t∈C(ξ_t) based on the current state ξ_t of the system. The inputs ν_t are kept constant over the sampling interval [tτ, (t + 1)τ[.

In the implementation of the controller C on a digital device, we can pick any input ν_t∈C(ξ_t) according to some selection criterion.

With the precise notion of a closed-loop system, we formulate the synthesis problem as follows.

Problem 1: Given a system S and LTL specification φ of the form shown in Equation (4.5), we can find a controller C (if it exists) so that B(S/C)≠Ø and S/C satisfies the specification; that is, . (With specifications of the form in Equation (4.5), we might also be able to solve more general problems, such as attractiveness specifications.)

Remark 1: Suppose that the output map H of S is injective. We consider two sets Q, P⊆Y with Q⊆P. Let C₁ and C₂ be two controllers for S:

Here Q′ = H(dom C₁). Then we define the controller:

We claim that . If x ∈ dom C₁, every external behavior ζ of S with initial state x stays in Q (and P) forever and, therefore, ζ satisfies . If x ∈ dom C₂dom C₁, every external behavior with initial state x reaches Q′ in finite time. Let be the first time for which ζ_t ∈ Q′. Since H is injective, this implies that the corresponding internal behavior satisfies ξ_f ∈ dom C₁, after which controller C₁ is used to keep the behavior inside Q, which shows that ζ satisfies FGQ ∧ GP.

Definition 3: Let S and Ŝ be two metric systems with U = Û, Y = Ŷ, and metric d. Consider the parameter . The relation

is said to be an ε-approximate simulation relation (ε-aSR) from S to Ŝ if the following is true:

• For all x₀ ∈ X₀, there exists so that and for any :

•

• implies the existence of such that

We say that Ŝ approximately simulates S or that S is approximately simulated by Ŝ, denoted by the following if there exists an ε-aSR from S to Ŝ:

If R is an ε-aSR from S to Ŝ and R^–1 is an ε-aSR from Ŝ to S, then R is called an ε-approximate bisimulation relation (ε-aBSR) between S and Ŝ. We say that S is ε-approximately bisimilar to Ŝ, denoted by the following if there exists an ε-aBSR between S and Ŝ:

The next theorem shows that approximate (bi)similarity implies approximate behavioral (equivalence) inclusion. The theorem comes from Proposition 9.4 in [Tabuada09].

Theorem 1: Let S and Ŝ be two metric systems with U = Û, Y, = Ŷ, and metric d. Suppose that there exists an ε-aSR from S to Ŝ. Then, for every external behavior ζ of S, there exists an external behavior of Ŝ such that

Equivalently we have the following:

If S and Ŝ are ε-approximately bisimilar, we have the following:

In the following discussion, let us assume that we are given a system S and a finite system Ŝ, that ε-approximately simulates S. Theorem 1 allows us to (approximately) answer verification problems for S using the abstraction Ŝ. Suppose that we would like to know if S satisfies a safety property φ = GP. By utilizing well-known algorithms from automata theory [Vardi96], we can check whether Ŝ satisfies for . The formula represents a more restricted variant of φ and accounts for the approximate behavioral inclusion in Equation (4.7) in the sense that holds. If Ŝ satisfies we deduce from Equation (4.7) that S satisfies φ. We express this fact in symbols as follows:

Note, however, that does not allow us to make the reverse conclusion; that is, does not imply . To reason about the reverse direction, we need the stronger notion of bisimilarity. Given that , we deduce from Equation (4.8) that , with , implies and we obtain both directions as follows:

In contrast to the formula represents a relaxed variant of the formula φ and there exists a “gap” in the decision procedure based on approximately bisimilar models. However, as we will see in Section 4.2.4, under suitable stability assumptions this gap can be made arbitrarily small.

In this section we show how to refine the controller Ĉ for Ŝ to a controller C for S. Depending on the particular specification at hand, we will employ different refinement strategies. The controller refinement for general specifications based on bisimulation relations can be found in [Tabuada08]. The specialized case considered in this chapter is reported in [Girard12].

We start with the rather straightforward refinement strategy for safety specifications φ = GP. Let R be an ε-aBSR between S and Ŝ. We then refine a controller Ĉ_s for Ŝ to a controller C_s for S:

The control inputs available at a state x of the original system are given by the union of control inputs that are available to the symbolic model at the related states .

The refinement strategy for reachability specifications φ = GP ∧ FQ is formulated in terms of the minimal time function associated with a controller Ĉ_r for Ŝ. The function is defined as the least upper bound on the entry time of all external behaviors of Ŝ/Ĉ with initial state in the set Q while staying in P:

Since Ŝ/Ĉ_r is finite, the function can be computed iteratively by a shortest-path algorithm. We obtain the refinement strategy for reachability specifications as follows. Let R be an ε-aBSR between S and Ŝ and let Ĉ_r be a controller for Ŝ. Let T_Ĉr be given according to Equation (4.10). Then we define the controller Ĉ_r for S:

Here, we use the convention that argmin_x∈Af(x) = Ø for inf_x∈Af(x) = ∞. The control inputs available at a state x of the original system are given by the control inputs that are associated with a related state that attains the minimum in . Basically, we pick the inputs associated with a symbolic state from which the symbolic model Ŝ/Ĉ_r reaches the set Q the fastest.

In the following theorem, we summarize Theorem 1 and Theorem 3 of [Girard12], which ensure the correctness of the presented refinement procedures. Moreover, we provide a statement for the case when the specification for the symbolic model is unrealizable—that is, when there exists no controller such that the closed-loop system satisfies the specification. This statement follows immediately by the symmetry of the presented refinement strategies; that is, a controller for the original system can be refined to a controller for the symbolic model by exchanging the roles of the system and the symbolic model.

Theorem 2: Let S and Ŝ be two metric systems with U = Û, Y = Ŷ, and metric d. Let R be an ε-aBSR from S to Ŝ. Consider the sets P, Q ⊆ Y and their approximations:

The following implications hold:

Here the controllers C_i, i ∈ {s, r} for S are refined from the controllers Ĉ_i for Ŝ according to Equations (4.9) and (4.10), respectively.

Moreover, if (or ) is unrealizable with respect to Ŝ, then GP (or GP ∧ FQ) is unrealizable with respect to S.

Here control input g ∈ G = [1;k], system state , and system matrices and affine terms are given by and , respectively.

A trajectory of Σ associated with an initial state and a constant input g ∈ G is given by the following expression:

where e^A denotes the matrix exponential defined by the series . Let us define the system that captures the sampled behavior of Σ.

Given a sampling time , we define S_τ(Σ) as follows:

The transition relation is defined by the following:

In the following sections, we construct a symbolic model for S_τ(Σ).

We assume in the present discussion that there exist a symmetric, positive definite matrix and a constant that satisfy the following inequality:

Conditions on the matrices A_g, g ∈ G that imply the existence of such a matrix M and k are given in [Shorten98] and [Liberzon99]. Given M, we define the following function:

We argue that V is actually a δ-GUAS Lyapunov function for Σ [Girard13, Definition 2]. Let λ^– and λ⁺ be the smallest and largest eigenvalues of M, respectively. Then we can verify that V satisfies the following inequalities for all x, and g ∈ G:

Here D_iV denotes the partial derivative of V with respect to i-th argument. Observe that the inequalities in Equations (4.15) and (4.16) are sufficient for V being a δ-GUAS Lyapunov function and the following inequality holds:

Moreover, it is easy to show that W(x) := V(x, 0) is a norm on and, therefore, satisfies the triangle inequality. Then we use V(x, y) = V(x - y,0) and obtain the following inequality for all x,y,:

Based on the definition of the grid, balls of radius η centered at the grid points [K]_η cover the set K:

With the discretization parameter at hand, we define the system:

The transition relation is given by the following:

Note that S_τ(Σ) and S_τ,η(Σ) are metric systems with the same input and output space. The metric is simply given by d(x, y) = |x - y|. Moreover, given that G is finite and K is bounded, the system S_τ,η(Σ) is finite.

The following theorem is from Theorem 4.1 in [Girard10].

Theorem 3: Consider a control system Σ, discretization parameters τ,, and a desired precision . Suppose a symmetric, positive definite matrix M and a constant satisfy Equation (4.14). Let and λ⁺, λ^– be the largest and smallest eigenvalues of M, respectively. If the relation

holds, then the following is an ε-aBSR between S_τ(Σ) and S_τ,η(Σ) with respect to the metric d(x, y) = |x - y|:

Let us provide the proof of this theorem, as it nicely illustrates the relationship between Equation (4.21) and R being an ε-aBSR between S and Ŝ.

We show only that R is an ε-aSR from S to Ŝ. The reverse direction follows by the symmetry of the arguments. Recall Definition 3 of an ε-aSR. Let us check the first condition. From Equation (4.19), it follows that for every x ∈ K, there exists such that . We use Equation (4.15) to see that . From Equation (4.21), it follows that , which implies that .

To show the second condition, let . From Equation (4.15), we get the inequality ; it follows from the definition of R that .

We proceed with the third condition in Definition 3. Let and . Then, by definition of the transition relation, we have x′ = ξ_x,g(τ). We pick so that with the following:

By the definition of the transition relation of S_τ,η(Σ), such an always exists. Now we deduce by the following series of inequalities that :

Recall that the desired specification for the converter is given by the LTL formulaφ = FGQ ∧ GP, where Q represents a neighborhood of the reference state and P are our safety constraints. In the discussion that follows, we restrict the computation of the symbolic model to P and, therefore, set K = P. Moreover, we focus on the following specification instead of φ:

φ′ = FQ ∧ GP

Nevertheless, as stated in Remark 1, it is a straightforward process to also synthesize a controller for φ with the presented methods.

As a first step in the construction of S_τ,η(Σ), we introduce a state transformation to provide better numerical conditioning. We rescale the voltage, which results in the new state x = [i₁, 5ν_c]^T. There exist both a symmetric positive definite matrix M and a constant satisfying Equation (4.14), which are given by k = 0.014 and the following:

The eigenvalues of M are λ^– = 1 and λ⁺ = 1.02554. We fix the desired accuracy to ε = 0.1 and the sampling time to τ = 0.5. We choose the state-space discretization parameter as η = 97·10^–5 so that Equation (4.21) holds, and we compute S_τ,η(Σ), which results in a symbolic model with approximately 7·10⁵ states.

The atomic propositions in the new state space, which are illustrated in Figure 4.5, are given by Q′ = [1.1,1.6] × [5.4, 5.9] and P′ = [0.65, 1.65] × [4.95, 5.95]. We use and to synthesize a controller Ĉ so that . The controller C for S follows by Equation (4.11).

The domain of the controller and some sample trajectories are illustrated in Figure 4.5. The atomic propositions Q′ and P′ are illustrated by the small and large dashed rectangle, respectively. The black region shows the target set for the symbolic model enlarged by ε balls; that is, . The dark gray shaded regions show the domain of the controller domC. In particular, the light gray shaded region and the dark gray shaded region show C^–1(1) and C^–1(2), respectively. Some example trajectories of the closed-loop system S_τ(Σ)/C are shown by the dotted lines.

In the following subsections, we discuss some generalizations (related methods) of the presented scheme and provide follow-up references for the interested reader. We explain the curse of dimensionality and refer to existing methods that address this issue. We describe two possibilities to account for the continuous-time behavior of a system and comment on practical aspects of the implementation of the synthesized controllers on embedded devices. We conclude this section by listing software tools that can be used to compute symbolic models for the design of controllers for CPS.

Note that we do not address extensions with respect to more complex specifications. It is conceptually clear that once we have a method to compute symbolic models (together with the appropriate simulation relations) for a particular class of CPS, any controller synthesis method developed for a finite system that is tailored to a specific specification language—for example, LTL, CTL, or μ-Calculus—can be adapted to synthesize controllers for this class of CPS, while enforcing the respective specification.

Symbolic models of two-dimensional continuous-time single-integrator and double-integrator systems are analyzed in [Kress-Gazit09] and [Fainekos09a], respectively. General discrete-time linear control systems are treated in [Kloetzer08, Tabuada06, Wongpiromsarn12]. [Yordanov12] presents an algorithm to compute symbolic models for piecewise affine systems.

Methods to construct symbolic models for switched polynomial systems are presented in [Ozay13]. General nonlinear systems (with time delays), switched nonlinear systems, and networked control systems under incremental stability assumptions, similar to the one presented here, are considered in [Pola08] ([Pola10]), [Girard10], and [Borri12], respectively. [Reißig11], [Zamani12], and [Tazaki12] provide algorithms to compute symbolic models of nonlinear systems without stability assumptions.

Symbolic models that are adequate for synthesis of hybrid control systems with state-dependent autonomous transitions are not yet fully understood. Two approaches for the special cases of hybrid systems with discrete-time linear dynamics and order-minimal hybrid systems are described in [Mari10] and [Bouyer06], respectively.

Algorithms to compute symbolic models that lead to controllers that are robust against model uncertainties, actuation errors, or uncontrollable environment dynamics are rather rare. In contrast to the unperturbed case, the symbolic model for perturbed systems needs to be related to the concrete system by an alternating simulation relation instead of a simulation relation [Tabuada09]. Alternating simulation relations are used to account for the uncontrollable disturbances and ensure the correctness of the controller refinement under all possible perturbations. [Wongpiromsarn12] considers discrete-time linear systems with bounded disturbances. Symbolic models of perturbed nonlinear systems under stability assumptions are considered in [Pola09]; they are examined without stability assumptions in [Liu14].

For example, symbolic models for flat systems are developed in [Tabuada05], [Colombo11], and [Colombo13]. Flat systems have the nice property that the external behavior of the system—that is, the output trajectories—are reproducible (using an input transformation) by a chain of integrators. Therefore, any synthesis problem with respect to the nonlinear system is reducible to a (often lower-dimensional) linear system. By exploiting this property and reducing the chain of integrators further to a first-order system [Girard09], a safety synthesis problem involving an eight-dimensional nonlinear system has been solved [Colombo13]. Another particular system class—monotone systems—is analyzed in [Moor02a].

Rather than focusing on particular system properties, various methods try to reduce the computational burden, by adaptively improving the quality of the symbolic model while solving the synthesis problem on the abstract domain. For example in [Camara11] and [Mouelhi13], symbolic models on multiple time scales are used to locally refine the symbolic model where the controller synthesis fails. In [Rungger12], a heuristic is presented with the objective of reducing one of the most expensive operations—that is, the reachable set computations—in the construction of symbolic models. [Gol12] and [Rungger13] present techniques to adapt the computation of the symbolic model of a discrete-time linear system to a given specification, thereby reducing the domain on which the symbolic model needs to be computed. The aforementioned schemes vary with respect to the considered system dynamics, ranging from linear systems [Gol12, Rungger13], to incrementally stable switched nonlinear systems [Camara11, Mouelhi13], to general nonlinear systems [Rungger12]. Various methods have been used to compute symbolic models of CPS, including those with as many as five continuous variables.

Another interesting approach is described in [Le Corronc13]. These authors propose a quite different scheme to compute symbolic models of incrementally stable switched nonlinear systems. Instead of following the well-known methods in which the states of the symbolic model correspond to grid points or partition elements in the state space, they use bounded sequences of the switching signal as symbolic states. This approach has the potential to yield symbolic models that are constructed independently of the state-space dimension. For example, the authors were able to construct a symbolic model of a five-dimensional switched linear system with three modes.

Yet another advanced approach to compute symbolic models with the objective of reducing the computational burden induced by CoD is based on so-called sampling-based techniques [Bhatia11, Karaman11, Maly13]. Rather than computing the symbolic model on a grid or partition of the continuous state space, the symbolic model is constructed incrementally. New transitions are added to the abstract system by sampling the continuous input space and state space. Several different heuristics are used to guide the growth of the symbolic model. In [Maly13], a symbolic model of a hybrid system with a five-dimensional continuous state space is constructed to solve a synthesis problem with respect to a co-safety LTL specification.

Another issue that relates to the implementation of a controller that is obtained using the symbolic synthesis methods is the required state information. For example, the controller synthesis approach outlined in Section 4.2.3 assumes that complete state information is available at the controller. A more realistic assumption is that only quantized state information is available. Controller refinement schemes that address this issue and require only quantized state information are developed in [Mari10], [Girard13], and [Reißig14].

More complex continuous dynamics—in particular, discrete-time piecewise affine systems in connection with full LTL specifications—are supported by conPAS2 [Yordanov12].

Code System from Maria (CoSyMA) [Mouelhi13] is a tool that supports incrementally stable switched systems. CoSyMA uses an advanced multiscale abstraction technique to compute the symbolic models and handles time-bounded reachability and safety specifications.

A versatile tool that provides algorithms to compute symbolic models of various dynamical systems is Pessoa [Mazo10]. It offers synthesis procedures for safety and reachability specifications and is specifically tailored to linear systems. However, Pessoa also supports the construction of symbolic models of nonlinear systems.

The interdisciplinary field of automated controller design for CPS is a rather young research area. The pioneering work reported in [Koutsoukos00], [Moor02], [Förstner02], and [Caines98] has clarified, in principle, how we might leverage discrete algorithmic synthesis methods for CPS, yet numerous questions remain to be answered and challenges are as yet unresolved. The most pressing challenge is perhaps the need to decrease the computational complexity of the symbolic approach. The CoD needs to be addressed for some practically interesting classes of CPS before we can see a widespread application of this approach in practice. Furthermore, when it comes to the deployment of synthesized controllers on an embedded device, the memory size of the controller might represent an obstacle.

In addition to complexity issues, several theoretical questions need to be answered, such as those dealing with the completeness of the symbolic approach. As we have seen, if the control system satisfies certain incremental stability assumptions, it is possible to construct approximate bisimilar abstractions, which implies approximate completeness. However, completeness results for control systems with unstable dynamics or more complex dynamics—for example, hybrid systems—remain an open question.

[Alur00]. R. Alur, T. A. Henzinger, G. Lafferriere, and G. J. Pappas. “Discrete Abstractions of Hybrid Systems.” Proceedings of the IEEE, vol. 88, no. 7, pages 971–984, 2000.

[Angeli02]. D. Angeli. “A Lyapunov Approach to Incremental Stability Properties.” IEEE Transactions on Automatic Control, vol. 47, no. 3, pages 410–421, 2002.

[Baier08]. C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, Cambridge, MA, 2008.

[Beccuti06]. G. A. Beccuti, G. Papafotiou, and M. Morari. “Explicit Model Predictive Control of the Boost DC-DC Converter.” Analysis and Design of Hybrid Systems, vol. 2, pages 315–320, 2006.

[Bhatia11]. A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi. “Motion Planning with Complex Goals.” IEEE Robotics and Automation Magazine, vol. 18, no. 3, pages 55–64, 2011.

[Borri12]. A. Borri, G. Pola, and M. Di Benedetto. “A Symbolic Approach to the Design of Nonlinear Networked Control Systems.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 255–264, 2012.

[Bouyer06]. P. Bouyer, T. Brihaye, and F. Chevalier. “Control in O-Minimal Hybrid Systems.” Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pages 367–378, 2006.

[Buisson05]. J. Buisson, P. Richard, and H. Cormerais. “On the Stabilisation of Switching Electrical Power Converters.” In Hybrid Systems: Computation and Control, pages 184–197. Springer, 2005.

[Caines98]. P. E. Caines and Y. J. Wei. “Hierarchical Hybrid Control Systems: A Lattice Theoretic Formulation.” IEEE Transactions on Automatic Control, vol. 43, no. 4, pages 501–508, 1998.

[Camara11]. J. Camara, A. Girard, and G. Gössler. “Safety Controller Synthesis for Switched Systems Using Multi-Scale Symbolic Models.” Proceedings of the Joint 50th IEEE Conference on Decision and Control and European Control Conference, pages 520–525, 2011.

[Colombo11]. A. Colombo and D. Del Vecchio. “Supervisory Control of Differentially Flat Systems Based on Abstraction.” Proceedings of the Joint 50th IEEE Conference on Decision and Control and European Control Conference, pages 6134–6139, 2011.

[Colombo13]. A. Colombo and A. Girard. “An Approximate Abstraction Approach to Safety Control of Differentially Flat Systems.” European Control Conference, pages 4226–4231, 2013.

[Fainekos09a]. G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas. “Temporal Logic Motion Planning for Dynamic Robots.” Automatica, vol. 45, no. 2, pages 343–352, 2009.

[Fainekos09]. G. E. Fainekos and G. J. Pappas. “Robustness of Temporal Logic Specifications for Continuous-Time Signals.” Theoretical Computer Science, vol. 410, no. 42, pages 4262–4291, 2009.

[Förstner02]. D. Förstner, M. Jung, and J. Lunze. “A Discrete-Event Model of Asynchronous Quantized Systems.” Automatica, vol. 38, no. 8, pages 1277–1286, 2002.

[Girard11]. A. Girard. “Controller Synthesis for Safety and Reachability via Approximate Bisimulation.” Technical report, Université de Grenoble, 2011. http://arxiv.org/abs/1010.4672v1.

[Girard12]. A. Girard. “Controller Synthesis for Safety and Reachability via Approximate Bisimulation.” Automatica, vol. 48, no. 5, pages 947–953, 2012.

[Girard13]. A. Girard. “Low-Complexity Quantized Switching Controllers Using Approximate Bisimulation.” Nonlinear Analysis: Hybrid Systems, vol. 10, pages 34–44, 2013.

[Girard07]. A. Girard and G. J. Pappas. “Approximation Metrics for Discrete and Continuous Systems.” IEEE Transactions on Automatic Control, vol. 52, pages 782–798, 2007.

[Girard09]. A. Girard and G. J. Pappas. “Hierarchical Control System Design Using Approximate Simulation.” Automatica, vol. 45, no. 2, pages 566–571, 2009.

[Girard10]. A. Girard, G. Pola, and P. Tabuada. “Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems.” IEEE Transactions on Automatic Control, vol. 55, no. 1, pages 116–126, 2010.

[Gol12]. E. A. Gol, M. Lazar, and C. Belta. “Language-Guided Controller Synthesis For Discrete-Time Linear Systems.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 95–104, 2012.

[Henzinger00]. T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong-Toi. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.” In Hybrid Systems: Computation and Control, pages 130–144. Springer, 2000.

[Karaman11]. S. Karaman and E. Frazzoli. “Sampling-Based Algorithms for Optimal Motion Planning.” International Journal of Robotics Research, vol. 30, no. 7, pages 846–894, 2011.

[Kloetzer08]. M. Kloetzer and C. Belta. “A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications.” IEEE Transactions on Automatic Control, vol. 53, pages 287–297, 2008.

[Koutsoukos00]. X. D. Koutsoukos, P. J. Antsaklis, J. A. Stiver, and M. D. Lemmon. “Supervisory Control of Hybrid Systems.” Proceedings of the IEEE, vol. 88, no. 7, pages 1026–1049, 2000.

[Kress-Gazit09]. H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. “Temporal-Logic–Based Reactive Mission and Motion Planning.” IEEE Transactions on Robotics, vol. 25, no. 6, pages 1370–1381, 2009.

[Le Corronc13]. E. Le Corronc, A. Girard, and G. Gössler. “Mode Sequences as Symbolic States in Abstractions of Incrementally Stable Switched Systems.” Proceedings of the 52nd IEEE Conference on Decision and Control, pages 3225–3230, 2013.

[Liberzon99]. D. Liberzon and A. S. Morse. “Basic Problems in Stability and Design of Switched Systems.” IEEE Control Systems Magazine, vol. 19, no. 5, pages 59–70, 1999.

[Liu14]. J. Liu and N. Ozay. “Abstraction, Discretization, and Robustness in Temporal Logic Control of Dynamical Systems.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 293–302, 2014.

[Liu13]. J. Liu, N. Ozay, U. Topcu, and R. M. Murray. “Synthesis of Reactive Switching Protocols from Temporal Logic Specifications.” IEEE Transactions on Automatic Control, vol. 58, no. 7, pages 1771–1785, 2013.

[Maly13]. M. R. Maly, M. Lahijanian, L. E. Kavraki, H. Kress-Gazit, and M. Y. Vardi. “Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments.” Proceedings of the 16th International Conference on HSCC, pages 353–362, 2013.

[Mari10]. F. Mari, I. Melatti, I. Salvo, and E. Tronci. “Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems.” In Computer Aided Verification, pages 180–195. Springer, 2010.

[Mazo10]. M. Mazo, Jr., A. Davitian, and P. Tabuada. “Pessoa: A Tool for Embedded Controller Synthesis.” In Computer Aided Verification, pages 566–569. Springer, 2010.

[Milner89]. R. Milner. Communication and Concurrency. Prentice Hall, 1995.

[Moor02a]. T. Moor and J. Raisch. “Abstraction Based Supervisory Controller Synthesis for High Order Monotone Continuous Systems.” In Modelling, Analysis, and Design of Hybrid Systems, pages 247–265. Springer, 2002.

[Moor02]. T. Moor, J. Raisch, and S. O’Young. “Discrete Supervisory Control of Hybrid Systems Based on l-Complete Approximations.” Discrete Event Dynamic Systems, vol. 12, no. 1, pages 83–107, 2002.

[Mouelhi13]. S. Mouelhi, A. Girard, and G. Gössler. “Cosyma: A Tool for Controller Synthesis Using Multi-Scale Abstractions.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 83–88, 2013.

[Ozay13]. N. Ozay, J. Liu, P. Prabhakar, and R. M. Murray. “Computing Augmented Finite Transition Systems to Synthesize Switching Protocols for Polynomial Switched Systems.” American Control Conference, pages 6237–6244, 2013.

[Pnueli89]. A. Pnueli and R. Rosner. “On the Synthesis of a Reactive Module.” Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179–190, 1989.

[Pola08]. G. Pola, A. Girard, and P. Tabuada. “Approximately Bisimilar Symbolic Models for Nonlinear Control Systems.” Automatica, vol. 44, no. 10, pages 2508–2516, 2008.

[Pola10]. G. Pola, P. Pepe, M. Di Benedetto, and P. Tabuada. “Symbolic Models for Nonlinear Time-Delay Systems Using Approximate Bisimulations.” Systems and Control Letters, vol. 59, no. 6, pages 365–373, 2010.

[Pola09]. G. Pola and P. Tabuada. “Symbolic Models for Nonlinear Control Systems: Alternating Approximate Bisimulations.” SIAM Journal on Control and Optimization, vol. 48, no. 2, pages 719–733, 2009.

[Reißig11]. G. Reißig. “Computing Abstractions of Nonlinear Systems.” IEEE Transactions on Automatic Control, vol. 56, no. 11, pages 2583–2598, 2011.

[Reißig13]. G. Reißig and M. Rungger. “Abstraction-Based Solution of Optimal Stopping Problems Under Uncertainty.” Proceedings of the 52nd IEEE Conference on Decision and Control, pages 3190–3196, 2013.

[Reißig14]. G. Reißig and M. Rungger. “Feedback Refinement Relations for Symbolic Controller Synthesis.” Proceedings of the 53rd IEEE Conference on Decision and Control, 2014.

[Rungger13]. M. Rungger, M. Mazo, and P. Tabuada. “Specification-Guided Controller Synthesis for Linear Systems and Safe Linear-Time Temporal Logic.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 333–342, 2013.

[Rungger12]. M. Rungger and O. Stursberg. “On-the-Fly Model Abstraction for Controller Synthesis.” American Control Conference, pages 2645–2650, 2012.

[Senesky03]. M. Senesky, G. Eirea, and T. J. Koo. “Hybrid Modelling and Control of Power Electronics.” In Hybrid Systems: Computation and Control, pages 450–465. Springer, 2003.

[Shorten98]. R. N. Shorten and K. S. Narendra. “On the Stability and Existence of Common Lyapunov Functions for Stable Linear Switching Systems.” Proceedings of the 37th IEEE Conference on Decision and Control, vol. 4, pages 3723–3724, 1998.

[Tabuada08]. P. Tabuada. “An Approximate Simulation Approach to Symbolic Control.” IEEE Transactions on Automatic Control, vol. 53, no. 6, pages 1406–1418, 2008.

[Tabuada09]. P. Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.

[Tabuada05]. P. Tabuada and G. J. Pappas. “Hierarchical Trajectory Refinement for a Class of Nonlinear Systems.” Automatica, vol. 41, no. 4, pages 701–708, 2005.

[Tabuada06]. P. Tabuada and G. J. Pappas. “Linear Time Logic Control of Discrete-Time Linear Systems.” IEEE Transactions on Automatic Control, vol. 51, no. 12, pages 1862–1877, 2006.

[Tazaki12]. Y. Tazaki and J. Imura. “Discrete Abstractions of Nonlinear Systems Based on Error Propagation Analysis.” IEEE Transactions on Automatic Control, vol. 57, pages 550–564, 2012.

[Tiwari08]. A. Tiwari. “Abstractions for Hybrid Systems.” Formal Methods in System Design, vol. 32, no. 1, pages 57–83, 2008.

[Vardi95]. M. Y. Vardi. “An Automata-Theoretic Approach to Fair Realizability and Synthesis.” In Computer Aided Verification, pages 267–278. Springer, 1995.

[Vardi96]. M. Y. Vardi. “An Automata-Theoretic Approach to Linear Temporal Logic.” In Logics for Concurrency, pages 238–266. Springer, 1996.

[Wongpiromsarn12]. T. Wongpiromsarn, U. Topcu, and R. M. Murray. “Receding Horizon Temporal Logic Planning.” IEEE Transactions on Automatic Control, vol. 57, no. 11, pages 2817–2830, 2012.

[Wongpiromsarn11]. T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. “TuLip: A Software Toolbox for Receding Horizon Temporal Logic Planning.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 313–314, 2011.

[Yordanov12]. B. Yordanov, J. Tumová, I. Černá, J. Barnat, and C. Belta. “Temporal Logic Control of Discrete-Time Piecewise Affine Systems.” IEEE Transactions on Automatic Control, vol. 57, no. 6, pages 1491–1504, 2012.

[Zamani12]. M. Zamani, G. Pola, M. Mazo, and P. Tabuada. “Symbolic Models for Nonlinear Control Systems Without Stability Assumptions.” IEEE Transactions on Automatic Control, vol. 57, pages 1804–1809, 2012.

[Zamani14]. M. Zamani, I. Tkachev, and A. Abate. “Bisimilar Symbolic Models for Stochastic Control Systems Without State-Space Discretization.” Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pages 41–50, 2014.