Automatic Synthesis of Stabilizing Controllers for
Discrete Time Linear Hybrid Systems
Leonardo Picchiami1
1
    Computer Science Dept., Sapienza University of Rome, via Salaria 113, 00198, Italy


                                         Abstract
                                         Many Cyber-Physical Systems are either mission or safety critical, thus the controllers for such systems
                                         must be provably correct. To this aim, in the last decades many methodologies have been developed
                                         which are able to automatically generate correct-by-construction controllers for Cyber-Physical Sys-
                                         tems.
                                             In this paper, we focus on one of such methodologies, implemented in the QKS tool, which is able
                                         to explicitly take into account the specification of the discretization of the state space due to analog-to-
                                         digital conversion. Controllers output by QKS are able to drive any controllable state inside the system
                                         goal. However, such controllers may allow a goal state to go outside the goal region, in order to be able
                                         to bring it back into the goal region later. QKS does not provide any means to detect such behavior.
                                             Here we propose to modify QKS in order to provide an additional feature, which only outputs stabi-
                                         lizing controllers, i.e., controllers which never allow goal states to go outside the goal region. If this is
                                         not possible for the input system, an empty controller is returned.
                                             We prove the feasibility of our approach on well-known control theory case studies, namely the
                                         multi input buck DC-DC converter and the inverted pendulum. Our experimental results show that we
                                         are able to output stabilizing controllers using limited additional resources with respect to the original
                                         QKS.

                                         Keywords
                                         Automatic Controller Synthesis, Stabilizing Controllers, CPS




1. Introduction
The development of correct-by-construction software controllers for Cyber-Physical Systems
(CPSs) is a strong requirement in many safety/mission-critical contexts such as, for example,
avionics [1, 2, 3, 4], smart grids [5, 6, 7, 8, 9], automotive [10, 11, 12, 13] or biological systems [14,
15, 16, 17, 18, 19, 20, 21, 22, 23]. In fact, many CPSs are Software-Based Control Systems (SBCSs),
which are typically subdivided into two subsystems: plant and controller. The plant is a physical
system (e.g., electric devices), whereas the controller is a software component running on
a microcontroller. The controller, in a closed-loop system, interacts with the plant to satisfy
formal specifications, i.e., functional requirements (liveness and safety) needed for correctness
of the system. In our setting, we want the controller to drive the system towards a goal region
(liveness), so that only safe states are traversed (safety). To this aim, the controller implements a

IPS-RCRA 2021: 9th Italian Workshop on Planning and Scheduling and 28th International Workshop on Experimental
Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
   picchiami@di.uniroma1.it (L. Picchiami)
 0000-0001-5477-6419 (L. Picchiami)
                                       © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
control law ctrlLaw, which, by looking at the current state, decides which action must be taken
to bring the system closer to the goal, while retaining safety. Such control law is guaranteed to
correctly work when the current state is within its control region CtrlReg.
   The usual control-loop workflow is as follows: the plant sensors measure an input 𝑥. SBCS
compute the Analog-to-Digital (AD) conversion getting a quantized value 𝑥         ˆ . The controller
checks if 𝑥ˆ belongs to the control region. If it is not in ctrlRegion, then the procedure of Fault
Detection, Isolation and Recovery is triggered. Otherwise, the system carries out the Digital-to-
Analog (DA) conversion and sends the command to the plant actuators.
   Designing a controller is an hard task [24]. In recent years, many articles have been published
aiming at automatically synthesizing controllers, often basing on ideas borrowed from logics [25,
26, 27, 28, 29, 30] and model checking techniques [31, 32, 33, 34, 35, 36, 37, 38, 39, 40]. This
has led to the introduction of many tools to automatically generate controllers, such as, e.g.,
PESSOA [41] and Synthia [42].
   In this paper, we focus on the Quantized feedback Kontrol Synthesizer (QKS) tool [43]. QKS
is a tool to automatically synthesize control software for an input system (plant) modeled as a
Discrete-Time Linear Hybrid System (DTLHS), i.e., a system described by continuous as well as
discrete variables. QKS also takes as input the liveness and safety specification, i.e., the goal
region to be reached by the system, as well as how many bits 𝑏 are available for the AD and
DA conversions. As an output, QKS returns the C code implementation of the control software,
which is guaranteed to drive any system state in the control region to the goal in a finite number
of steps, also taking into account the AD and DA conversion.
   The controller output by QKS is such that, once the system has reached the goal, it may also
exit from the goal itself. If this happens, the controller is again able to bring the system back
to the goal again. This may be undesired in some applications, where instead, it is required
that the system stabilizes in the goal, so preventing the system from leaving it. A system is
able to continuously meet properties that ensure the correctness and prevent errors as long
as it remains in the goal. So, in safety/mission-critical contexts (e.g., medical devices, drugs
or banking systems), we need controllers that implement the 𝑙-stability. Otherwise, we might
obtain systems that can be dangerous, for example, for a human or a company.
   Note that, in this paper, we present a new notion of stabilizing controllers. In the literature,
such a notion has often been used in a different unrelated setting, e.g., bounding fluctuations of
controller trajectories [44, 45]. Here, instead, we focus on controllers which “traps” a system
on the goal, if possible. To overcome the undesired behavior outlined above, in this paper, we
present an extension to QKS, which only outputs controllers which stabilize the system up
𝑙 ≥ 0 steps, being 𝑙 a further input for QKS.
   Other extensions of QKS have been presented in the literature with different objectives
than the ones we have here. Examples are in [46] (performing an on-the-fly controller gener-
ation), [47] (introducing a parallel algorithm for the controller synthesis) and [48] (aiming at
reducing the size of control software implementation). To the best of our knowledge, this is the
first time that an algorithm for stabilizing controllers for QKS is presented.
   The paper outline is as follows. We recall the mathematical notations which formalizes the
synthesis of software controllers (Section 2). Then, we introduce and formalize the concept
of stabilizing controllers (Section 3). Under this framework, we present a new algorithm to
generate stabilizing controllers (Section 4). Finally, we report an experimental comparison
between the existing algorithm of controller synthesis provided by QKS and the synthesis
algorithm of stabilizing controllers (Section 5). To this end, our case studies are the well-known
Multi-input Buck DC-DC converter and the Inverted Pendulum.


2. Formal Framework
To make this paper self-contained, we briefly summarize all concepts needed for the formaliza-
tion of stabilizing controllers. For a complete discussion, see [43].

2.1. Linear Predicate
Let [𝑛] = {1, . . . , 𝑛} be the set of positive integers less than 𝑛 and let 𝑋 = [𝑥1 , . . . , 𝑥𝑛 ] be a
sequence of distinct variables. Every variable 𝑥 ∈ 𝑋 is defined on either a finite (e.g., boolean
variables) or infinite (e.g., discrete or continuous variables) domain, denoted by 𝒟𝑥 . Boolean
variables are denoted as 𝑥𝑏 , continuous variables as 𝑥𝑟 , and discrete variables as 𝑥𝑑 . Along
the same lines, 𝑋 𝑏 (resp., 𝑋 𝑑 , 𝑋 𝑟 ) represents the sequence of the boolean (resp, discrete and
real) variables among the ones in 𝑋. The domain of a sequence of variables 𝑋 is denoted by
𝒟𝑋 = 𝑥∈𝑋 𝒟𝑥 .
        ∏︀
   A linear expression 𝐿(𝑋) is a linear combination of variables in 𝑋, i.e., 𝑥∈𝑋 𝑎𝑥 𝑥 where 𝑎𝑥
                                                                              ∑︀
are rational constants. A linear constraint is an expression of the form 𝐿(𝑋) ◁▷ 𝑏 where 𝑏 is a
rational constant and ◁▷ ∈ {≤, ≥, =} . A predicate is any logical combination of OR and AND
operations among linear constraints. A conjunctive predicate is predicate with AND operations
only.
   A valuation over 𝑋 is a function 𝑣 : 𝑋 → 𝒟𝑋 , assigning to each variable 𝑥 a value in the cor-
responding domain 𝒟𝑥 . Given a valuation 𝑣, we write 𝑋 * for the sequence [𝑣(𝑥1 ), . . . , 𝑣(𝑥𝑛 )] ∈
𝒟𝑋 , and we call it valuation as well. A satisfying assignment to predicate 𝑃 (𝑋) is a valuation
of 𝑋 * such that 𝑃 (𝑋) holds. If 𝑃 (𝑋 * ) holds for some 𝑋 * , then 𝑃 is feasible.
   Given a constraint 𝐶(𝑋) and a fresh variable 𝑦, the guarded constraint 𝑦 → 𝐶(𝑋) (if 𝑦
then 𝐶(𝑋)) denotes the predicate (𝑦 = 0) ∨ 𝐶(𝑋). By negating the guard variable, denoted
by (𝑦¯ → 𝐶(𝑋)), we get the predicate (𝑦 = 1) ∨ 𝐶(𝑋) (if not 𝑦 the 𝐶(𝑋)). A guarded
predicate is a conjunction of either constraints or guarded constraints. If all variables in 𝑋
are bounded (which implies that a linear expression 𝐿(𝑋) has a finite supremum), then any
guarded constraint may be translated in a linear constraint as follows: 𝑦 → 𝐿(𝑋) ≤ 𝑏 is
equivalent to (𝑠𝑢𝑝(𝐿(𝑋)) − 𝑏)𝑦 + 𝐿(𝑋) ≤ 𝑠𝑢𝑝(𝐿(𝑋)), while 𝑦¯ → 𝐿(𝑋) ≤ 𝑏 is equivalent to
(𝑏 − 𝑠𝑢𝑝(𝐿(𝑋)))𝑧 + 𝐿(𝑋) ≤ 𝑏. By recalling that 𝐿(𝑋) ≥ 𝑏 is equivalent to −𝐿(𝑋) ≤ −𝑏 and
𝐿(𝑋) = 𝑏 is equivalent to 𝐿(𝑋) ≤ 𝑏 ∧ 𝐿(𝑋) ≥ 𝑏, all guarded constraint may be translated to
linear predicates.

2.2. Labeled Transition Systems
A Labeled Transition System (LTS) is a tuple 𝒮 = (𝑆, 𝐴, 𝑇 ) where 𝑆 is a (possibly infinite) set of
states, 𝐴 is a (possibly infinite) set of actions and, 𝑇 : 𝑆 × 𝐴 × 𝑆 → B is the transition relation
of 𝒮.
   Let s ∈ 𝑆 and a ∈ 𝐴, 𝐴𝑑𝑚(𝒮, 𝑠) = {𝑎 ∈ 𝐴 | ∃𝑠′ : 𝑇 (s, a, s ′ )} is the set of admissible actions
starting from a state 𝑠, while 𝐼𝑚𝑔(𝑆, 𝑠, 𝑎) = {s ′ ∈ 𝑆 : 𝑇 (s, a, s ′ )} is the set of next states of s
through the action a (non-deterministic action). A transition is a triple (s, a, s ′ ) ∈ 𝑆 × 𝐴 × 𝑆
such that 𝑇 (s, a, s ′ ) holds. If s = s ′ , then the transition (s, a, s) is a self-loop.
   A path for an LTS 𝒮 is a sequence of states-actions 𝜋 = 𝑠0 𝑎0 𝑠1 𝑎1 . . . . . . where ∀𝑡 ≥
0 𝑇 (𝑠𝑡 , 𝑎𝑡 , 𝑠𝑡+1 ) holds. In addition, |𝜋| is the length of a given path that represents the number
of actions within 𝜋. 𝜋 (𝑆) (𝑡) denotes the (𝑡 + 1)-th state within 𝜋 and, 𝜋 (𝐴) (𝑡) denotes the
(𝑡 + 1)-th action over 𝜋.

2.3. Discrete Time Hybrid System
A Discrete Time Hybrid System (DTHS) ℋ = (𝑋, 𝑈 , 𝑌 , 𝑁 ) is a tuple defined as follows:
    • 𝑋 = 𝑋 𝑟 ∪ 𝑋 𝑑 is a finite sequence of real as well as discrete variables (possibly including
      boolean variables). It models the current state. Along the same lines, 𝑋 ′ denotes the next
      state.
    • 𝑈 = 𝑈 𝑟 ∪ 𝑈 𝑑 is a finite sequence of input variables.
    • 𝑌 = 𝑌 𝑟 ∪ 𝑌 𝑑 is a finite sequence of auxiliary variables typically used to model local
      variables.
    • 𝑁 (𝑋, 𝑈, 𝑌, 𝑋 ′ ) is the predicate that defines the system transition relation.
  An LTS can model the dynamics of a DTLHS as follows. Given a DTLHS ℋ = (𝑋, 𝑈, 𝑌, 𝑁 ),
the LTS of ℋ is defined as 𝐿𝑇 𝑆(ℋ) = (𝒟𝑋 , 𝒟𝑈 , 𝑁   ˜ ), where 𝑁    ˜ : 𝒟𝑥 × 𝒟𝑈 × 𝒟𝑥 → B is a
function such that 𝑁 (𝑥, 𝑢, 𝑥) ≡ ∃𝑦 ∈ 𝒟𝑦 𝑁 (𝑥, 𝑢, 𝑦, 𝑥 ), i.e., it represents the transition relation
                    ˜                                 ′

for the dynamics of the system. In such a way, a state for ℋ is also a state for 𝐿𝑇 𝑆(ℋ), and a
path for ℋ is also a path for 𝐿𝑇 𝑆(ℋ).

2.4. LTS control problem
A controller 𝐾 is a solution for a control problem of a given DTLHS ℋ. It restricts the set of
enabled behaviors of ℋ by selecting only those actions that bring the system to a goal region
infinitely often. In the following, we recall the main formalization for controllers and control
problems.

2.4.1. Definition of controller
Given a set of states 𝑆 and a set of actions 𝐴, a controller is a function 𝐾 : 𝑆 × 𝐴 → B such
that, ∀𝑠 ∈ 𝑆 and ∀𝑎 ∈ 𝐴, if 𝐾(𝑠, 𝑎) holds, then ∃𝑠′ ∈ 𝑆 such that 𝑇 (𝑠, 𝑎, 𝑠′ ) holds. If 𝐾(𝑠, 𝑎)
holds, we say that action 𝑎 is enabled in state 𝑠 by 𝐾. The set of states for which the at least
one action is enabled by a given controller 𝐾 is defined as 𝑑𝑜𝑚(𝐾) = {𝑠 ∈ 𝑆 | ∃𝑎 𝐾(𝑠, 𝑎)}.
   Given a controller 𝐾 on 𝑆 and 𝐴, the closed-loop system for an LTS 𝒮 = (𝑆, 𝐴, 𝑇 ) is the LTS
𝒮 (𝐾) = (𝑆, 𝐴, 𝑇 (𝐾) ) where 𝑇 (𝐾) (𝑠, 𝑎, 𝑠′ ) = 𝑇 (𝑠, 𝑎, 𝑠′ ) ∧ 𝐾(𝑠, 𝑎). In addition, a controller 𝐾
is also a control law if, ∀𝑠 ∈ 𝑆, 𝐾(𝑠, 𝑎) holds at most for one action.
   Given an LTS 𝒮, a path 𝜋 is a fullpath if either it is infinite or its last state (𝜋 (𝑆) (|𝜋|)) does
not have any successor state, (i.e., 𝐴𝑑𝑚(𝒮, 𝜋 (𝑆) (|𝜋|)) = ∅). The set of fullpaths of 𝒮 starting
from a state 𝑠 (i.e., 𝜋 (𝑆) (0) = 𝑠) with an action 𝑎 (i.e., 𝜋 (𝐴) (0) = 𝑎) is denoted by 𝑃 𝑎𝑡ℎ(𝒮, 𝑠, 𝑎).
   Given a fullpath 𝜋 and a region 𝐺 ⊆ 𝑆, 𝑗(𝒮, 𝜋, 𝐺) denotes the shortest distance to reach 𝐺
through 𝜋, i.e., 𝑗(𝒮, 𝜋, 𝐺) = min{𝑛 | 𝑛 > 0 ∧ 𝜋 (𝑆) (𝑛) ∈ 𝐺} if 𝜋(𝑖) ∈ 𝐺 for some 𝑖, otherwise
𝑗(𝒮, 𝜋, 𝐺) = +∞. Furthermore, let 𝐽(𝒮, 𝐺, 𝑠, 𝑎) = sup{𝑗(𝒮, 𝜋, 𝐺) | 𝜋 ∈ 𝑃 𝑎𝑡ℎ(𝒮, 𝑠, 𝑎)}
be the shortest distance to 𝐺 starting with state 𝑠 and action 𝑎. This allows us to define
𝐽 * (𝒮, 𝐺, 𝑠) = sup{𝐽(𝒮, 𝐺, 𝑠, 𝑎) | 𝑎 ∈ 𝐴𝑑𝑚(𝒮, 𝑠) for some 𝑎 ∈ 𝐴} as the worst case distance
from 𝐺.

2.4.2. Definition of control problem
An LTS control problem is a triple 𝒫 = (𝒮, 𝐼, 𝐺), where 𝒮 = (𝑆, 𝐴, 𝑇 ) is an LTS and 𝐼, 𝐺 ⊆ 𝑆.
A (strong) solution for 𝒫 is a controller 𝐾 for 𝒮 such that 𝐼 ⊆ 𝑑𝑜𝑚(𝐾) and ∀𝑠 ∈ 𝑑𝑜𝑚(𝐾),
𝐽 * (𝒮 (𝐾) , 𝐺, 𝑠) is finite. An optimal solution for a control problem 𝒫 is a controller 𝐾 * such
                     *
that ∀𝐾 𝐽 * (𝒮 (𝐾 ) , 𝐺, 𝑠) ≤ 𝐽 * (𝒮 (𝐾) , 𝐺, 𝑠). Along the same lines, the most general optimal
(m.g.o.) solution is the solution 𝐾   ¯ such that, for all optimal solutions 𝐾 * to 𝒫, ∀𝑠 ∈ 𝑆 and
∀𝑎 ∈ 𝐴, 𝐾(𝑎, 𝑠) → 𝐾      ¯ (𝑎, 𝑠) holds, i.e., if 𝐾(𝑠, 𝑎) holds, then 𝐾
                                                                      ¯ (𝑠, 𝑎) holds. The m.g.o. solution
is unique.

2.5. Control Problem for DTLHS
Since an LTS models the dynamics of a DTLHS, a control problem for a DTLHS is formally reduced
to a control problem for an LTS. Thus, a control problem for a DTLHS ℋ = (𝑋, 𝑈, 𝑌, 𝑁 ) is
denoted as (𝐿𝑇 𝑆(ℋ), 𝐼, 𝐺) for some 𝐼, 𝐺 ⊆ 𝒟𝑋 .
   In order to manage AD and DA conversions, we define a quantization function for real interval
[𝑎, 𝑏] as a non-decreasing function 𝛾 : [𝑎, 𝑏] → Z, that maps real values inside a continuous real
interval in integer values.
   Let a DTLHS ℋ = (𝑋, 𝑈, 𝑌, 𝑁 ) and let 𝑊 = 𝑋 ∪ 𝑈 , a quantization 𝒬 is a pair (𝐴, Γ) where:

    • 𝐴 is a predicate over 𝑊 that bounds real variables in 𝑊 , i.e., 𝐴 = ∧𝑤∈𝑊 𝐴𝑤 = ∧𝑤∈𝑊 𝑎𝑤 ≤
      ∏︀ ≤ 𝑏𝑤 . 𝐴𝑤 defines the admissible region for variable 𝑤. For any 𝑉 ∈ 𝑊 , 𝐴𝑉 =
      𝑤
        𝑣∈𝑉 𝐴𝑣 .
    • Γ = {𝛾𝑤 | 𝑤 ∈ 𝑊 ∧ 𝛾𝑤 is a quantization function for 𝐴𝑤 }, i.e., Γ is a set of quantization
      functions for all real variables in ℋ. For 𝑊 = [𝑤1 , . . . , 𝑤𝑘 ] and 𝑣 = [𝑣1 , . . . , 𝑣𝑘 ], we will
      write Γ(𝑣) for the tuple [𝛾𝑤1 (𝑣1 ), . . . , 𝛾𝑤𝑘 (𝑣𝑘 )].

  A quantized feedback control solution for a DTLHS control problem 𝒫 = (ℋ, 𝐼, 𝐺), given a
quantization 𝒬 = (𝐴, Γ) for ℋ = (𝑋, 𝑈, 𝑌, 𝑁 ), is a 𝐾 solution to 𝒫 s.t.:

    • if (𝑥, 𝑢) ∈
                / 𝐴𝑋 × 𝐴𝑈 , then 𝐾(𝑥, 𝑢) = 0;
    • otherwise, 𝐾(𝑥, 𝑢) = 𝐾 ˆ (Γ(𝑥), Γ(𝑢)), being 𝐾
                                                   ˆ : Γ(𝐴𝑋 ) × Γ(𝐴𝑈 ) → B, i.e., 𝐾 works by
      only looking at the (integer) values coming after the AD conversion.

2.6. Automatically Generating Quantized Feedback Solutions for DTLHS
     Quantized Control Problems
In the following, we focus on QKS (Quantized Kontrol Synthesizer, [43]), which takes as input a
quantization control problem 𝒫 = (ℋ, 𝐼, 𝐺) for a DTLHS ℋ = (𝑋, 𝑈, 𝑌, 𝑁 ) with quantization
𝒬 = (𝐴, Γ) and output a correct-by-construction quantized feedback control solution to 𝒫.
To this aim, QKS goes through the procedure shown in Algorithm 1. Namely, in step 1, initial
region 𝐼 and goal region 𝐺 are quantized. In step 2, a minimal control abstraction is computed
as an LTS ℋ̂(Γ(𝐴𝑋 ), Γ(𝐴𝑈 ), 𝑁    ˆ ). In a nutshell, in the minimal control abstraction, each abstract
transition in 𝑁 ˆ stems from some concrete transition in ℋ and viceversa, i.e., 𝑁             ˆ, 𝑠ˆ′ ) if and
                                                                                       ˆ (𝑠ˆ, 𝑎
only if there exists 𝑦 ∈ 𝑌 s.t. 𝑁 (𝑠, 𝑎, 𝑠′ ) holds. Some special cases (self loops and actions going
outside the admissible region 𝐴) are treated separately [43]. In step 3, the output quantized
controller 𝐾 ˆ is computed with its domain 𝐷   ˆ and a boolean value 𝑏 which is true iff 𝐼ˆ ⊆ 𝑑𝑜𝑚(𝐾        ˆ ),
i.e., if 𝐾 is able to control all states in the initial region. Note that, if 𝑏 is false, QKS provides
         ˆ
a necessary condition (not detailed here) for controller existence. The quantized controller
synthesis for DTLHSs is actually an undecidable problem [49].

Algorithm 1 QFC Synthesis Algorithm
Input: DTLHS control problem (ℋ, 𝐼, 𝐺), quantization 𝒬 = (𝐴, Γ)
function: 𝑞𝐶𝑡𝑟𝑆𝑦𝑛𝑡(ℋ, 𝒬, 𝐼, 𝐺)
    ˆ ← Γ(𝐼), 𝐺
 1: 𝐼         ˆ ← Γ(𝐺)
 2: ℳ̂ ← 𝑚𝑖𝑛𝐶𝑡𝑟𝐴𝑏𝑠(ℋ, 𝒬)
        ˆ,𝐾
 3: (𝑏, 𝐷                         ˆ ) return (𝑏, 𝐷
          ˆ ) ← 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟(ℳ̂, 𝐼ˆ, 𝐺              ˆ,𝐾
                                                   ˆ)


   Algorithm 2 details the computation performed in step 3 of Algorithm 1. Namely, function
𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟 starts with an empty controller (step 1). Then, a loop is performed in which, at the
𝑖-th iteration, the states which are at worst case distance 𝑖 from the goal for some action 𝑎 (𝐹
in step 3) are added to 𝐾, provided that no other actions already existed for those states (with
distance 𝑗 < 𝑖, step 4). All computations are performed representing sets as OBDDs (Ordered
Binary Decision Diagrams) [50, 51].

Algorithm 2 Most General Optimal Controller Synthesis
Input: An LTS control problem (𝒮, 𝐼, 𝐺), 𝒮 = (𝑆, 𝐴, 𝑇 ).
function: 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟(𝒮, 𝐼, 𝐺)
 1: 𝐾(𝑠, 𝑎) ← 0, 𝐷(𝑠) ← 𝐺(𝑠), 𝐷     ˜ (𝑠) ← 0
                   ˜
 2: while 𝐷(𝑠) ̸= 𝐷 (𝑠) do:
 3:   𝐹 (𝑠, 𝑎) ← ∃𝑠′ 𝑇 (𝑠, 𝑎, 𝑠′ ) ∧ ∀𝑠′ [𝑇 (𝑠, 𝑎, 𝑠′ ) ⇒ 𝐷(𝑠′ )]
 4:   𝐾(𝑠, 𝑎) ← 𝐾(𝑠, 𝑎) ∨ (𝐹 (𝑠, 𝑎) ∧ ̸ ∃𝑎 𝐾(𝑠, 𝑎))
 5:   𝐷˜ (𝑠) ← 𝐷(𝑠), 𝐷(𝑠) ← 𝐷(𝑠) ∨ ∃𝑎 𝐾(𝑠, 𝑎)
 6: return ⟨∀𝑠 [𝐼(𝑠) ⇒ ∃𝑎 𝐾(𝑠, 𝑎)], ∃𝑎 𝐾(𝑠, 𝑎), 𝐾(𝑠, 𝑎)⟩




3. Stabilizing Controllers
The quantized controllers defined in Section 2 are designed so that to drive all controlled
states inside the goal infinitely often. That is, for a DTLHS control problem 𝒫 = (ℋ, 𝐼, 𝐺),
if 𝑠 ∈ 𝐺, then a controller 𝐾 can possibly enable an action 𝑎 leading to a state 𝑠′ ∈
                                                                                    / 𝐺, i.e.,
𝐾(𝑠, 𝑎) ∧ ∃𝑠′ [𝑁                     / 𝐺]. However, 𝐾 will eventually bring all descendants of 𝑠′ back
                  ˜ (𝑠, 𝑎, 𝑠′ ) ∧ 𝑠′ ∈
into 𝐺, i.e., if 𝒮 = 𝐿𝑇 𝑆(ℋ), ∀𝑎 ∈ 𝐴. 𝐾(𝑠′ , 𝑎) → ∀𝜋 ∈ 𝑃 𝑎𝑡ℎ(𝒮 (𝐾) , 𝑠′ , 𝑎). ∃𝑛 𝜋 𝑆 (𝑛) ∈ 𝐺.
   In some safety- or mission-critical applications, this could not be enough, as it is desired
that, once the goal is reached, the controller does not let any state escape from it, i.e., ∀𝑠 ∈
𝐺 ∩ 𝑑𝑜𝑚(𝐾), if 𝐾(𝑠, 𝑎) then ∀𝑠′ . 𝑁 (𝑠, 𝑎, 𝑠′ ) → 𝑠′ ∈ 𝐺. If a controller succeeds in doing this,
then it is said to be a stabilizing controller.
   It is easy to see that, for a given quantized DTLHS control problem, if a stabilizing controller
𝐾 exists, then QKS returns 𝐾. In fact, function 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟 in Algorithm 2 always returns the
action with the lowest (worst case) distance from the goal, thus if there exists an action 𝑎 which
directly maintains a goal state 𝑔 ∈ 𝐺 inside the goal, 𝑎 is enabled in 𝑔 by 𝐾. If another action 𝑏
is enabled in 𝑔 by 𝐾, it must not have the same distance as 𝑎, thus it is stabilizing as well.
   Unfortunately, the procedure used by QKS does not detect if the output controller is actually
stabilizing or not. In this paper, we present an automatic procedure which modifies function
𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟 so that the controlled states are all stabilized in the goal for at least 𝑙 ≥ 0 steps,
where 𝑙 is an additional input to both 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟 and 𝑞𝐶𝑡𝑟𝑆𝑦𝑛𝑡 (Algorithm 1). That is, the
output 𝐾𝑙 must be an 𝑙-stabilizing controller such that:

   1. 𝐾𝑙 is a strong controller for the problem 𝒫.
   2. ∀ 𝑠 ∈ 𝑑𝑜𝑚(𝐾𝑙 ) ∀ 𝑎 ∈ 𝐴𝑑𝑚(𝒮, 𝑠) 𝐾𝑙 (𝑠, 𝑎) holds if and only if ∀𝑖 ≥ 0, 𝜋 ∈ 𝑃 𝑎𝑡ℎ(𝒮 (𝐾𝑙 ) ,
      𝑠, 𝑎). 𝜋 (𝑆) (𝑖) ∈ 𝐺 → [∀ 𝑗 = 1, . . . , 𝑙 − 1. 𝜋 (𝑆) (𝑗 + 𝑖) ∈ 𝐺].


4. Synthesis of Stabilizing Controllers
In order to compute the 𝑙-stabilizing controller for a quantized DTLHS control problem 𝒫 =
(ℋ, 𝐼, 𝐺) with quantization 𝒬, we modified function 𝑞𝐶𝑡𝑟𝑆𝑦𝑛𝑡 of Algorithm 1 so that: i) it
takes an integer 𝑙 ≥ 0 as an additional input; ii) in step 3, it calls function 𝑠𝑡𝑟𝑜𝑛𝑔𝑆𝑡𝑎𝑏𝐶𝑡𝑟
instead of function 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟, also passing 𝑙 to it.

Algorithm 3 Stabilizing Controller Synthesis
Input: An LTS control problem (𝒮, 𝐼, 𝐺), 𝒮 = (𝑆, 𝐼, 𝐺), integer 𝑙 ≥ 0.
function: 𝑠𝑡𝑟𝑜𝑛𝑔𝑆𝑡𝑎𝑏𝐶𝑡𝑟(𝒮, 𝐼, 𝐺, 𝑙)
 1: 𝐾𝑙 (𝑠, 𝑎) ← 0, 𝐷(𝑠) ← 0, 𝐷        ˜ (𝑠) ← 1
                     ˜
 2: while 𝐷(𝑠) ̸= 𝐷 (𝑠)) do:
 3:   𝐹 (𝑠, 𝑎) ← ∃𝑠′ 𝑇 (𝑠, 𝑎, 𝑠′ ) ∧ ∀𝑠′ [𝑇 (𝑠, 𝑎, 𝑠′ ) ⇒ (𝐷(𝑠′ ) ∨ (𝐺(𝑠′ ) ∧
 4:           ∧ ∀𝑠1 𝑎1 , . . . , 𝑠𝑙 𝑎𝑙 𝑠1 = 𝑠′ ∧ ∀𝑖 = 1, . . . , 𝑙 [𝑇 (𝑠𝑖 , 𝑎𝑖 , 𝑠𝑖+1 ) ⇒ 𝐺(𝑠𝑖+1 )])]
 5:   𝐾𝑙 (𝑠, 𝑎) ← 𝐾𝑙 (𝑠, 𝑎) ∨ (𝐹 (𝑠, 𝑎) ∧ ̸ ∃𝑎 𝐾𝑙 (𝑠, 𝑎))
 6:   𝐷˜ (𝑠) ← 𝐷(𝑠), 𝐷(𝑠) ← 𝐷(𝑠) ∨ ∃𝑎 𝐾𝑙 (𝑠, 𝑎)
 7: return ⟨∀𝑠 [𝐼(𝑠) ⇒ ∃𝑎 𝐾𝑙 (𝑠, 𝑎)], ∃𝑎 𝐾𝑙 (𝑠, 𝑎), 𝐾𝑙 (𝑠, 𝑎)⟩


   We then added function 𝑠𝑡𝑟𝑜𝑛𝑔𝑆𝑡𝑎𝑏𝐶𝑡𝑟 to QKS, which is detailed in Algorithm 3. Functions
𝑠𝑡𝑟𝑜𝑛𝑔𝑆𝑡𝑎𝑏𝐶𝑡𝑟 and 𝑠𝑡𝑟𝑜𝑛𝑔𝐶𝑡𝑟 are similar, but with important differences. Both use a set 𝐷(𝑠)
(set of controlled states) to accumulate all found controllable states in the current iteration and
a set 𝐷
      ¯ (𝑠) to store all controlled states up to the previous iteration. Basically, the idea is to end
the computation when the procedure does not find other controllable states. Iteratively, both
procedures look for new pairs state-action. After that, they update the 𝐷         ¯ (𝑠) to the previous
iteration and add new controllable states to 𝐷(𝑠).
   The main difference is in selecting pairs state-action. The state-of-the-art condition requires
that a state 𝑠 is controllable if, for a given action 𝑎, it presents at least a transition to successor
state and, every successor state is inside the set of controlled states. A controlled state can be
inside the goal region or belongs to a path that brings the system to the goal region. Since the
set of the controlled state is initialized as the set of states within the goal region, the condition
works.
   By contrast, stabilizing controllers are required to check also the stabilizing subpath inside 𝐺.
This new condition establishes that each state is controllable if:

    • it presents at least a successor state;
    • every successor state either is inside the set of controlled states or belongs to the goal
      region along with a next stabilizing subpath of length 𝑙 where each state is inside the goal
      region.

  In such a way, a state can be controlled even when it belongs to a path that brings the system
up to 𝐺 and stabilizes it inside 𝐺. Making a comparison between these two conditions, we can
see how stabilizing controllers incrementally restrict possible paths of the system, because any
shortest stabilizing subpath than 𝑙 inside the goal region is discarded.


5. Experimental Results
To establish the viability of our approach, we provided a C implementation of our algorithm
inside QKS. We exploited the OBDD library as for the standard strong m.g.o. synthesis algorithm.
Likewise, our algorithm will result in a controller implemented as a C function.
   We performed several experiments on two case studies: Multi-Buck DC-DC converter [52, 53]
and Inverted Pendulum [54]. We provided experimental results on several configurations of
Multi-Buck DC-DC converter in terms of switches. For the inverted pendulum, instead, we
have one configuration. We used several machines on High-Performance Computing (HPC)
infrastructure to synthesize the output controller. The quantization of the control problem
requires specifying the number of bits for the quantization schema. We carried out several runs
by using 9, 10 and 11 bits. Moreover, we incremented the size of 𝑙 according to obtained results.
When QKS did not find a stabilizing controller for a given 𝑙, we terminated the experiments on
that model.

5.1. Multi Buck DC-DC converter
5.1.1. Case study description
Buck DC-DC converter is a mixed-mode circuit that converts DC input voltage to desired output
DC output voltage. For example, it is used to scale down to typical laptop battery voltage
(12-24) getting a few low voltages needed by laptop processor (e.g., [53]). Another example
                                                                                                                     m
             +𝑣𝑛𝑢                                                                                            θ
                     𝑢𝑛
               𝐼𝑛𝑢
                       𝑢
                     +𝑣𝑛−1                 𝐷  𝐷
                                     𝑢𝑛−1+𝑣𝑛−1 𝑛−1
                             𝑢
                            𝐼𝑛−1
                                                                        𝑖𝐿                                       l
                                         +𝑣𝑖𝑢         +𝑣 𝐷
                                                     𝑢𝑖 𝑖 𝐷𝑖                    𝑟𝐿
                                                                                           +𝑣𝑂
     𝑉𝑛                                     𝐼𝑖𝑢                             𝐿
                          ...                         +𝑣1𝑢
            𝑉𝑛−1                                               𝑢1 𝐷1
                                                                                +𝑣𝐶   𝐶                      F
                                𝑉𝑖         ...         𝐼1𝑢 +𝑣1𝐷                            𝑅
                                                𝑉1                     𝐷0       𝑖𝐶    𝑟𝐶
                                                                 +𝑣𝐷
                                                                       𝑖𝐷


          (a) Multi-input Buck DC-DC converter                                                   (b) Inverted Pendulum
Figure 1: Case studies for experiments


concerns to support Dynamic Voltage and Frequency Scaling (DVFS) in multicore processors (e.g.,
[55]). A typical software approach manages the switches 𝑢1 , ...𝑢𝑛 through a microcontroller.
In such a model, shown in Figure 1a, we have 𝑛 power supplies with voltage 𝑉1 , ..., 𝑉𝑛 . 𝑛
switches with voltage 𝑣1𝑢 , ...., 𝑣𝑛𝑢 . Current values 𝐼1𝑢 , ...., 𝐼𝑛𝑢 . 𝑛 input diodes 𝐷0 , ...., 𝐷𝑛−1 and
current 𝑖𝐷0 , ...., 𝑖𝑛−1 . The circuit state variables are 𝑖𝐿 and 𝑣𝑂 . In the following we recall the
                     𝐷

guarded predicate which model the multi-buck as a DTLHS, where coefficients 𝑎𝑖 depend on
circuit parameters as follows: 𝑎1,1 = − 𝑟𝐿𝐿 , 𝑎1,2 = − 𝐿1 , 𝑎1,3 = − 𝐿1 , 𝑎2,1 = 𝑟𝑐𝑅               𝑟𝑐 𝑟𝐿
                                                                                         +𝑅 [− 𝐿 + 𝐶 ],
                                                                                                         1

          +𝑅 [ 𝐿 + 𝐶 ], 𝑎2,3 = − 𝐿 𝑟𝑐 +𝑅 . For a complete discussion see [48]).
𝑎2,2 = 𝑟𝑐−1     𝑟𝑐 𝑅     1             1 𝑟𝑐 𝑅


    𝑖′𝐿 = (1 + 𝑇 𝑎1,1 )𝑖𝐿 + 𝑇 𝑎1,2 𝑣𝑂 + 𝑇 𝑎1,3 𝑣𝐷            𝑣𝐷 = 𝑣𝑛𝑢∑︀
                                                                      − 𝑉𝑛                  𝑞0 → (𝑖𝐷 ≥ 0)
      ′
    𝑣𝑂 = 𝑇 𝑎⋀︀2,1 𝑖𝐿 + (1 + 𝑇 𝑎2,2 )𝑣𝑂 + 𝑇 𝑎2,3 𝑣𝐷       𝑖𝐿 = 𝑖𝐷 + 𝑛𝑖=1 𝐼𝑖𝑢                ¯𝑞 0 → (𝑣𝐷 ≤ 0)
                      𝑞 → (𝑣𝑖𝐷 = 𝑅on 𝐼𝑖𝑢 )               𝑞 → (𝑣𝐷 = 𝑅on 𝑖𝐷 )             ¯𝑞 → (𝑣𝐷 = 𝑅off 𝑖𝐷 )
            ⋀︀ 𝑖∈[𝑛] 𝑖                                  ⋀︀0                            ⋀︀0
                     ¯𝑞 𝑖 → (𝑣𝑖𝐷 = 𝑅off 𝐼𝑖𝑢 )                    𝑞𝑖 → (𝐼𝑖𝑢 ≥ 0)                 ¯𝑞 → (𝑣 𝐷 ≤ 0)
           ⋀︀  𝑖∈[𝑛]
                                𝑢           𝑢
                                                   ⋀︀      𝑖∈[𝑛]
                                                                       𝑢         𝑢
                                                                                     ⋀︀ 𝑖∈[𝑛] 𝑖 𝑢 𝑖 𝐷
              𝑗∈[𝑛−1] 𝑢𝑗 → (𝑣𝑗 = 𝑅on 𝐼𝑗 )             𝑗∈[𝑛−1] 𝑢¯ 𝑗 → (𝑣𝑗 = 𝑅off 𝐼𝑗 )   𝑖∈[𝑛] 𝑣𝐷 = 𝑣𝑖 + 𝑣𝑖 − 𝑉𝑖


5.1.2. Experiments evaluation
We used three different configurations of the non-robust buck DC-DC converter. We carried out
experiments with 𝑛 = 1, 2, 3 in the number of switches. For every configuration, as a baseline,
we synthesized a controller also using the standard strong m.g.o. synthesis algorithm (𝑙 = 0).
  Our experimental results are shown in Table 1. Columns in Table 1 have the following
meaning: 𝑛 is the number of power supplies in the multi-buck, Bits is the number of bits used
for the quantization of the DTLHS state variables, 𝑙 is the value for the 𝑙-stabilizing controller,
Nodes is the number of internal nodes of the OBDD representing the resulting 𝑙-stabilizing
controller, Actions and States are the number of actions enabled and the number of states
controlled by the resulting 𝑙-stabilizing controller, and finally Memory and Time provide the
RAM usage in MB and the execution time in seconds, respectively.
  As shown in Table 1, we are able to synthesize only 0-stabilizing controllers using 9 bits. By
contrast, using 10 and 11 bits, our runs result in a strong controller with stabilizing length 𝑙 = 1
for 𝑛 = 1, 2, 3 power supplies. In any case, we did not obtain a stabilizing controller for 𝑙 = 2.
  We simulated the system with 𝑛 = 1 power supplies and 𝑏 = 10 bits for the AD quantization.
          (a) 𝑣𝑂 simulation trajectories                     (b) 𝑖𝐿 simulation trajectories
Figure 2: Multi-Buck DC-DC simulations with n=1 and b=10 bits


The starting state of the simulation is 𝑣𝑂 = 4 and 𝑖𝐿 = 3. We obtained the trajectories reported
in Figure 2 over a time horizon 𝑇 ∈ [0, 200] in three different settings: without a controller,
control-loop with the 0-stabilizing controller, and control-loop with the 1-stabilizing controller.
In Figure 2a, we can observe how both controllers drive the system toward the goal region.
However, the 1-stabilizing controller stabilizes the system faster than the 0-stabilizing controller,
and it provides better stability inside the goal region. Conversely, Figure 2b shows that in any
case, the current value reaches the goal, but still, 𝑙-stabilizing controllers, incrementally in terms
of 𝑙, lead to better stability.




                       (a) Actions                         (b) 1-Stabilizing Controller
Figure 3: Multi-Buck DC-DC experiment with n=1 and b=10 bits


   In Figure 3 we provide a visual representation for 𝑛 = 1 power supplies and 𝑏 = 10 bits for
the AD quantization. Figure 3a encodes action 1 with green, 0 with purple and any action with
pink. It illustrates the distribution of actions inside the control region. Figure 3b shows the
distribution of actions in the control region.
   The synthesis of stabilizing controllers involves a higher computational cost. In fact, the
size of 𝑙 increases the amount of memory and time needed for a single computation. In such a
context, both the memory usage and execution time depend on the number of bits used for the
quantization schema, the size of the model and the length of the stabilizing subpath specified
by the user.
Table 1
Multi Buck DC-DC converter experiments
           𝑛    Bits   𝑙   Nodes    Actions     States    Memory (MB)        Time (s)
            1    9     0    3246     255309    223703         218.07       2.213460e+03
            1    9     1     1         0          0           298.36       2.269390e+03
            1    10    0   12207    1048770    943713         552.08       9.285320e+03
            1    10    1   11865    1042325    943713         876.57       2.681168e+04
            1    10    2     1         0          0           1952.13      8.743820e+03
            1    11    0   32597    4312433    3840526        1832.43      3.896438e+04
            1    11    1   31216    4277932    3840526        3184.59      9.040446e+04
            1    11    2     1         0          0           7956.45      3.257370e+04
            2    9     0    8063     318057    237420         337.75       5.760150e+03
            2    9     1     1         0          0           433.08       5.258140e+03
            2    10    0   25977    1290474    986115         978.55       2.171697e+04
            2    10    1   25145    1260858    986115         1475.83      4.703410e+04
            2    10    2     1         0          0           2975.62      1.545672e+04
            2    11    0   62733    5314364    3981081        3520.31      9.021701e+04
            2    11    1   60308    5202979    3981081        5392.5       1.530524e+05
            2    11    2     1         0          0          12096.40      6.382998e+04
            3    9     0   12150     946463    240977         558.31       1.249221e+04
            3    9     1     1         0          0           682.47       1.150078e+04
            3    10    0   37201    3817353    997023         1829.64      4.669121e+04
            3    10    1   37101    3767342    997023         2502.92      5.028375e+04
            3    10    2     1         0          0           4849.4       3.937717e+04
            3    11    0   91502    15715546   4022278        6855.14      1.629664e+05
            3    11    1   92178    15390590   4022278        9474.27      2.455190e+05
            3    11    2     1         0          0          20331.05      1.588620e+05


5.2. Inverted Pendulum
5.2.1. Case study description
The controller synthesis for the Inverted Pendulum (IP) [54] is widely studied through QKS
(e.g., [56, 57, 48]). The system, shown in Figure 1b, is modelled by using an angle 𝜃 and the
angular velocity 𝜃̇ as a state variables. The input variable is the torquing force that influences
the torquing velocity in both directions. The input of the system is the torquing force 𝑢 · 𝐹
which can influence the velocity in any direction. 𝑢 is the direction and 𝐹 is the intensity of the
force. In this problem, we try to find a discrete controller whose actions can be: “apply the force
clockwise” (𝑢 = 1), “apply the force counterclockwise” (𝑢 = −1) and “do nothing” (𝑢 = 0). The
behaviour of the system is based on the pendulum mass 𝑚, the length of the pendulum 𝑙 and the
gravitational acceleration 𝑔. The motion of the system is described by the differential equation
𝜃̇ = 𝑔𝑙 sin 𝜃 + 𝑚𝑙1 2 𝑢𝐹 . In the following we recall the guarded predicate which model the inverted
pendulum as a DTLHS, where 𝑦𝜉 variables are in 𝑌 and 𝐼𝑗 for 𝑗 = 1, . . . , 4 represent a partition
of the interval [−𝜋, 𝜋]. For a complete discussion see [48].
                                                  𝑔          1
      (𝑥′1 = 𝑥1 + 2𝜋𝑦𝑞 + 𝑇 𝑥2 ) ∧ (𝑥′2 = 𝑥2 + 𝑇 𝑦sin + 𝑇 2 𝑢𝐹 )
                                                   𝑙 ⋀︀     𝑚𝑙
        ∧ 𝑖∈[4] 𝑦𝑖 → 𝑓𝑖− (𝑦𝛼 ) ≤ 𝑦sin ≤ 𝑓𝑖+ (𝑦𝛼 ) ∧ 𝑖∈[4] 𝑦𝑖 → 𝑦𝛼 ∈ 𝐼𝑖 ∧ 𝑖∈[4] 𝑦𝑖 ≥ 1
           ⋀︀                                                           ∑︀

        ∧ 𝑥1 = 2𝜋𝑦𝑘 + 𝑦𝛼 ∧ −𝜋 ≤ 𝑥′1 ≤ 𝜋

5.2.2. Experiments evaluation
Our experimental results are shown in Table 2. Columns in Table 2 have the same meaning of
the columns with the same name in Table 1. We note that, in such a case study, only 0-stabilizing
controllers exist.

Table 2
Inverted pendulum experiments
              Bits   𝑙   Nodes   Actions    States    Memory (MB)         Time
               9     0   12238   453843    262144        324.87       7.200670e+03
               9     1     1        0         0          455.29       6.550130e+03
               10    0   24878   1831288   1048576        916.39      3.348904e+04
               10    1     1        0         0          1495.06      3.536044e+04
               11    0   51110   7335238   4194304       3229.16      1.658496e+05
               11    1     1        0         0          5602.21      1.640529e+05




6. Conclusions
We provided a new concept of controllers along with a specific synthesis algorithm. Ensuring the
system meets liveness/safety property is a key goal in safety/mission-critical contexts. On such
a basis, the development of correct-by-construction controllers increasing safety guarantees can
become a challenge for many CPSs. On the other hand, the experiments showed several settings
in which we can not obtain stabilizing controllers. Moreover, each performed run required
more computational resources (i.e., time and memory) than the standard synthesis algorithm.
However, the need for correctness of safety/mission-critical systems justifies the usage of a
higher quantity of computational resources.
   As future works, we may go in several directions. Firstly, we plan to provide a simulation
environment as a tool to observe the resulting trajectories of the input system in the closed-loop
with the controller provided by QKS. Secondly, to extend the algorithm of weak controller
synthesis to give the user some information about stabilizing controllers (if the strong algorithm
fails). Thirdly, to perform computational evaluations to establish the computational cost in
terms of user-defined input parameters. Last but not least, we plan to provide more experimental
results on several case studies.
Acknowledgments
This work was partially supported by: Italian Ministry of University and Research under grant
“Dipartimenti di eccellenza 2018–2022” of the Department of Computer Science of Sapienza
University of Rome.


References
 [1] A. Basu, S. Bensalem, M. Bozga, B. Delahaye, A. Legay, E. Sifakis, Verification of an AFDX
     infrastructure using simulations and probabilities, in: RV 2010, volume 6418 of LNCS,
     Springer, 2010. doi:10.1007/978-3-642-16612-9_25.
 [2] L. Planke, Y. Lim, A. Gardi, R. Sabatini, T. K., N. Ezer, A cyber-physical-human system for
     one-to-many uas operations: Cognitive load analysis, Sensors 20 (2020). doi:10.3390/
     s20195467.
 [3] Z. Wu, N. Huang, X. Zheng, X. Li, Cyber-physical avionics systems and its reliability
     evaluation, in: IEEE CYBER 2014, IEEE, 2014. doi:10.1109/CYBER.2014.6917502.
 [4] K. Sampigethaya, R. Poovendran, Aviation cyber-physical systems: Foundations for future
     aircraft and air transport, Proc. IEEE 101 (2013). doi:10.1109/JPROC.2012.2235131.
 [5] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Prodanovic,
     L. Elmegaard, Demand-aware price policy synthesis and verification services for smart
     grids, in: SmartGridComm 2014, IEEE, 2014. doi:10.1109/SmartGridComm.2014.
     7007745.
 [6] I. Melatti, F. Mari, T. Mancini, M. Prodanovic, E. Tronci, A two-layer near-optimal strategy
     for substation constraint management via home batteries, IEEE Trans. Ind. Elect. (2021).
     doi:10.1109/TIE.2021.3102431.
 [7] B. Hayes, I. Melatti, T. Mancini, M. Prodanovic, E. Tronci, Residential demand management
     using individualised demand aware price policies, IEEE Trans. Smart Grid 8 (2017). doi:10.
     1109/TSG.2016.2596790.
 [8] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Prodanovic,
     L. Elmegaard, User flexibility aware price policy synthesis for smart grids, in: DSD 2015,
     IEEE, 2015. doi:10.1109/DSD.2015.35.
 [9] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, L. Elmegaard, Parallel
     statistical model checking for safety verification in smart grids, in: SmartGridComm 2018,
     IEEE, 2018. doi:10.1109/SmartGridComm.2018.8587416.
[10] D. Goswami, R. Schneider, A. Masrur, M. Lukasiewycz, S. Chakraborty, H. Voit, A. An-
     naswamy, Challenges in automotive cyber-physical systems design, in: SAMOS 2012,
     IEEE, 2012. doi:10.1109/SAMOS.2012.6404199.
[11] S. Chakraborty, M. Al Faruque, W. Chang, D. Goswami, M. Wolf, Q. Zhu, Automotive
     cyber–physical aystems: A tutorial introduction, IEEE Des.&Test 33 (2016). doi:10.1109/
     MDAT.2016.2573598.
[12] L. Zhang, Modeling automotive cyber physical systems, in: DCABES 2013, IEEE, 2013.
     doi:10.1109/DCABES.2013.20.
[13] S. Osswald, S. Matz, M. Lienkamp, Prototyping automotive cyber-physical systems, in:
     Adjunct Proceedings of the 6th International Conference on Automotive User Interfaces
     and Interactive Vehicular Applications, 2014, pp. 1–6.
[14] M. Hengartner, T. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Roeblitz,
     R. Ehrig, L. Saleh, K. Spanaus, C. Schippert, Y. Zhang, B. Leeners, Negative affect is
     unrelated to fluctuations in hormone levels across the menstrual cycle: Evidence from
     a multisite observational study across two successive cycles, J. Psycho. Res. 99 (2017).
     doi:10.1016/j.jpsychores.2017.05.018.
[15] B. Leeners, T. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Roeblitz, L. Saleh,
     K. Spanaus, C. Schippert, Y. Zhang, M. Hengartner, Lack of associations between female
     hormone levels and visuospatial working memory, divided attention and cognitive bias
     across two consecutive menstrual cycles, Front. Behav. Neuro. 11 (2017). doi:10.3389/
     fnbeh.2017.00120.
[16] B. Leeners, T. Krüger, K. Geraedts, E. Tronci, T. Mancini, M. Egli, S. Röblitz, L. Saleh,
     K. Spanaus, C. Schippert, Y. Zhang, F. Ille, Associations between natural physiological
     and supraphysiological estradiol levels and stress perception, Front. Psycol. 10 (2019).
     doi:10.3389/fpsyg.2019.01296.
[17] F. Maggioli, T. Mancini, E. Tronci, SBML2Modelica: Integrating biochemical models
     within open-standard simulation ecosystems, Bioinformatics 36 (2020). doi:10.1093/
     bioinformatics/btz860.
[18] T. Mancini, E. Tronci, I. Salvo, F. Mari, A. Massini, I. Melatti, Computing biological model
     parameters by parallel statistical model checking, in: IWBBIO 2015, volume 9044 of LNCS,
     Springer, 2015. doi:10.1007/978-3-319-16480-9_52.
[19] T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, S. Sinisi, E. Tronci, R. Ehrig, S. Röblitz,
     B. Leeners, Computing personalised treatments through in silico clinical trials. A case
     study on downregulation in assisted reproduction, in: RCRA 2018, volume 2271 of CEUR
     W.P., CEUR, 2018.
[20] E. Tronci, T. Mancini, I. Salvo, S. Sinisi, F. Mari, I. Melatti, A. Massini, F. Davi’, T. Dierkes,
     R. Ehrig, S. Röblitz, B. Leeners, T. Krüger, M. Egli, F. Ille, Patient-specific models from
     inter-patient biological models and clinical records, in: FMCAD 2014, IEEE, 2014. doi:10.
     1109/FMCAD.2014.6987615.
[21] S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, B. Leeners, Complete populations of
     virtual patients for in silico clinical trials, Bioinformatics 36 (2020). doi:10.1093/
     bioinformatics/btaa1026.
[22] S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, F. Mari, B. Leeners, Optimal personalised
     treatment computation through in silico clinical trials on patient digital twins, Fundam.
     Inform. 174 (2020). doi:10.3233/FI-2020-1943.
[23] S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, Reconciling interoperability with efficient
     verification and validation within open source simulation environments, Simul. Model.
     Pract. Theory 109 (2021). doi:10.1016/j.simpat.2021.102277.
[24] W. Brogan, Modern Control Theory (3rd Ed.), Prentice H., 1991. doi:10.5555/135299.
[25] M. Cadoli, T. Mancini, F. Patrizi, SAT as an effective solving technology for constraint
     problems, in: ISMIS 2006, volume 4203 of LNCS, Springer, 2006.
[26] M. Cadoli, T. Mancini, Combining relational algebra, SQL, constraint modelling, and local
     search, TPLP 7 (2007). doi:10.1017/S1471068406002857.
[27] T. Mancini, P. Flener, J. Pearson, Combinatorial problem solving over relational databases:
     View synthesis through constraint-based local search, in: SAC 2012, ACM, 2012. doi:10.
     1145/2245276.2245295.
[28] G. Gottlob, G. Greco, T. Mancini, Conditional constraint satisfaction: Logical foundations
     and complexity, in: IJCAI 2007, 2007.
[29] T. Mancini, M. Cadoli, Detecting and breaking symmetries by reasoning on problem
     specifications, in: SARA 2005, volume 3607 of LNCS, Springer, 2005.
[30] T. Mancini, M. Cadoli, D. Micaletto, F. Patrizi, Evaluating ASP and commercial solvers on
     the CSPLib, Constraints 13 (2008).
[31] E. Clarke, O. Grumberg, D. Peled, Model Checking, MIT, 1999.
[32] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli, Bounded probabilistic
     model checking with the Mur𝜙 verifier, in: FMCAD 2004, IEEE, 2004.
[33] T. Mancini, F. Mari, A. Massini, I. Melatti, F. Merli, E. Tronci, System level formal verification
     via model checking driven simulation, in: CAV 2013, volume 8044 of LNCS, Springer, 2013.
     doi:10.1007/978-3-642-39799-8_21.
[34] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci, System level formal verification
     via distributed multi-core hardware in the loop simulation, in: PDP 2014, IEEE, 2014.
     doi:10.1109/PDP.2014.32.
[35] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci, Anytime system level verification
     via random exhaustive hardware in the loop simulation, in: DSD 2014, IEEE, 2014. doi:10.
     1109/DSD.2014.91.
[36] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci, SyLVaaS: System level formal
     verification as a service, in: PDP 2015, IEEE, 2015. doi:10.1109/PDP.2015.119.
[37] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci, SyLVaaS: System level formal
     verification as a service, Fundam. Inform. 149 (2016). doi:10.3233/FI-2016-1444.
[38] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci, Anytime system level verification
     via parallel random exhaustive hardware in the loop simulation, Microprocessors and
     Microsystems 41 (2016). doi:10.1016/j.micpro.2015.10.010.
[39] T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, E. Tronci, On minimising the maximum
     expected verification time, Inf. Proc. Lett. 122 (2017). doi:10.1016/j.ipl.2017.02.001.
[40] T. Mancini, I. Melatti, E. Tronci, Any-horizon uniform random sampling and enumeration
     of constrained scenarios for simulation-based formal verification, IEEE TSE (2021). doi:10.
     1109/TSE.2021.3109842.
[41] M. Mazo, A. Davitian, P. Tabuada, PESSOA: A tool for embedded controller synthesis, in:
     CAV 2010, volume 6174 of LNCS, Springer, 2010. doi:10.1007/978-3-642-14295-6_
     49.
[42] H. Peter, R. Ehlers, R. Mattmüller, Synthia: Verification and synthesis for timed automata,
     in: CAV 2011, volume 6806 of LNCS, Springer, 2011. doi:10.1007/978-3-642-22110-1_
     52.
[43] F. Mari, I. Melatti, I. Salvo, E. Tronci, Model based synthesis of control software from
     system level formal specifications, ACM TOSEM 23 (2014).
[44] F. Dullerud, G.E.and Paganini, Stabilizing Controllers, Springer, 2000. doi:10.1007/
     978-1-4757-3290-0_6.
[45] V. M. Popov, R. Georgescu, Hyperstability of Control Systems, Springer, 1973. doi:10.
     5555/578779.
[46] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, E. Tronci, On-the-fly control software
     synthesis, in: SPIN 2013, volume 7976 of LNCS, Springer, 2013. doi:10.1007/
     978-3-642-39176-7_5.
[47] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, E. Tronci, A map-reduce parallel approach to
     automatic synthesis of control software, in: SPIN 2013, volume 7976 of LNCS, Springer,
     2013. doi:10.1007/978-3-642-39176-7_4.
[48] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, E. Tronci, On model based synthesis of embedded
     control software, in: EMSOFT 2012, ACM, 2012. doi:10.1145/2380356.2380398.
[49] F. Mari, I. Melatti, I. Salvo, E. Tronci, Undecidability of quantized state feedback control
     for discrete time linear hybrid systems, in: ICTAC 2012, volume 7521 of LNCS, Springer,
     2012. doi:10.1007/978-3-642-32943-2_19.
[50] R. Bryant, Binary decision diagrams and beyond: Enabling technologies for formal
     verification, in: ICCAD 1995, IEEE, 1995. doi:10.1109/ICCAD.1995.480018.
[51] R. Drechsler, J. Shi, G. Fey, Synthesis of fully testable circuits from BDDs, IEEE Trans.
     Comp.-Aided Des. Integr. Circ. & Sys. 23 (2004). doi:10.1109/TCAD.2004.823342.
[52] G. Schrom, P. Hazucha, J. Hahn, D. S. Gardner, B. A. Bloechel, G. Dermer, S. G. Narendra,
     T. Karnik, V. De, A 480-mhz, multi-phase interleaved buck dc-dc converter with hysteretic
     control, in: 2004 IEEE 35th annual power electronics specialists conference (IEEE Cat. No.
     04CH37551), volume 6, IEEE, 2004, pp. 4702–4707.
[53] W.-C. So, C. Tse, Y.-S. Lee, Development of a fuzzy logic controller for DC/DC converters:
     Design, computer simulation, and experimental evaluation, IEEE Trans. Pow. Electr. 11
     (1996).
[54] G. Kreisselmeier, T. Birkholzer, Numerical nonlinear regulator design, IEEE Trans. Aut.
     Contr. 39 (1994).
[55] W. Kim, M. S. Gupta, G.-Y. Wei, D. M. Brooks, Enabling on-chip switching regulators for
     multi-core processors using current staggering, Proceedings of the Work. on Architectural
     Support for Gigascale Integration (2007).
[56] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, E. Tronci, Linearizing discrete-time hybrid
     systems, IEEE TAC 62 (2017). doi:10.1109/TAC.2017.2694559.
[57] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, E. Tronci, Automatic control software synthesis
     for quantized discrete time hybrid systems, in: CDC 2012, IEEE, 2012. doi:10.1109/CDC.
     2012.6426260.