Input Synthesis for Sampled Data Systems by Program Logic
Takumi Akazaki

Ichiro Hasuo

Department of Computer Science
The University of Tokyo, Japanultraredrays@is.s.u-tokyo.ac.jp

ichiro@is.s.u-tokyo.ac.jp

Kohei Suenaga
Graduate School of Informatics
Kyoto University, Japanksuenaga@fos.kuis.kyoto-u.ac.jp

Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems:
given a hybrid system that is subject to input from outside (also called disturbance or noise), findan input sequence that steers the system to the desired postcondition. In this paper we focus on
sampled data systems—systems in which a digital controller interrupts a physical plant in a periodic
manner, a class commonly known in control theory—and furthermore assume that a controller isgiven in the form of an imperative program. We develop a structural approach to input synthesisthat features forward and backward reasoning in program logic for the purpose of reducing a search
space. Although the examples we cover are limited both in size and in structure, experiments with aprototype implementation suggest potential of our program logic based approach.

1

Introduction

Cyber-physical systems (CPS)—integration of digital control with physical environments—are gaining
yet more and more importance, with cars, airplanes and all others controlled by computers. Hybrid
systems capture one of the crucial aspects of CPS, by focusing on the combination of continuous flow
dynamics and discrete jump dynamics. Quality assurance of hybrid systems is therefore a big concern inindustry as well as in academia.
In this paper we study the input synthesis problem of hybrid systems: given a hybrid system thatis subject to input from outside (also commonly called disturbance or noise), we aim to find an input
sequence that steers the system to the desired postcondition. Our interest in input synthesis stems fromthe following concrete problem; it was provided by our research partner in car manufacturing industry
as a prototype of the problems they often encounter in their design process.
Example 1.1. In the system below in Fig. 1, the controller interrupts the plant (a car) once every secondand manages the velocity v of the car. The controller chooses one mode mi and the plant operates in thatmode for one second, after which the value of v is fed back to the controller via the sensor. The problem
is to come up with an initial state of the whole system together with an input sequence i0 · · · i999 , suchthat:
• (precondition) the initial state satisfies cnt = 0 and x ∈ [−0.1, 0.1]; and• (postcondition) after 1000 seconds, the system satisfies cnt = 100.
The input synthesis problem can arise in many different contexts in quality assurance of hybrid
systems. One example is testing: the desired postcondition is the trigger for some countermeasure (e.g.
a fuse) against certain extremity (the countermeasure is outside the model); and we seek for input (i.e.
M. Bujorianu (Ed.) and R. Wisniewski (Ed.): 4th Workshop on
Hybrid Autonomous Systems 2014 (HAS 2014).
EPTCS 174, 2015, pp. 22–39, doi:10.4204/EPTCS.174.3

c T. Akazaki, I. Hasuo & K. Suenaga
This work is licensed under theCreative Commons Attribution License.

T. Akazaki, I. Hasuo & K. Suenaga

23

xs (Boolean)Sensori∈R/ xs : kv − ik ≤ 0.25?
O
v

/

if xs
then cnt := cnt + 1
else cnt := 0;
switchcnt < 25 : xa := m1
25 ≤ cnt < 50 : xa := m2
50 ≤ cnt : xa := m3
m1 : v̇ = 0.02(−v + 19)
m2 : v̇ = 0.02(−v + 5)
m3 : v̇ = 0.02(−v + 4)

Controller

xa

o
Plant

Figure 1: A hybrid systema test case) that drives the system to activating the countermeasure. The input sequence thus discoveredin the model can be fed to the physical realization of the system to see if the countermeasure works
properly.
This paper contributes an algorithm for solving the input synthesis problem. Its novelty is the use of
program logic: we make the most of the structures expressed in the digital controller given in the formof a program. In fact, a likely human effort for the problem in Example 1.1 is:(∗) “for the system to have cnt = 100 at time k = 1000, the Boolean value xs must be true
from k = 900 through k = 999, and . . . ”;
this is nothing but reasoning in program logic and is included in our proposed algorithm.
More specifically, we restrict our attention to a class of hybrid systems commonly called sampled
data systems. One such system consists of a physical plant, a digital controller that periodically interrupts
the plant (for simplicity we assume a fixed interval), and a sensor that feeds the state of the plant back to
the controller. This structural assumption—restrictive yet realistic—allows us to think of the behaviors
of such systems quite much as the semantics of programs, and enables forward and backward reasoning
in program logic. In our algorithm for solving the input synthesis problem, reasoning in program logic(like the above (∗)) contributes to the reduction of the search space. Indeed our prototype implementation
successfully solves the problem in Example 1.1.
Related Work The closest to the current work is one by Zutshi, Sankaranarayanan and Tiwari [17],where they verify safety properties of sampled data systems. Their model is more expressive, in thata plant can autonomously change its modes without interruption by a controller. While their goal isreachability analysis and is different from the current paper’s, their relational abstraction technique canbe useful in our algorithm, too, in particular for the forward approximation phase.
SMT-solver based approaches [6, 8] to hybrid system analysis are related, too, especially in theiremphases on discrete jump dynamics rather than continuous flow. Their effectivity in the input synthesis
problem is not yet clear, though: the only available implementation (that of dReal [8]) returned ‘unsat’
to Example 1.1.
More generally, an important feature of our modeling is that a digital controller is given in the formof a program, unlike an automaton used in a majority of existing work (including [8, 17]). The contrast
is comparable to the difference between the theorem proving (or type-based) approach and softwaremodel checking in program verification. While there have been results [11, 12] that suggest these two
approaches are equivalent on a fundamental level, differences do remain especially in applications. In
our proposed algorithm it is an advantage that we can exploit rich structural information that is explicit
in a program in inferring impossibility (false) more quickly.

24

Input Synthesis for Sampled Data Systems by Program Logic

The backward search phase of our algorithm resembles a membership question addressed in theseminal work by Alur et al. [2]. Since our plant (flow) dynamics is not necessarily linear, it is noteasy to see how the results in [2] can be used in our problem. They could nevertheless be applied tometa-properties of the problem such as complexity.
Fainekos and his colleagues have developed several techniques for analyzing robustness of hybrid
systems. Among them is a tool called S-Taliro [3]: it searches for a trajectory by optimization that relieson the continuous nature of the system dynamics. It is possible to encode the input synthesis problem
into an input to S-Taliro. However our leading example (Example 1.1), of a jump-heavy nature, seems
to fall out of the tool’s focus (it timed out with a smaller problem of 15, not 1000, time units).
Several techniques for testing hybrid systems have been proposed [1, 4, 5, 7, 10]. Although they
synthesize test cases and therefore seem similar to what we do here, their goal is to meet certain coverage
criteria (such as star discrepancy in [5]) and not to come up with input that steers the system to a specificdesired postcondition.
The current work is on logical analysis of hybrid systems; and in that respect it is close to Platzer’s
recent series of work (see e.g. [13]) where dynamic logic is extended in a systematic way so that it
encompasses continuous dynamics too. Also related is the work [14, 15] by some of the authors where:
flow is turned into jump with the help of nonstandard analysis; and (discrete) program logic is applied
as it is to hybrid systems.
Future Work In this paper we applied program logic to the specific problem of input synthesis. We
believe the technique have a greater potential and plan to look at other applications.
The current implementation can only handle continuous plants of dimension 1. Its extension tolarger dimensions seems feasible. Specifically, the forward approximation phase of our algorithm will
be unproblematic, while in the backward search phase we will have to give up completeness.
Currently our modeling of a sampled data system has a fixed clock cycle. It does not seem hard toaccommodate variable intervals; such extension as well as its use is a topic of our future work.
Our modeling benefits a lot from the assumption that the controller communicates with the plant andthe sensor using finite datatypes. Some hybrid systems do call for relaxation of this assumption in theirmodeling; it is our future work to see how the current input synthesis algorithm carries over to suchrelaxation.
Organization of the Paper In §2 we introduce our modeling of sampled data systems and formalize
the input synthesis problem. In §3 we describe our algorithm, explaining its three phases one by one.
In §4 our implementation is described, together with the experimental results. The proofs are deferred tothe appendix.
Acknowledgments We are grateful to the reviewers of an earlier version for their useful comments andsuggestions. T.A. and I.H. are supported by Grants-in-Aid for Young Scientists (A) No. 24680001, andby Aihara Innovative Mathematical Modeling Project, FIRST Program, JSPS/CSTP; K.S. is supported
by Grants-in-Aid for Young Scientists (B) No. 70633692 and The Hakubi Project of Kyoto University.
Notations R is the set of real numbers; B = {tt, ff} is the set of Boolean values. We let f [x0 7→ y0 ]denote function update: it carries x0 to y0 and acts as f on the other input.

T. Akazaki, I. Hasuo & K. Suenaga

2

Modeling Sampled Data Systems

2.1

Overview

Sampled data systems are a class of hybrid systems commonly known
in control theory. In those systems a physical plant is interrupted by adigital controller in a periodic manner. In the current paper where ourinterests are in input synthesis, it is convenient to explicitly separate
the third component called a sensor. The three components are thenorganized in a loop, as shown on the right in (1).
In the execution of sampled data systems thus modeled, we referto the three stages in which the sensor, the controller, and the plant
operates, respectively, as the sense, think, and act stages. Note that thesensor also takes input from outside the system.
For simplification we further assume the following.

25

(1)

1. A (digital) controller is written in an imperative programming language.
2. In the execution of a sampled data system, the sense-think-act loop is executed at fixed intervals—
once every one second. 1
3. The sense and control stages take no time for their execution.
4. The controller governs the plant by picking a mode, from a finite set {m1 , . . . , mM }. In particular,
the controller cannot feed the plant with a continuous value r.
5. In the act stage the plant operates according to (the ODE associated with) the mode mi picked by
the controller. The act stage lasts for one second (a fact that follows from 2. and 3).
6. The data sent from the sensor to the controller is finitely many Boolean values.
While there are many actual systems that fall out of the realm of this modeling, it does cover fairly
many—among which are fixed interval digital controllers, a class of hybrid systems ubiquitous in industry. Sampled data systems, especially under the above assumptions, come to exhibit pleasant structuralproperties: its behaviors are much like those of programs and we can apply forward and backward reasoning in program logic. Assumptions 2. and 3. are common (see e.g. [17]). For example, Assumption
3. is reasonable considering the speed of digital circuits and typical sensing intervals (∆ ≈ 1ms). Assumptions 4. and 6.—that the controller communicates via finite datatypes—are essential in reducing the
input synthesis problem to a search problem.

2.2

The Language IMPCtrl

We start with defining an imperative programming language IMPCtrl that is used to describe the (digital)
controller of a sampled data system. It is a standard one and is much like IMP in [16], but lacks thewhile construct. It is indeed unrealistic to have while loops in real-time applications like cyber-physicalsystems. Moreover, without while loops we can succinctly express weakest preconditions and strongest
preconditions—the latter are fully exploited in our algorithm for input synthesis.
1 The clock cycle can be an arbitrary number ∆; in this paper we assume ∆ = 1 for simplicity.

26

Input Synthesis for Sampled Data Systems by Program Logic

In IMPCtrl the set Var = Vart ∪ Vars ∪ Vara of variables
is divided into three classes: the think, sense and act variables. The distinction is for the purpose of communicatingwith the other two components (plant and sensor) of a system.
As we will see, a think variable xt ∈ Vart stores a real number (which will be a floating-point number in an actual implementation); a sense variable xs ∈ Vars represents a Boolean
value sent from the sensor; and the (only) act variable xa in Vara = {xa } tells the plant which mode mi
the plant should take in the coming interval.
Definition 2.1 (the language IMPCtrl ). Let Modes = {m1 , . . . , mM } be a fixed finite set of modes; Vartbe a countable set of think variables; Vars be a finite set of sense variables; and Vara = {xa }. The syntax
of IMPCtrl is as follows.
AExp 3BExp 3Cmd 3

a ::= r | xt | a1 aop a2
arithmetic expr.
b ::= true | false | xs | a1 rop a2 | ¬b | b1 ∨ b2 | b1 ∧ b2
Boolean expr.
c ::= skip | xt := a | xa := mi | c1 ; c2 | if b then c1 else c2 commands

Here r ∈ R, mi ∈ Modes, xt ∈ Vart , xs ∈ Vars , aop ∈ {+, −, ×} and rop ∈ {=, <, ≤, >, ≥}.
The semantics of IMPCtrl is as usual, like in [16]. See Def. A.1 for details.

2.3

Assertions for IMPCtrl

We now introduce an assertion language for IMPCtrl . Its formulas are used to express pre- and postconditions in the input synthesis problem, as well as in program logic. The semantics of the first-orderlanguage AssnCtrl is as usual. See Def. A.2.
Definition 2.2 (the assertion language AssnCtrl ). We fix a set Var0 of “logical” variables such that Var ∩Var0 6= 0.
/ The assertion language AssnCtrl is defined as follows.
AExp 3 a ::= r | xt | v0 | a1 aop a2
MExp 3 m ::= mi | xa
Fml 3 Φ ::= true | false | xs | a1 rop a2 | m = m | ¬Φ |
Φ1 ∨ Φ2 | Φ1 ∧ Φ2 | ∀v0 ∈ R.Φ | ∃v0 ∈ R.Φ

arithmetic expressions
mode expressions
formulasHere r ∈ R, mi ∈ Modes, xt ∈ Vart , xs ∈ Vars , and v0 ∈ Var0 . Intuitively, σ ∈ Σ is a valuation that0depends on the state of a sampled data system; and γ ∈ RVar is another valuation of (logical) variables
in AssnCtrl .

2.4

Calculi for Weakest Preconditions and Strongest Postconditions

We introduce program logic for IMPCtrl in the form of a weakest precondition calculus (see e.g. [16])and a strongest postcondition calculus (see e.g. [9]). The calculi will be exploited for the search space
reduction in input synthesis.
Definition 2.3 (weakest precondition wJc, ΦK; strongest postcondition sJc, ΦK ). Given c ∈ Cmd of
IMPCtrl and Φ ∈ Fml of AssnCtrl , we define a formula wJc, ΦK ∈ Fml inductively on c.
wJskip, ΦK ≡ Φ ,wJc1 ; c2 , ΦK ≡ wJc1 , wJc2 , ΦKK ,wJxt := a, ΦK ≡ Φ[a/xt ] ,wJxa := mi , ΦK ≡ Φ[mi /xa ] ,wJif b then c1 else c2 , ΦK ≡ (b ∧ wJc1 , ΦK) ∨ (¬b ∧ wJc2 , ΦK) ;(2)

T. Akazaki, I. Hasuo & K. Suenaga

27

A formula sJc, ΦK ∈ Fml is defined as follows, similarly by induction.
sJskip, ΦK
sJxt := a, ΦK
sJxa := mi , ΦK
sJif b then c1 else c2 , ΦK

≡
≡
≡
≡

Φ ,
sJc1 ; c2 , ΦK ≡ sJc2 , sJc1 , ΦKK ,∃v0 ∈ R.(Φ[v0 /xt ] ∧ xt = a[v0 /xt ]) ,(Φ[m1 /xa ] ∨ · · · ∨ Φ[mM /xa ]) ∧ xa = mi ,sJc1 , b ∧ ΦK ∨ sJc2 , ¬b ∧ ΦK .

(3)

In our implementation, AssnCtrl is restricted to its propositional fragment for tractability. The quantifier in (3) is thus immediately eliminated using the quantifier elimination mechanism in Mathematica.
The third line in (3) is essentially the same as the second; there we can dispense with a quantifier ∃ since
Modes = {m1 , . . . , mM } is a finite set.
0

Proposition 2.4. For any σ ∈ Σ and γ ∈ RVar ,1. (weakest precondition) σ , γ |= wJc, ΦK if and only if JcK(σ ), γ |= Φ;

2. (strongest postcondition) σ , γ |= Φ if and only if JcK(σ ), γ |= sJc, ΦK.

2.5

Modeling Sampled Data Systems, Formally

We present the formal definition of our modeling of sampled data systems, under the assumptions in §2.1.
Definition 2.5 (sampled data system). Let n be a natural number, and I ⊆ Rn be a fixed set called the
input domain. An n-dimensional sampled data system is a triple S = (c, p, s) where:• c ∈ Cmd is a command of IMPCtrl (§2.2), called a controller;• p = ẋ = pmi (t, x) mi ∈Modes is a family of (explicit, n-dimensional) ODEs indexed by Modes ={m1 , . . . , mM }, called a plant; and• s : Rn × I → BVars is a function, called a sensor.
A state of a sampled data system is a pair (σ , x) of σ ∈ Σ and x ∈ Rn . In a state (σ , x), the component σ
is called a controller state(C-state), and x a plant state (P-state).
The dimension n refers to that of the (continuous) plant, meaning that x and ẋ in the plant p = ( ẋ =pmi (t, x) )mi ∈Modes are vectors in Rn .
Example 2.6 (count and brake). In Fig. 2 is a simplification of Example 1.1; this will be our running
example. The value v is intended to be the velocity of a car.
xs (Boolean)i ∈ [−0.2, 0.2]

Sensor/ xs : v + i ≥ 1?
O
v

if xs
then cnt := cnt + 1
else cnt := 0;/
if cnt < 2then xa := Aclelse xa := Brk

Controllerxa

Acl : v̇ = (2 − v) log 2 o
Brk : v̇ = −0.5
Plant

Figure 2: A sampled data system (running example)
The example follows a pattern of fixed interval controllers commonly used in industry. Namely, acounter cnt is used to tell if extremity (v + i ≥ 1) has continued for a certain critical number of intervals(2 here). If cnt reaches the critical number a countermeasure is taken: the plant is set to the braking

28

Input Synthesis for Sampled Data Systems by Program Logic

mode (Brk) and the velocity v decreases. Otherwise the plant operates in the acceleration mode (Acl),
which is a first-order lag system where the velocity v approaches towards 2.
The system takes input i—whose domain is assumed to be [−0.2, 0.2]—that models disturbance fromoutside. For example, the road can be slippery, which can make the actual velocity v different from thevalue that is used by the controller.

2.6

Semantics of Sampled Data Systems

We formally define the semantics of a sampled data system. Our current concern is not so much on
the solution of ODEs as on the interaction between a controller and a plant. Therefore we adopt thefollowing black-box view of a plant.
Definition 2.7 (execPlant(p, x)). In what follows we assume that all the ODEs used for a plant haveunique solutions. That is, for any n-dimensional ODE ẋ = p(t, x) and an initial value x0 ∈ Rn , weassume that there exists a unique function F : [0, 1] → Rn such that: F(0) = x0 ; and for any t ∈ [0, 1],
Ḟ(t) = p(t, F(t)).
By execPlant(p, x0 ) we denote the state of the plant ẋ = p(t, x) at time t = 1, assuming that the initialstate (at time t = 0) is x0 . That is, execPlant(p, x0 ) = F(1) where F is the function in the above.
In our implementation we actually use the result of numerical calculations (by MATLAB) as thevalue execPlant(p, x), ignoring numerical errors.
Definition 2.8 (semantics of a sampled data systems). Let S = (c, p, s) be a sampled data system. The
one-step transition is a ternary relation → among two states (σ , x), (σ 0 , x0 ) and input i ∈ I; this is denotediby (σ , x) →− (σ 0 , x0 ). It is defined as follows.
i
We have (σ , x) →− (σ 0 , x0 ) if (σ 0 , x0 ) = (actS ◦ thinkS ◦ senseS )(σ , x, i), where the three functions
are defined by:senseS : Σ × X × I −→ Σ × X ,(σ , x, i) 7−→ σ [xs 7→s(x, i)(xs )], x ;thinkS : Σ × X −→ Σ × X ,(σ , x) 7−→ JcK(σ ), x ;(4)actS : Σ × X −→ Σ × X ,(σ , x) 7−→ σ , execPlant(pσ (xa ) , x) .
Here JcK is as in Def. A.1. It is clear that, given a state (σ , x) and i ∈ I, the post-state (σ 0 , x0 ) such
i

i

i

iT −1

0
1
that (σ , x) →− (σ 0 , x0 ) is uniquely determined. A succession (σ0 , x0 ) −→(σ1 , x1 ) −→· · · −−→ (σT , xT ) of
one-step transition is called a run of the system S .

A specification of a state of a sampled data system is given by a pair of an assertion formula (on thecontroller) and a subset of Rn (on the plant).
Definition 2.9 (CP-condition). Let S = (c, p, s) be an n-dimensional sampled data system. A controllerplant condition (CP-condition) for S is a pair (Φ, X) of an assertion Φ ∈ Fml called the controller
condition and a condition X ⊆ Rn called the plant condition. The projection to each component isdenoted by πC and πP respectively.
Given a state (σ , x) ∈ Σ × Rn of S and a CP-condition (Φ, X), we write (σ , x) |= (Φ, X) if σ |= Φand x ∈ X. (Φ, X) is satisfiable if there is a state that satisfies it.

2.7

The Input Synthesis Problem for Sampled Data Systems

Definition 2.10 (input synthesis problem). The input synthesis problem is:

T. Akazaki, I. Hasuo & K. Suenaga

29• S = (c, p, s), an n-dimensional sampled data system;

given:• (Φinit , Xinit ) and (Φfinal , Xfinal ), a pre- and a post-CP-condition; and• T ∈ N, the number of steps,• an initial state (σ0 , x0 ) ∈ Σ × Rn such that (σ0 , x) |= (Φinit , Xinit ); andreturn:i0• an input sequence i0 , . . . , iT −1 ∈ I such that, for the corresponding run (σ0 , x0 ) −
→

i

iT −1

1
→
· · · −−→ (σT , xT ) of S , we have (σT , xT ) |= (Φfinal , Xfinal ).
(σ1 , x1 ) −Example 2.11. Let S be the sampled data system in Example 2.6. Consider

a pre-CP-condition (cnt = 0, [0, 1]) and a post-CP-condition (true, [1.5, 2])
and T = 4 as the number of steps. In the input synthesis problem, we seek for an initial state (σ0 , x0 )and an input sequence i0 , i1 , i2 , i3 ∈ [−0.2, 0.2] such that
i

i

i

3
0
1
→
··· −
→
(σ4 , x4 ) and (σ4 , x4 ) |= (true, [1.5, 2]) .
(σ0 , x0 ) |= (cnt = 0, [0, 1]) , (σ0 , x0 ) −→(σ1 , x1 ) −3

An Algorithm for Input Synthesis for Sampled Data Systems

In this section we present our algorithm. We identify the core of the input synthesis problem to be thediscovery of suitable input and output of the controller at each step. More specifically, we seek for a
successful path
−−−−→
(0)
(T −2)(T −1)(5), m(T −2) ), . . . , (σs , m(0) ), m(T −1) ), (σs(σs , m) := (σs(k)

where σs : Vars → B is a valuation of sense variables—which shall be henceforth called sensor out(k)put—and m(k) ∈ Modes is a mode.2 Together with an initial state (σ0 , x0 ), the sensor output σs de(k)termines the behavior of the controller, and the mode m determines that of the plant, at each step k.
Therefore a path like in (5) determines the behavior of the whole sampled data system from step 0 throughstep T ; a “successful” path is then one that steers the given precondition to the given postcondition.
Towards the discovery of a successful path, our approach is to exploit the program logic in §2.4—i.e.
to make most of the structure of the controller as a program. In our modeling of sampled data systems(§2) we have made assumptions so that the program-logic approach is possible.
Concretely, our algorithm consists of the following three phases.
1. (Forward approximation) We overapproximate the set of CP-states that the system can reach,starting from the pre-CP-condition (Φinit , Xinit ) and going forward step by step. This first phase isseen as a preparation for the second (main) phase.
2. (Backward search) A successful path (5) will be a path in a so-called backward search tree. Its
branching degree is 2|Vars | × |Modes|; its nodes are labeled with CP-conditions; and its root islabeled with the post-CP-condition (Φfinal , Xfinal ). We search for a successful path in the tree, in a
depth-first manner.
3. (Synthesis of actual input) We choose an initial state (σ , x) and go on to synthesize an input−−−−→
sequence i0 , . . . , iT −1 , using the successful path (σs , m) discovered in the previous phase. This canbe done in a straightforward linear manner.
The second phase (backward search) is where an actual (depth-first) search is done. Program logic isused there to prune branches and reduce the search space.
2 Note that time is reversed in (5). This is purely for the purpose of presentation.

30

3.1

Input Synthesis for Sampled Data Systems by Program Logic

Forward Approximation

In this phase of the algorithm, we overapproximate
the behavior of the given sampled data system and
obtain a sequence k-FA(Φinit , Xinit ) 0≤k≤T of CP-conditions. These are obtained iteratively as follows.
Notation 3.1 (s−1 ). Let S = (c, p, s) be an n-dimensional sampled data system; I be its input domain;and σs ∈ BVars be sensor output. We abuse notation and denote by s−1 (σs ) the set of plant states that canbe “steered” to σs . Precisely, s−1 (σs ) := {x ∈ Rn | ∃i ∈ I. s(x, i) = σs } .
For example, let σs such that σs (xs ) = tt in the setting of Example 2.6. We have s−1 (σs ) = {x ∈ X |∃i ∈ [−0.2, 0.2]. x + i ≥ 1} = [0.8, ∞).
Definition 3.2 (1-FA, k-FA). Let S = (c, p, s) be a sampled data system. Let us first define the functions
prepre
1-FApresense , 1-FAthink and 1-FAact as follows. Their types should be obvious.
1-FApresense (σs )(Φ, X)
1-FAprethink (Φ, X)
1-FApreact (m)(Φ, X)

:=
:=
:=


−1 (σ )
sJxs := σs (x
),
ΦK,
X
∩
s
s
s

sJc, ΦK, X ,Φ ∧ xa = m, execPlant(pm , X) .

(6)

Here sJc, ΦK in the second line is the strongest postcondition (Def. 2.3); execPlant(pm , X) in the thirdline is the direct image of X ⊆ Rn by the function in Def. 2.7; and sJxs := σs (xs ), ΦK in the first line isdefined as follows, similarly to Def. 2.3.
(
(Φ[true/xs ] ∨ Φ[false/xs ]) ∧ xs
sJxs := σs (xs ), ΦK :≡(Φ[true/xs ] ∨ Φ[false/xs ]) ∧ ¬xs

if σs (xs ) = true
if σs (xs ) = false

These three functions are composed to yield:

pre
pre
;
1-FApre (σs , m)(Φ, X) := 1-FApre
act (m) 1-FAthink 1-FAsense (σs )(Φ, X)
this is understood as the strongest postcondition after the one-step execution of S , assuming that thesensor output σs and the mode m have been chosen.
Finally, the one-step forward approximation function is defined as the following disjunction/union
over different σs and m:
1-FA(Φ, X) :=W

pre(σs ,m)∈M πC 1-FAS(σs , m)(Φ, X) , (σs ,m)∈M πP 1-FApre (σs , m)(Φ, X)


,

pre
where M := { (σ , m) ∈ BVars × Modes | 1-FA (σs , m)(Φ, X) is satisfiable.}(7)
The projections πC and πP , as well as satisfiability of CP-conditions, are from Def. 2.9.

We write k-FA(Φ, X) for (1-FA)k (Φ, X). The sequence k-FA(Φinit , Xinit ) 0≤k≤T of CP-conditions iscalled the forward approximation sequence for S .
As an example we present forward approximation for Example 2.11. The first one-step approxima-

T. Akazaki, I. Hasuo & K. Suenaga

31tion (from k = 0 to 1) is shown below, stage by stage.
sense

+3

k=0

think

+3

act

+3

xs 7→ tt

cnt = 0 ∧ xs
[0.8, 1]6cnt = 1

/ ∧xa = Acl ∧ xs,

[0.8, 1]Brk

cnt = 0[0, 1]
xs 7→ ff&
cnt = 0 ∧ ¬xs[0, 1]

Acl
cnt = 0/ ∧xa = Acl ∧ ¬xs[0, 1]
Brk

3+3 k = 1

cnt = 1∧xa = Acl ∧ xs
[1.4, 1.5]

3

Acl

unify

cnt = 0∧xa = Acl ∧ ¬xs[1, 1.5]

,

&

false
[0.3, 0.5]2(cnt = 0 ∨ cnt = 1)
∧xa = Acl
[1, 1.5]

(8)

false
[−0.5, 0.5]

Observe that we have four CP-conditions in the fourth column from the left. Each of them corresponds
to a choice of (σs , m). Two among the four CP-conditions are unsatisfiable and hence discarded (i.e. they
are not in M ); the remaining two are unified and yield 1-FA(cnt = 0, [0, 1]) in the rightmost column. 3
By continuing further we obtain the forward approximation sequence shown on the below in (9),presented pictorially.
For the completeness of our algorithm we needto prove that our forward approximation is indeed
an over-approximation.
Proposition 3.3. Let i0 , . . . , ik−1 ∈ I be any input
i

ik−1

0
sequence; (σ , x) −→· · · −−→ (σ 0 , x0 ) be a run of S ;and (σ , x) |= (Φ, X). Then (σ 0 , x0 ) |= k-FA(Φ, X).
2

3.2

Backward Search

In this phase of the algorithm we search for a suc−−−−→
cessful path (σs , m) of sensor output and modes—
i.e. one that steers an initial state to a desired post(9)condition. The search is conducted in a backward depth-first manner in a tree called the backward searchtree.
For the input synthesis problem, it is not necessary to construct the whole backward search tree: finding a leaf whose CP-condition is compatible with the precondition suffices. We will use program logic(§2.4)—and the forward approximation sequence obtained in the previous phase—in pruning branches
and reducing the search space.
Definition 3.4 (backward search tree). Given an input synthesis problem, its backward search tree is atree with branching degree 2|Vars | × |Modes| and with height T + 1. The nodes of the tree are definedinductively as follows.
• The root of the tree is labeled with the postcondition (Φfinal , Xfinal ).
3 Our approximation can be finer: in (8), in the unification stage, the correlation between a C-condition and a P-condition

is forgotten by separately taking the disjunction of C-conditions and the union of P-conditions (see (7)). Finer approximation,
however, makes the approximants grow much bigger and slows down the backward search phase of the algorithm.

32

Input Synthesis for Sampled Data Systems by Program Logic−−−−→(T −1)(k+1)• Let (Φ, X) be the label at the position (σs , m) = (σs, m(T −1) ), . . . , (σs, m(k+1) ) . Its child−−−−→ 0 0
at the position (σs , m)(σs , m ) is labeled by(Φ0 , X 0 ) :=πC k-FA(Φinit , Xinit ) ∧ πC (1-BSpre (σs , m)(Φ, X)),(10)

πP k-FA(Φinit , Xinit ) ∩ πP (1-BSpre (σs , m)(Φ, X)) ,where the function 1-BSpre is defined as follows.
1-BSpre (σs , m)(Φ, X):=

1-BSpreact (m)(Φ, X)
1-BSprethink (Φ, X)
1-BSpre(σsense s )(Φ, X)

:=
:=
:=



pre
pre
1-BS
(m)(Φ,
X)
where
1-BSpre
(σ
)
1-BS
act
sense sthinkΦ ∧ xa = m, execPlant(rev(pm ), X) ,(wJc, ΦK, X) , and(Φ[σs (xs )/xs ], X ∩ s−1 (σs )) .

(11)

In the second line, execPlant(rev(pm ), x1 ) means running the original ODE ẋ = pm (t, x) with time
reversed (i.e. from t = 1 to t = 0) and with the “initial” value x1 (at time t = 1). Concretely, rev(pm )is given by: rev(pm )(t, x) = −pm (1 − t, x).
−−−−→
−−−−→By BS (σs , m) we denote the label in the tree, at the position designated by the path (σs , m).
−−−−→BS (σs , m) is therefore a CP-condition.
−−−−→
Definition 3.5 (successful path). Let (σs , m) be a path in the backward search tree. It is successful if: 1)−−−−→
it is of length T ; and 2) the label BS (σs , m) at the leaf is satisfiable.
The following establishes that that finding a successful path in the backward search tree is equivalent
to solving the input synthesis problem.
−−−−→
Proposition 3.6 (soundness & completeness). Let (σs , m) be a successful path in the backward search−−−−→
tree. Assume also that σ0 ∈ Σ and x0 ∈ Rn satisfy (σ0 , x0 ) |= BS (σs , m) . Then there exists an input
sequence i0 , . . . , iT −1 ∈ T such that an initial state (σ0 , x0 ) together with i0 , . . . , iT −1 is an answer to the
input synthesis problem.
Conversely, assume there is an answer to an input synthesis problem, given by (σ0 , x0 ) and i0 , . . . , iT −1 .
−−−−→Then there is a successful path (σs , m).
2
In searching for a successful path in a backward search tree, once we hit an unsatisfiable label, clearly
all its offspring are unsatisfiable. We therefore prune such a branch. The use of k-FA in (10) strengthens
the labels and makes more branches pruned.
Lemma 3.7 (pruning is correct). In the backward search tree, assume that the label at the position−−−−→(σs , m) is unsatisfiable. Then its child has an unsatisfiable label too.
2
An example is again using Example 2.11. Fig. 3 describes details of one-step generation (from theroot k = 4 to k = 3) of the backward search tree. The rightmost is the root; the four leftmost nodes are
the direct children of the root; and the intermediate layers are not present in the backward search tree but
are shown for illustration. Each of the four children corresponds to each possible choice of (σs , m). The
bottom two children are unsatisfiable—the intuition is that the plant’s mode at time k = 3 cannot be Brk
for the postcondition to hold. The search for a successful path will therefore be continued from one of
the two top children.
Presented in Fig. 4 is a more bird’s-eye view of the backward search tree: it shows one possible traceof the depth-first search. It has found a successful path−−−−→
(σs , m) = (xs 7→ tt, Acl), (xs 7→ ff, Acl), (xs 7→ tt, Brk), (xs 7→ tt, Acl) .
(12)
In the search shown in Fig. 4, pruning has occurred at the nodes (N1)–(N3).

T. Akazaki, I. Hasuo & K. Suenaga

33

combine with fwd approx.
ks
k = 3 ksocnt = 0[1, 1.5] ∪ [1.75, 1.875]
cnt = 0 ∨ cnt = 1∨cnt = 2 ∨ cnt = 3[1, 1.2]
cnt = 1 ∨ cnt = 2∨cnt = 3
0/

s

true

o

cnt ≥ 1k[2, 2.5]
false[2, 2.5]o[1, 2][1, 1.2]

o

think

ks

cnt < 1 xs 7→ tt
l(xs ∧ cnt < 1) ∨ ¬xs[1, 2]

o

false
0/

sense

act

ks

k=4

xa = Acld[1, 2]

xs 7→ ff

Acl

true

xs 7→ ttBrk[1.5, 2]xs ∧ cnt ≥ 1r

xa = Brkoz[2, 2.5][2, 2.5]
xs 7→ ff

Figure 3: Generation of the backward search tree, in detail
k=0

k=1

k=2

k=3

(N3)
(N1)

cnt = 0[0.8, 1](N2)

i
xs 7→ tt
Acl

xs 7→ tt

cnt = 0
0/

k Acl

true
0/

o xs 7→ ff

cnt = 1
[1, 1.5]lcnt = 0 ∨ cnt = 1 ∨ cnt = 2 o[0.5, 1]
xs 7→ ff
xs 7→ tt
Acl
Brk

Acl

s

false
[0.8, 1] ∪ [1.5, 1.75]

k=4

xs 7→ ttAcl
cnt = 0[1, 1.5]∪ [1.75, 1.875]hxs 7→ ttAcl

true
[1.5, 2]

Figure 4: A bird’s-eye view of the backward search tree

3.3

Synthesis of Actual Input−−−−→
The second phase gives us a successful path (σs , m); as discussed at the beginning of §3, this determines
the behavior of the whole sampled data system. We now synthesize an actual answer to the input synthe−−−−→
sis problem from the path (σs , m). Theoretically it is possible (Prop. 3.6); it is moreover computationallycheap, using a CAS like Mathematica.
We describe the procedure by example. For Example 2.11, the second phase gives a successful path−−−−→
in (12), from which we obtain a refinement of the pre-CP-condition BS (σs , m) = (cnt = 0, [0.8, 1])(the leftmost node in Fig. 4).
−−−−→• (Choosing an initial state) By Prop. 3.6 any (σ0 , v0 ) such that (σ0 , v0 ) |= BS (σs , m) admits adesired input sequence. Let us say σ0 (cnt) = 0 and v0 := 0.9.
• (Running the plant) It is crucial that the behavior of the plant is completely determined now, given−−−−→
the initial P-state v0 and the sequence of modes hm(0) , . . . , m(T −1) i extracted from the path (σs , m).
In the current example the plant dynamics is as follows: 0.9 −−→ 1.45 −−→ 0.95 −−→ 1.475 −−→
Acl
Brk
Acl
Acl
1.7375.
• (Synthesis of input) For each moment k, we now know the plant state v(k) and the sensor output
−−−−→
(k)
σs ∈ BVars ; the latter is extracted from the path (σs , m). We choose input ik so that it, combined(k)with v(k) , gives the sensor output as specified by σs .
For example let us pick i2 . Now σ (2) (xs ) = (v + i ≥ 1?) = ff and v(2) = 0.95; we choose i2 ∈ I =[−0.2, 0.2] so that v(2) +i2 = 0.95+i1 < 1; say i2 = 0. In implementation we let the FindInstancefunction of Mathematica do this job.

34

Input Synthesis for Sampled Data Systems by Program Logic

Overall, we obtain the following run from the pre-CP-condition to the post-CP-condition. This gives an
0.1
0.0
0.0
0.0
answer (cnt 7→ 0, v = 0.9) −→ (1, 1.45) −→ (2, 0.95) −→ (0, 1.475) −→ (1, 1.7375) to the input synthesis
problem in Example 2.11.

4Implementation, Optimization and Experiments

Our prototype implementation has a front-end written in OCaml which in particular implements inferences in program logic (Def. 2.3). Mathematica is used for simplifying arithmetic formulas and inequalities, as well as for picking a value under a certain assumption. We also use MATLAB for numericallysolving ODEs.
Our implementation is currently restricted to one-dimensional plants (n = 1). From time to time wehave to calculate the evolution of an interval according an ODE (like execPlant(pm , X) in (6) for a setX); such calculation is done by the method of [6].
Optimization Techniques We further employ the following techniques for speedup. We note that thenone of these affect correctness (Prop. 3.6) of our algorithm.
• (Truncation of forward approximation) In the forward approximation phase, a problem is thatan approximant k-FA(Φinit , Xinit ) can grow exponentially as k grows—as hinted already in (9).
Such explosion of approximants slows down not only the forward approximation phase, but also
the backward search phase. Moreover such a big approximant tends not to contribute a lot topruning branches.
To avert this we truncate forward approximation under certain circumstances. Specifically westop calculating C-conditions when the approximated C-condition has become compatible withany choice of modes—a sign of the C-condition no longer contributing to pruning. Currently suchtruncation is implemented only for C-conditions; but it should also be possible for P-conditions,e.g. by merging intervals in (9).
• (Prioritization in search) In the backward (depth-first) search phase, we can have multiple children from which to pick. Besides randomized picks, we have the following prioritization strategies. In the by-volume prioritization, we estimate the volume of the P-condition (i.e. a region in
Rn ) of each child, and pick one with the biggest. In the by-robustness prioritization, in contrast,
we pick the child whose P-condition is the closest to the “center” of the forward-approximatedP-condition. In other words, the picked child is the one with a P-condition that intersects with theforward-approximated P-condition in the most robust manner. This robustness-driven optimization
is much like in S-Taliro [3].
Experiments We used Mathematica 9.0.1 and MATLAB 8.1.0 (for Linux x86, 64-bit), on ThinkPad
T530 with Intel Core i7-3520M 2.90GHz CPU with 3.7GB memory.
The first table below shows the result of our prototype implementation applied to the problem in
Example 2.11, with a varying number T of steps. All the times are in seconds. The rows correspondto different prioritization strategies, and whether truncation of forward approximation is enabled. For
random prioritization the experiment was repeated 50 times and the average is shown, together with thestandard deviation. From the results we can see that forward approximation truncation is very effective
as the problem becomes larger, on the one hand. On the other hand, no clear comparative advantage of
any of the three prioritization strategies is observed.

T. Akazaki, I. Hasuo & K. Suenaga

35

The second table below presents the breakdown of two cases (both T = 100) from the first table, into
the three phases of the algorithm, together with the number of backtracks in a search. While truncation
causes more backtracks (this is because less information is passed to the backward search phase), we seethat the speed of both of the first two phases are greatly improved thanks to simpler approximants.
We also applied our implementation to the original problem in Example 1.1. It successfully solved
the problem in 638.968 seconds.
Overall, our experiments so far are limited to examples of a specific structure: namely, a counter inthe controller, incremented or reset to 0 every second, causes the change of modes of the plant. This
structure however is a commonly used one in industry (see Example 2.6); and its discrete nature (thecounter takes an integer value that can be fairly large) becomes a challenge in many approaches toverification, testing or input synthesis. The experimental results seem to suggest that our program logic
based approach is promising in coping with this kind of challenges.
prioritization
randomby volumeby robustness
randomby volumeby robustness

truncation

prioritization
by volumeby volumetruncation

on
on
on

on

T = 10
3.228
3.633
3.072
3.409
3.689
3.552

T = 209.849
10.19711.082
11.3149.289
20.702

fwd. approx.
36.622
15.118

T = 3018.46414.33222.23120.06812.32341.443

bwd. search
76.56821.565

T = 100
108.437 ± 37.574
115.31168.46454.132 ± 31.953
38.42538.803

T = 1000
No answer
No answer
No answer
377.361 ± 80.392
445.784245.661

synthesis
2.121
1.743

num. of backtracks
140
176

total
115.31138.425

References[1] Rajeev Alur, Aditya Kanade, S. Ramesh & K. C. Shashidhar (2008): Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In Luca de Alfaro & Jens Palsberg, editors: EMSOFT, ACM,
pp. 89–98. Available at http://doi.acm.org/10.1145/1450058.1450071.
[2] Rajeev Alur, Robert P. Kurshan & Mahesh Viswanathan (1998): Membership Questions for Timed andHybrid Automata. In: RTSS, IEEE Computer Society, pp. 254–263. Available at http://doi.
ieeecomputersociety.org/10.1109/REAL.1998.739751.
[3] Yashwanth Annpureddy, Che Liu, Georgios E. Fainekos & Sriram Sankaranarayanan (2011): S-TaLiRo: A
Tool for Temporal Logic Falsification for Hybrid Systems. In Parosh Aziz Abdulla & K. Rustan M. Leino,
editors: TACAS, Lecture Notes in Computer Science 6605, Springer, pp. 254–257. Available at http://dx.doi.org/10.1007/978-3-642-19835-9_21.
[4] Bahareh Badban, Martin Fränzle, Jan Peleska & Tino Teige (2006): Test automation for hybrid systems. In
Johannes Mayer, Neelam Gupta & Yves Ledru, editors: SOQUA, ACM, pp. 14–21. Available at http://doi.acm.org/10.1145/1188895.1188902.
[5] Thao Dang & Tarik Nahhal (2009): Coverage-guided test generation for continuous and hybrid systems.
Formal Methods in System Design 34(2), pp. 183–213. Available at http://dx.doi.org/10.1007/
s10703-009-0066-0.
[6] Andreas Eggers, Nacim Ramdani, Nedialko Nedialkov & Martin Fränzle (2011): Improving SAT Modulo
ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods. In Gilles Barthe, Alberto
Pardo & Gerardo Schneider, editors: SEFM, Lect. Notes in Comp. Sci. 7041, Springer, pp. 172–187. Available at http://dx.doi.org/10.1007/978-3-642-24690-6_13.
[7] J.M. Esposito (2004): Randomized test case generation for hybrid systems: metric selection. In:
System Theory, 2004. Proceedings of the Thirty-Sixth Southeastern Symposium on, pp. 236–240,
doi:10.1109/SSST.2004.1295655.

36

Input Synthesis for Sampled Data Systems by Program Logic[8] Sicun Gao, Soonho Kong & Edmund M. Clarke (2013): dReal: An SMT Solver for Nonlinear Theories overthe Reals. In Maria Paola Bonacina, editor: CADE, Lecture Notes in Computer Science 7898, Springer, pp.
208–214. Available at http://dx.doi.org/10.1007/978-3-642-38574-2_14.
[9] Mike Gordon & Hlne Collavizza (2010): Forward with Hoare. In A.W. Roscoe, Cliff B. Jones & Kenneth R.
Wood, editors: Reflections on the Work of C.A.R. Hoare, Springer London, pp. 101–121. Available at
http://dx.doi.org/10.1007/978-1-84882-912-1_5.
[10] A. Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee & George J. Pappas (2007): Robust
Test Generation and Coverage for Hybrid Systems. In Alberto Bemporad, Antonio Bicchi & Giorgio C.
Buttazzo, editors: HSCC, Lecture Notes in Computer Science 4416, Springer, pp. 329–342. Available at
http://dx.doi.org/10.1007/978-3-540-71493-4_27.
[11] Naoki Kobayashi & C.-H. Luke Ong (2009): A Type System Equivalent to the Modal Mu-Calculus Model
Checking of Higher-Order Recursion Schemes. In: LICS, IEEE Computer Society, pp. 179–188. Available
at http://doi.ieeecomputersociety.org/10.1109/LICS.2009.29.
[12] Mayur Naik & Jens Palsberg (2008): A type system equivalent to a model checker. ACM Trans. Program.
Lang. Syst. 30(5). Available at http://doi.acm.org/10.1145/1387673.1387678.
[13] André Platzer (2012): The Complete Proof Theory of Hybrid Systems. In: LICS, IEEE, pp. 541–550. Available at http://dx.doi.org/10.1109/LICS.2012.64.
[14] Kohei Suenaga & Ichiro Hasuo (2011): Programming with Infinitesimals: A While-Language for Hybrid
System Modeling. In Luca Aceto, Monika Henzinger & Jiri Sgall, editors: ICALP (2), Lecture Notes
in Computer Science 6756, Springer, pp. 392–403. Available at http://dx.doi.org/10.1007/
978-3-642-22012-8_31.
[15] Kohei Suenaga, Hiroyoshi Sekine & Ichiro Hasuo (2013): Hyperstream processing systems: nonstandard
modeling of continuous-time signals. In Roberto Giacobazzi & Radhia Cousot, editors: POPL, ACM, pp.
417–430. Available at http://doi.acm.org/10.1145/2429069.2429120.
[16] Glynn Winskel (1993): The Formal Semantics of Programming Languages. MIT Press.
[17] Aditya Zutshi, Sriram Sankaranarayanan & Ashish Tiwari (2012): Timed Relational Abstractions for
Sampled Data Control Systems. In P. Madhusudan & Sanjit A. Seshia, editors: CAV, Lecture Notes
in Computer Science 7358, Springer, pp. 343–361. Available at http://dx.doi.org/10.1007/
978-3-642-31424-7_27.

T. Akazaki, I. Hasuo & K. Suenaga

A

37

Auxiliary Definitions and Lemmas

Definition A.1 (semantics J K of IMPCtrl ). Let Σ be the set of valuations, that is,Σ = σ : Var → R ∪ B ∪ Modes σ (Vart ) ⊆ R, σ (Vars ) ⊆ B, σ (xa ) ∈ Modes

.

(13)

For each expression e of IMPCtrl , their semantics JeK is defined in the following standard way. Fora ∈ AExp, JaK : Σ → R is defined by
JrK(σ ) = r ,Jxt K(σ ) = σ (xt ) ,Ja1 aop a2 K(σ ) = Ja1 K(σ ) aop Ja2 K(σ ) .

For b ∈ BExp, JbK : Σ → {tt, ff} is defined by
Jb1 ∨ b2 K(σ ) = Jb1 K(σ ) ∨ Jb2 K(σ ) and similarly for ¬, ∧, true and false;
Jxs K(σ ) = σ (xs ) ; andJa1 rop a2 K(σ ) = Ja1 K(σ ) rop Ja2 K(σ ) .
For c ∈ Cmd, JcK : Σ → Σ is defined by
Jxt := aK(σ ) = σ [xt 7→ JaK(σ )] , Jxa :=(mi K(σ ) = σ [xa 7→ mi ] ,
Jc1 K(σ ) if JbK(σ ) = tt
Jc1 ; c2 K(σ ) = Jc2 K Jc1 K(σ ) , Jif b then c1 else c2 K(σ ) =Jc2 K(σ ) if JbK(σ ) = ff.
JskipK(σ ) = σ ,Here f [x0 7→ y0 ] denotes function update: the function f [x0 7→ y0 ] carries x0 to y0 and acts as f on theother input.
Definition A.2 (semantics of AssnCtrl ). We define the semantics of a ∈ AExp of AssnCtrl as a function0
JaK : Σ × RVar → R.
JrK(σ , γ) = r ,Jv0 K(σ , γ) = γ(v0 ) ,Jxt K(σ , γ) = σ (xt ) ,Ja1 aop a2 K(σ ) = Ja1 K(σ , γ) aop Ja2 K(σ , γ)0For m ∈ MExp, its semantics is a function JmK : Σ × RVar → Modes defined by Jmi K(σ , γ) = mi and
Jxa K(σ , γ) = σ (xa ). Finally for formulas, the semantics of Φ ∈ Fml is given by the relation |= between0Σ × RVar and Fml defined as follows. σ , γ |= true, σ , γ 2 false, anddef.

σ , γ |= xs ⇐⇒def.
σ , γ |= a rop a0 ⇐⇒def.

σ , γ |= m = m0 ⇐⇒def.

σ , γ |= Φ1 ∨ Φ2 ⇐⇒def.
σ , γ |= ∀v0 ∈ R.Φ ⇐⇒σ (xs ) = tt ,JaK(σ , γ) rop Ja0 K(σ , γ) ,JmK(σ , γ) = Jm0 K(σ , γ) ,σ , γ |= Φ1 or σ , γ |= Φ2(similarly for ¬ and ∧),σ , γ[v0 7→ r] |= Φ for any r ∈ R(similarly for ∃).

0

We write σ |= Φ if σ , γ |= Φ for every γ ∈ RVar .
The next observation follows immediately from Def. 2.5 and 2.9.
Lemma A.3. (Φ, X) is unsatisfiable if and only if Φ is an unsatisfiable formula (i.e. logically equivalent
to false) or X = 0.
/
2

38

Input Synthesis for Sampled Data Systems by Program Logic

B

Omitted Proofs

B.1

Proof of Prop. 3.3

Lemma B.1. Let i ∈ I, σ ∈ Σ and x ∈ Rn . Assume (σ , x) |= (Φ, X). Then:sense(σ , x, i)act(σ , x)|= 1-FApre
sense (s(i, x))(Φ, X) ,|= 1-FApre
act (σ (xa ))(Φ, X) .

think(σ , x)|= 1-FApre
think (Φ, X) ,(14)

Proof. For sense, it is easily shown that σ [xs 7→ s(x, i)] |= sJxs := σs (xs ), ΦK by induction on Φ. Moreover x ∈ X ∩ s−1 (s(x, i)) by Notation 3.1. Therefore we have sense(σ , x, i) |= 1-FApre
sense (s(i, x))(Φ, X).
For think, the claim is obvious from Prop. 2.4.
For act, we trivially have σ |= xa = σ (xa ). Therefore(σ , execPlant(pσ (xa ) , x)) |= (Φ ∧ xa = σ (xa ), execPlant(pσ (xa ) , X))2follows immediately from the assumption.

Proof. (Of Prop. 3.3) It is sufficient to show for k = 1; the general case follows by induction. Let i ∈ I,i(σ , x) →− (σ 0 , x0 ) be a run of S , and (σ , x) |= (Φ, X). We need to show
(σ 0 , x0 ) |= 1-FA(Φ, X) .
That is obvious because we obtain the following from Lemma. B.1.
(σ 0 , x0 ) |= 1-FApre (s(i, x), σ 0 (xa ))(Φ, X) .

B.2

2

Proof of Prop. 3.6

Lemma B.2. The following three properties hold.
(σ , x) |= 1-BSpre
sense (σs )(Φ, X)(σ , x) |= 1-BSpre
think (Φ, X)
pre(σ , x) |= 1-BSact (m)(Φ, X)=⇒ sense(σ , x, i) |= (Φ, X) for some i ∈ I=⇒ think(σ , x) |= (Φ, X)=⇒ act(σ , x) |= (Φ, X)

It follows that: if (σ , x) |= 1-BSpre (σs , m)(Φ, X), then there exist input i ∈ I and a CP-state (σ 0 , x0 ) foriwhich we have (σ , x) →− (σ 0 , x0 ) and (σ 0 , x0 ) |= (Φ, X).
Proof. For sense, it follows from the assumption that σ |= Φ[σs (xs )/xs ] and x ∈ X ∩ s−1 (σs ). Then
we have (σ [xs 7→ σs (xs )], x) |= (Φ, X). Moreover, since x ∈ s−1 (σs ) there exists some i ∈ I such thats(x, i) = σs . For this choice of i we have sense(σ , x, i) = (σ [xs 7→ σs (xs )], x).
For think, we have σ |= wJc, ΦK and x ∈ X from the assumption. Therefore JcK(σ ), x |= (Φ, X)
from Prop. 2.4.
For act, we have σ |= Φ ∧ xa = m and x ∈ execPlant(rev(pm ), X) from the assumption. Then we
have σ (xa ) = m, hence x ∈ execPlant(rev(pσ (xa ) ), X), that is, x is reached from the region X by running
pσ (xa ) with time reversed. From this the claim (σ , execPlant(pσ (xa ) , x)) |= (Φ, X) follows.
2

Proof. (Of Prop. 3.6) For soundness, first we observe that (σ0 , x0 ) |= (Φinit , Xinit ). This is because−−−−→BS (σs , m) implies (Φinit , Xinit ) = 0-FA(Φinit , Xinit ) by Def. 3.4; see in particular (10).
Starting from (σ0 , x0 ), we can repeatedly apply Lem. B.2 to obtain input i0 , . . . , iT −1 and CP-states
i

iT −1

(T −1)

0(σ1 , x1 ), . . . , (σT , xT ) such that: (σ0 , x0 ) −→· · · −−→ (σT , xT ); and (σk , xk ) |= BS (σs(k), m(T −1) ), . . . , (σs , m(k) )T. Akazaki, I. Hasuo & K. Suenaga

39

for each k ∈ [0, T ]. Then in particular (σT , xT ) |= BS(ε) = (Φfinal , Xfinal ) where ε denotes the empty sequence. This means that (σ0 , x0 ) and i0 , . . . , iT −1 qualify as an answer.
i

iT −1

0
For completeness, let (σ0 , x0 ) −→· · · −−→ (σT , xT ) be a run of S . We can take−−−−→
(σs , m) :=

B.3



s(xT −1 , iT −1 ), σT (xa ) , . . . , s(x0 , i0 ), σ1 (xa ).

2

Proof of Lem. 3.7−−−−→
Proof. Assume the node (Φ, X) at the position (σs , m) has an unsatisfiable label. Consider its child at−−−−→
the position (σs , m)(σs0 , m0 ), for arbitrary σs0 ∈ BVarand m0 ∈ Modes.
s
We know Φ = false or X = 0/ from Lem. A.3. In case Φ = false, we easily see thatπC (1-BSpre (σs , m)(Φ, X)) = false .
In case X = 0,
/ similarly
πP (1-BSpre (σs , m)(Φ, X)) = 0/ .

2