=Paper=
{{Paper
|id=Vol-3065/paper4_149
|storemode=property
|title=Automatic Synthesis of Stabilizing Controllers for Discrete Time Linear Hybrid Systems
|pdfUrl=https://ceur-ws.org/Vol-3065/paper4_149.pdf
|volume=Vol-3065
|authors=Leonardo Picchiami
|dblpUrl=https://dblp.org/rec/conf/aiia/Picchiami21
}}
==Automatic Synthesis of Stabilizing Controllers for Discrete Time Linear Hybrid Systems==
https://ceur-ws.org/Vol-3065/paper4_149.pdf
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.