Towards an Approximate Conformance Relation for
Hybrid I/O Automata
Morteza Mohaqeqi

Mohammad Reza Mousavi

Department of Information Technology
Uppsala University, Sweden
morteza.mohaqeqi@it.uu.se

Centre for Research on Embedded Systems,
School of IT, Halmstad University, Sweden
m.r.mousavi@hh.se

Several notions of conformance have been proposed for checking the behavior of cyber-physical
systems against their hybrid systems models. In this paper, we explore the initial idea of a notion
of approximate conformance that allows for comparison of both observable discrete actions and
(sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely
the notion of Hybrid Input-Output Conformance (HIOCO) by M. van Osch and the notion of Hybrid
Conformance by H. Abbas and G.E. Fainekos. We prove that our proposed notion of conformance
satisfies a semi-transitivity property, which makes it suitable for a step-wise proof of conformance or
refinement.

1

Introduction

Conformance testing is a practical and rigorous technique for verifying system correctness against a specification. In the context of cyber-physical systems, several notions of conformance have been proposed
for testing such systems against their hybrid systems models, of which hybrid input-output conformance
(hioco) [17] and (τ , ε )-hybrid conformance (hconf ) [2, 3] are two notable examples. As we noted earlier
in [16, 13], these two notions are substantially different in that hconf allows for approximate comparison
of system dynamics, while hioco provides direct support for discrete actions and non-deterministic and
partial specifications. Hence, as indicated in [16, 13], combining the advantages of these approaches will
be beneficial and will lead to a flexible and realistic definition of conformance with the above-mentioned
characteristics.
In this paper, we define an approximate notion of conformance that allows for approximate comparison of both (sampled) continuous signals and observable discrete actions. To this end, we take the notion
of hconf [2, 3], and interpret discrete actions as special signals with discrete values (0 and ∞). As a first
sanity check, we set out to prove that our notion of conformance is a pre-order (i.e., it is reflexive and
transitive), making it suitable for step-wise conformance testing and refinement. Reflexivity immediately follows from the definition; transitivity, however, requires a twist in accumulating the conformance
bounds (error margins). We formulate the notion of semi-transitivity and prove that our proposed notion
is indeed semi-transitive.
We illustrate the definitions using a simple example of a thermostat. The thermostat has two input
discrete actions ON and OFF and one output (continuous) variable x denoting the current temperature.
The dynamics of the temperature are different depending on the state of the thermostat, which is in turn
determined by the discrete input actions. We provide a formalization of an ideal thermostat in hybrid
(I/O) automata and analayze the conformance of its implementation with respect to the specification.
The rest of this paper is organized as follows. In Section 2, we present an overview of the related
work and position our approach with respect to the state of the art in the literature. In Section 3, we
Kargahi and Trivedi: Verification and Validation of
Cyber-Physical Systems 2016 (V2CPS-16)
EPTCS 232, 2016, pp. 53–64, doi:10.4204/EPTCS.232.8

c M. Mohaqeqi and M.R. Mousavi
This work is licensed under the
Creative Commons Attribution License.

Approximate Conformance for Hybrid I/O Automata

54

introduce the preliminary definitions regarding hybrid I/O automata and their traces. In Section 4, we
review the notion of hioco. In Section 5, we first review the notion of hconf and show how it can be
extended to treat conformance for systems with discrete actions. Additionally, we state and prove it
semi-transitivity property. In Section 6, we conclude the paper and present some directions for future
research.

2

Related Work

There is a substantial literature on approximate notions of behavioral equivalence and/or pre-order for
hybrid systems. We have already mentioned two examples of such notions, namely hybrid input-output
conformance (hioco) [17] and (τ , ε )-hybrid conformance (hconf ) [2, 3]. Additionally, there are a number
of notions of approximate equivalence / pre-order based on Metrics such as [10, 11, 18]. In [16, 13],
we formally relate some of the basic notions of conformance for hybrid systems and their underlying
semantic models.
We expect the extension of our notion to the non-deterministic case to be straightforward; in [17]
and [3] already non-deterministic models are considered. The extension to richer semantic domains,
e.g., with probabilistics or stochastics, are far less trivial. We refer to [12, 19] for related ideas in this
direction.

3

Preliminaries

This section introduces the basic definitions and notations used throughout the rest of the paper, including
a formal definition of hybrid I/O automata and their associated traces.

3.1 Notation and Basic Definitions
We denote the set of real numbers by R and the set of non-negative integers by N. Given a tuple α =
(a1 , a2 , . . . , an ), the ith element of the tuple is denoted by γi (α ), that is, γi (α ) = ai .
For a function f , we denote its domain by dom( f ). For a set S, the restriction of f to S, denoted by
f ⌈S, is a function with the domain dom( f ) ∩ S, where ( f ⌈S)(c) = f (c), ∀c ∈ S.
In order to describe the system dynamics, we define and use the following notions of valuation and
trajectory.
Definition 1 (Valuation) Consider a set of real-valued variables V . A valuation of V is a function of
type V 7→ R, which assigns a real number to each variable v ∈ V . The set of all valuations of V is denoted
by Val(V ).
Definition 2 (Trajectory) Let D ⊂ R be an interval. A trajectory σ is a function σ : D → Val(V ) that
maps each element in interval D to a valuation. The set of all trajectories associated to V is denoted by
trajs(V ).
Consider a set of variables V and the corresponding set of valuations Val(V ). The restriction of a
valuation val ∈ Val(V ) to a set V ′ ⊆ V , denoted by val ↓ V ′ , is a valuation val′ ∈ Val(V ′ ) where for all
v ∈ V ′ , val′ (v) = val(v). Also, the restriction of a trajectory σ : D → Val(V ) to a set V ′ ⊆ V , denoted by
σ ↓ V ′ , is a trajectory D → Val(V ′ ) where (σ ↓ V ′ )(t) = σ (t) ↓ V ′ for all t ∈ D.
For a trajectory σ , the first valuation of σ (i.e., σ (min(dom(σ )))), if it exists, is denoted by σ .fval.
Moreover, if dom(σ ) is right-closed, then σ .lval is defined as the last valuation of σ .

M. Mohaqeqi and M.R. Mousavi

55

For an interval D ⊆ R and an arbitrary t ≥ 0, we define D + t , {t ′ + t|t ′ ∈ D} as the time shift of D.
Moreover, for a trajectory σ with domain D, σ + t is defined as a function with domain D + t such that
∀t ′ ∈ D : (σ + t)(t ′ + t) = σ (t ′ ).
For a trajectory σ , define τ D t , (τ ⌈[t, ∞)) − t. Additionally, trajectory σ is a prefix of trajectory σ ′ ,
denoted as σ ≤ σ ′ , if and only if σ = σ ′ ⌈dom(σ ). Also, the concatenation of two trajectories σ and σ ′
is defined by σ ⌢ σ ′ , σ ∪ σ ′ .

3.2 Hybrid Automata
Hybrid I/O automata (HIOA) [14] are defined as the extension of hybrid automata [5] with an additional
classification of external actions and variables as inputs and outputs. Hence, we first review the definition
of hybrid automata and then introduce its extension to input and output actions and variables.
Definition 3 (Hybrid Automata) A hybrid automaton (HA) A = (W, X , Q, Θ, E, H, D, T) consists of
• A set W of external variables and a set X of internal variables, disjoint from each other. We write
V ≡ W ∪ X.
• A set Q ⊆ Val(X ) of states.
• A nonempty set Θ ⊆ Q of start states.
• A set E of external actions and a set H of internal actions, disjoint from each other. We write
A ≡ E ∪ H.
a

• A set D ⊆ Q × A × Q of discrete transitions. We use x →A x′ as shorthand for (x, a, x′ ) ∈ D. We
a
sometimes drop the subscript and write x → x′ , when we think A should be clear from the context.
a
We say that a is enabled in x if there exists an x′ such that x → x′ .
• A set T of trajectories for V such that τ (t)⌈X ∈ Q for every τ ∈ T and t ∈ dom(τ ). Given a
trajectory τ ∈ T we denote τ .fval⌈X by τ .fstate and, if τ is closed, we denote τ .lval⌈X by τ .lstate.
We require that the following axioms hold:
T1 (Prefix closure)
For every τ ∈ T and every τ ′ ≤ τ , τ ′ ∈ T.
T2 (Suffix closure) For every τ ∈ T and every t ∈ dom(τ ), τ D t ∈ T
T3 (Concatenation closure) Let τ0 , τ1 , τ2 , . . . be a sequence of trajectories in T such that, for
each nonfinal index i, τi is closed and τi .lstate = τi+1 .fstate. Then τ0⌢ τ1⌢ τ2 . . . ∈ T.
Example 4 Figure 1a, due to [4], shows the hybrid automaton of the thermostat described in Section
1 with the set of variables of W = {y}, X = {l, x}, where l is a two-valued variable (mode ON and
mode OFF) determining the location of the automaton, x is a continuous real-valued variable, and y is
always equal to x, i.e., y(t) = x(t), ∀t ≥ 0. Further, the set of actions is specified as E = {ON OFF}, and
H = {}. Also, we have
Q = {(l, x) | l ∈ {mode ON, mode OFF}, 0 ≤ x ≤ 20}
and Θ = {(mode ON, 5)}. Trajectories generated by this HIOA are specified according to the differential
equations given for each location. Figure 1b depicts a set of trajectories for variable x (or equivalently
external variable y).

Approximate Conformance for Hybrid I/O Automata

56

20

τ0

τ2

τ4

15
x(t)

ON (x(t) ≤ 2)
mode ON

mode OFF

ẋ(t) = −x(t) + 20

ẋ(t) = −x(t)

x(t) ≤ 20

x(t) ≥ 0

5

0

OFF (x(t) ≥ 18)
(a) Hybrid automaton of the thermostat

τ3

τ1

10

0

2

4

6

8

10

t

(b) A sample of the continuous dynamics of the
system

Figure 1: Thermostat example

3.3 Hybrid I/O Automata
As mentioned before, an HIOA is a hybrid automaton in which the set of variables and actions are
classified as input and output, as specified below.
Definition 5 (Hybrid I/O Automata [14]) A hybrid I/O automaton (HIOA) is a tuple (H ,WI ,WO , EI , EO )
where
• H = (W, X , Q, Θ, E, H, D, T) is a hybrid automaton.
• WI and WO partition W into input and output variables, respectively. Variables in Z ≡ X ∪WO are
called locally controlled.
• EI and EO partition E into input and output actions, respectively. Actions in L ≡ H ∪ EO are called
locally controlled.
• The following additional axioms are satisfied:
– E1 (Input action enabling)
a
For every x ∈ Q and every a ∈ EI , there exists x′ ∈ Q such that x → x′ .
– E2 (Input trajectory enabling)
For every x ∈ Q and every v ∈ trajs(WI ), there exists τ ∈ T such that τ .fstate = x, τ ↓ WI ≤ v
and either
1. τ ↓ WI = v, or
2. τ is closed and some l ∈ L is enabled in τ .lstate.
Example 6 Consider the hybrid automaton described in Example 4. Classifying the set of variables into
input and output variables WI = {}, WO = {y} and the set of actions into input and output actions as
EI = {ON}, EO = {OFF} reveals the corresponding HIOA.
For an HIOA, a state is said to be agile if it affords some trajectory, i.e., there exists trajectory σ ∈ T
σ
for which s →. To show that a state is agile, we add a spacial action ξ to the set of output actions EO (the
usage of this action is explained in the next section).

M. Mohaqeqi and M.R. Mousavi

57

3.4 Hybrid sequences, executions, traces and solution pairs
To describe the behavior of a hybrid (I/O) automaton, we use the notions of execution, trace and solution
pair. To this end, we first define a notation of hybrid sequence.
Definition 7 (Hybrid Sequence [14]) Take a set of variables V and a set of actions A. Then, an (V, A)sequence is defined as a finite or infinite sequence α = τ0 , a1 , τ1 , a2 , . . ., in which
• each τi denotes a trajectory in trajs(V);
• each αi denotes an action in A;
• if α is finite then it ends with a trajectory;
• if τi is not the last trajectory in the sequence then dom(τi ) is closed.
Any (V, A)-sequence is called a hybrid sequence.
Next, we define the notions of execution fragment and execution for a hybrid I/O automaton.
Definition 8 (Execution Fragment and Execution [14]) A hybrid sequence α = τ0 , a1 , τ1 , a2 , . . . is an
execution fragment for an HIOA A if (i) each τi is a trajectory in T, and (ii) if τi is not the last trajectory
ai+1
then τi .lstate → τi+1 .fstate. For an execution fragment α , we define α .fstate to be τ0 .fstate.
An execution fragment α = τ0 , a1 , τ1 , a2 , . . . is called an execution of a hybrid automata A if τ0 .fstate
is a start state, i.e., τ0 .fstate ∈ Θ.
We write execsA to denote the set of all executions of A .
To capture the external behavior of a hybrid (I/O) automaton, we use the notion of trace. Intuitively,
a trace of an execution specifies the sequence of its external actions and the evolution of the external
variables.
Definition 9 (Trace [14]) Consider an execution α . The trace of α , denoted by trace(α ), is the (E,W )restriction of α (It is recalled that E and W denote the set of external actions and external variables,
respectively).
Example 10 Figure 1b depicts a set of trajectories for variable x of the HIOA specified in Example 6.
According to this sample behavior, α = τ0 , OFF, τ1 , ON, τ2 specifies a trace of the HIOA.
Definition 11 (Solution Pair [3]) Assume that u and y are two traces for a HIOA H; (u, y) is a solution
pair to H if
• dom(u) = dom(y), and
• there exists a trace α to H such that dom(α ) = dom(u), u = α ↓ WI , and y = α ↓ WO .

4

I/O Conformance for Hybrid I/O Automata

In this section, we review the notion of hioco [17], which is an exact notion of conformance, and adopt
it for the HIOA formalism. Subsequently, in the next section, we will adapt the ideas explored in this
section to come up with an approximate notion of conformance. To this end, we first define the output
and the trajectories associated with a state of an HIOA.

Approximate Conformance for Hybrid I/O Automata

58

Definition 12 Assume that A = (H ,WI ,WO , EI , EO ) is a hybrid IO automaton with the sets Q and Θ of
states and starting states, respectively. For a state s ∈ Θ we define
(
o
{o ∈ EO | {ξ } ∪ s →} , if s is agile
(1)
out(s) =
o
{o ∈ EO | s →}
, otherwise
Furthermore, for a set C ⊆ Q we define:
out(C) =

[

out(s).

s∈C

Definition 13 (after operator) For an HIOA A and a trace t, after operator is defined as
t

A after t = {s | s0 → s}

(2)

Definition 14 (Trajectories of a state) For an HIOA A and a state s, traj(s) is defined as
σ

traj(s) = {σ ∈ T | s →}

(3)

In order to define conformance, we need to focus on those trajectories of the system under test for
which a trajectory with the same behavior exists in the specification. This is achieved by the following
infilter operator.
Definition 15 (infilter) Consider two sets of trajectories ΣI and ΣS on a set of variables V . Assume
VI ⊆ V is the set of input variables; then
infilter(ΣI , ΣS ) = {σ ∈ ΣI | ∃σ ′ ∈ΣS : σ ↓ VI = σ ′ ↓ VI }

(4)

Finally, the notion of HIOCO is defined HIOA below.
Definition 16 (extension of hioco) An (input-enabled) HIOA I is said to hybrid input-output conform to
another HIOA S, denoted by I hioco S, if and only if for all traces t ∈ traces(S):
out(I after t) ⊆ out(S after t), and
infilter (traj(I after t), traj(S after t)) ⊆ traj(S after t)
Example 17 Assume that we refer to the HIOA specified in Example 6 by S. As specified in Example 10,
α = τ0 , OFF, τ1 , ON, τ2 is a trace of S. Then, we have out(S after α ) = {OFF}. Now, assume an imaginary HIOA I which generates a trace α ′ = τ0 , OFF, τ1 , ON, τ2 , ON. It is seen that ON ∈ out(I after α ).
As a consequence, I does not conform to S since out(I after α ) 6⊆ out(S after α ).

5

Approximate Conformance for Hybrid I/O Automata

As it can be noted in Definition 16, HIOCO considers an implementation to be conforming when it
exactly follows (features a non-empty subset of the behavior of) the specification. However, due to
(unavoidable) inaccuracies during the implementation and testing of a CPS, this is not a feasible and
practical approach. We wish to allow for limited deviations of the implementation from the specification.
In this regard, Abbas et al. [2, 3] define a notion of closeness which is measures the degree of similarity
between the observed behavior of two systems. However, the approach ignores the input and output
actions and mainly focuses on the continuous behavior of the system. In the remainder of this section,
we first review the hybrid conformance relation proposed by Abbas et al. [2, 3] and then extend it,
following the recipe of HIOCO, with discrete input and output actions.

M. Mohaqeqi and M.R. Mousavi

59

5.1 Conformance Relation based on the Notion of Closeness
In the hybrid conformance approach [2, 3], the behavior of a system is specified using a notion of trace
in which the types of observable discrete actions are not explicitly specified. Instead, the number of
discrete jumps are considered relevant in the definition of hybrid conformance. This kind of trace, which
we call an action-insensitive trace (or an a-trace) hereafter, is defined based on the notion of hybrid time
domain, defined below.
Definition 18 (Hybrid Time Domain [3]) A hybrid time domain E is a subset of R+ × N defined as
E=

J−1
[

[t j ,t j+1 ] × { j}

(5)

j=0

where 0 = t0 ≤ t1 ≤ t2 ≤ ... ≤ tJ . We denote the set of all hybrid time domains by T.
The hybrid time domain is used to specify the evolution of a CPS regarding both continuous evolution
(using time intervals [t j ,t j+1 ]) and discrete jumps (using integer numbers j). Next, we define the notion
of action-insensitive trace which is subsequently used to define the approximate notion of conformance.1
Definition 19 (Action-Insensitive Trace [3]) Take a hybrid time domain E and a set of variables V . An
action-insensitive trace (a-trace) over E is a function φ : E → Val(V ), where for every j, t 7→ φ (t, j) is
absolutely continuous in t over the interval I j = {t|(t, j) ∈ E}. The set of all a-traces defined over the
variable set V is denoted by a-trace(V ).
As it can be noted, the notion of a-trace is an abstraction of a trace, as defined in Definition 9. In
fact, an a-trace can be obtained from a given trace by removing its actions and keeping only the number
of jumps.
Definition 20 ((τ ,ε )-closeness [3]) Consider a test duration T ∈ R+ , a maximum number of jumps J ∈
N, and τ , ε > 0; then two a-traces y1 and y2 are said to be (τ ,ε )-close, denoted by y1 ≈(τ ,ε ) y2 , if
1. for all (t, i) ∈ dom(y1 ) with t ≤ T, i ≤ J, there exists (s, j) ∈ dom(y2 ) such that |t − s| ≤ τ and
ky1 (t, i) − y2 (s, j)k ≤ ε , and
2. for all (t, i) ∈ dom(y2 ) with t ≤ T, i ≤ J, there exists (s, j) ∈ dom(y1 ) such that |t − s| ≤ τ and
ky2 (t, i) − y1 (s, j)k ≤ ε .
Definition 21 (Conformance Relation [3]) Consider two hybrid I/O automata H1 and H2 . Given a
test duration T ∈ R+ , a maximum number of jumps J ∈ N, and τ , ε > 0, H2 conforms to H1 , denoted by
H2 ≈(τ ,ε ) H1 , if and only if for all solution pairs (u, y1 ) of H1 , there exists a solution pair (u, y2 ) of H2
such that the corresponding output a-traces y1 and y2 are (τ ,ε )-close.
Figure 2 shows two a-traces y1 and y2 where y1 ≈(0.8,1) y2 . As mentioned, the notion of hconf (≈(τ ,ε ) )
is not sensitive to the existence/absence of actions. As a result, if the HIOA generating y1 produces
output action OFF at t = 2 and the other HIOA produces no action, the two a-traces are still regarded as
conforming according to hconf.
1 In

[3], the term Hybrid Arc is used to refer to this concept.

Approximate Conformance for Hybrid I/O Automata

60
20

y(t)

15

τ2′

10

τ2

τ1′

5

0

y1
y2

0.5

1

τ1

0

2

4

6

8

10

t

Figure 2: Two signals which are ≈τ ,ε for τ = 0.8 and ε = 1 but not for τ = 0.8 and ε = 0.4.

5.2 Extension
The goal of this section is to extend the notion of closeness and the corresponding conformance relation
to the case of hybrid I/O automata. The main difference of our extended conformance with that of Abbas
et al. [2] is that we include the input and output actions for the comparison of two behaviors (i.e., the
comparison of specification and implementation).
According to Definition 20, the notion of closeness is specified on the basis of comparing a-traces.
However, as mentioned in the previous section, an a-trace is an abstraction of a trace of a HIOA, in
which, the actions are not explicitly specified. As a result, a natural way for extending the notion of
closeness to HIOA is to augment the closeness definition (Definition 20) with additional conditions that
also compare the corresponding actions of the traces.
We extend the definition of a-trace such that it can reflect the occurrence of actions as well as the
change of continuous variables. For this purpose, we consider each action as a special continuous variables. This variable is assumed to get only two values: 0 and ∞, where a value of 0 denotes the absence
of the corresponding action while the value of ∞ denotes an instantaneous occurrence of the action.
To this end, we first assume that the set of real numbers is augmented with a special number ∞
which is regarded to be larger than any number in R, and hence larger than any arbitrary ε . Further, for
notational convenience, we define ∞ − ∞ = 0. Let R∞ denote R extended with ∞.
We extend the notion of trace and solution pair (Definitions 9 and 11) such that for any action in
a given HIOA, there is a fresh variable. Such variables get only two values, namely 0 and ∞. This
naturally extends the notion of a-trace to our notion of trace which has the same type (apart from the
fact that Val(V ) ranges over R∞ ); the only difference is that the set of variables also includes the freshly
introduced action variables.
In order to extend the notion of closeness (and thus, hconf conformance relation), we need to define
the meaning of a norm (kk) for the signals containing a mixture of normal real-valued variables and these
extended type of variables. Assume y1 and y2 are two vector of variables of the same length, i.e.,
y1 = (y1 [1], . . . , y1 [n])
y2 = (y2 [1], . . . , y2 [n])
We define the distance of y1 and y2 , denoted by ky2 − y1 ke , as
(
∞,
∃i ∈ {1, . . . , n}s.t.(y1 [i] = ∞ and y2 [i] 6= ∞) or (y1 [i] 6= ∞ and y2 [i] = ∞)
ky2 − y1 ke =
(6)
ky2 − y1 k, otherwise

M. Mohaqeqi and M.R. Mousavi

61

where ky2 − y1 k denotes the ordinary Euclidean distance. Then, we can modify the definition of (τ ,ε )closeness based on this notion of distance.
Definition 22 (Modified (τ ,ε )-closeness) Consider a test duration T ∈ R+ , a maximum number of jumps
J ∈ N, and τ , ε > 0; then two a-traces y1 and y2 are said to be (τ ,ε )-close, denoted by y1 ≈e(τ ,ε ) y2 , if
1. for all (t, i) ∈ dom(y1 ) with t ≤ T, i ≤ J, there exists (s, j) ∈ dom(y2 ) such that |t − s| ≤ τ and
ky1 (t, i) − y2 (s, j)ke ≤ ε , and
2. for all (t, i) ∈ dom(y2 ) with t ≤ T, i ≤ J, there exists (s, j) ∈ dom(y1 ) such that |t − s| ≤ τ and
ky2 (t, i) − y1 (s, j)ke ≤ ε .
Definition 23 (Conformance Relation) Consider two hybrid I/O automata H1 and H2 . Given a test
duration T ∈ R+ , a maximum number of jumps J ∈ N, and τ , ε > 0, H2 conforms to H1 , denoted by
H2 ≈e(τ ,ε ) H1 , if and only if for all solution pairs (u, y1 ) of H1 , there exists a solution pair (u, y2 ) of H2
such that the corresponding output a-traces y1 and y2 are (τ ,ε )-close, considering the modified notion of
closeness in Definition 22.
Example 24 Consider two traces α = τ1 , OFF, τ2 and α ′ = τ1′ , τ2′ where τ1 , τ2 , τ1′ , and τ2′ are trajectories
shown in Fig. 2. Let φ1 and φ2 be the corresponding a-traces obtained according to the abovementioned
method for encoding the actions as numeric variables. Then, according to the modified notion of closeness, we will have φ1 6≈e(τ ,ε ) φ2 .

5.3 Step-wise Approximate Refinement
In order to apply our notion of conformance in a step-wise refinement trajectory, one needs to compose approximate conformance relations. This can be achieved through the following notion of semitransitivity.
Definition 25 (Semi-Transitivity) Let H1 , H2 , and H3 be three arbitrary hybrid I/O automata such
that H2 ≈(τ1 ,ε1 ) H1 and H3 ≈(τ2 ,ε2 ) H2 for some τ1 , τ2 , ε1 , ε2 > 0. Then, the conformance relation is
semi-transitive if H3 ≈(τ1 +τ2 ,ε1 +ε2 ) H1 .
Theorem 26 The extended conformance relation is semi-transitive.
Proof For the proof, we first formally specify the assumptions and the thesis of the theorem; the latter
is further refined and proven in a number of steps:
1. Assumption: H1 ≈e(τ1 ,ε1 ) H2 and H2 ≈e(τ2 ,ε2 ) H3 .
Claim: H1 ≈e(τ1 +τ2 ,ε1 +ε2 ) H3 .
2. Assumption Rewriting (according to Definition 22):
∀(u, y1 ) ∈ H1 : ∃(u, y2 ) ∈ H2 such that y1 ≈e(τ1 ,ε1 ) y2 ,

(7)

y2 ≈e(τ2 ,ε2 ) y3 .

(8)

∀(u, y2 ) ∈ H2 : ∃(u, y3 ) ∈ H3 such that

Claim: ∀(u, y1 ) ∈ H1 : ∃(u, y3 ) ∈ H3 such that y1 ≈e(τ1 +τ2 ,ε1 +ε2 ) y3 .
3. Assumption Rewriting:
∀(u, y1 ) ∈ H1 : ∃(u, y2 ) ∈ H2 such that
∀(t, i) ∈ dom(y1 ) : ∃(s, j) ∈ dom(y2 ) such that |t − s| ≤ τ1 and ky1 (t, i) − y2 (s, j)ke ≤ ε1 , (9)

Approximate Conformance for Hybrid I/O Automata

62
and also
∀(u, y2 ) ∈ H2 : ∃(u, y3 ) ∈ H3 such that

∀(s, j) ∈ dom(y2 ) : ∃(v, k) ∈ dom(y3 ) such that |v − s| ≤ τ2 and ky2 (s, j) − y3 (v, k)ke ≤ ε2 , (10)
conditioned on that t ≤ T and i ≤ J.
Claim:
∀(u, y1 ) ∈ H1 : ∃(u, y3 ) ∈ H3 such that
∀(t, i) ∈ dom(y1 ) : ∃(v, k) ∈ dom(y3 ) such that |v−t| ≤ τ1 + τ2 and ky1 (t, i)−y3 (v, k)ke ≤ ε1 + ε2 .
(11)
Now, we proceed with the proof. Fix an arbitrary (u, y1 ) ∈ H1 ; it follows from (9) that ∃y2 such that
(u, y2 ) ∈ H2 for which ∀(t, i) ∈ dom(y1 ) there exists (s, j) ∈ dom(y2 ) such that
|t − s| ≤ τ1

(12)

ky1 (t, i) − y2 (s, j)ke ≤ ε1

(13)

and
Similarly, from (10), it follows that considering y2 , ∃y3 such that (u, y3 ) ∈ H3 for which ∀(s, j) ∈ dom(y2 )
there exists (v, k) ∈ dom(y3 ) such that
(14)
|s − v| ≤ τ2
and
ky2 (s, j) − y3 (v, k)ke ≤ ε2 .

(15)

Now, fix an arbitrary ∀(t, i) ∈ dom(y1 ) and assume (s, j) and (v, k) are the corresponding points as
specified above. Since ε1 has a bounded value (i.e., ε1 < ∞), we can conclude from (13) that the value of
those variables in y1 (t, i) and y2 (s′ , j′ ) which are associated with the actions is exactly the same. This is
because that otherwise ky1 (t, i) − y2 (s′ , j′ )ke = ∞ > ε1 (according to (6)) which violates (13). The same
results hold for y2 (s′ , j′ ) with respect to y3 (v, k). As a consequence, the norm operator in (13) and (15)
is reduced to the normal Euclidean norm which yields the following relation (according to the triangular
property of the Euclidean norm)
ky1 (t, i) − y3 (v, k)ke ≤ ε1 + ε2 .

(16)

Besides, from (12) and (14) it is concluded that
|t − v| ≤ τ1 + τ2
Consequently, the claim declared in (11) is achieved.

6

(17)


Conclusions and Discussion

In this paper, we proposed a notion of conformance parameterized by conformance bounds in time and
value. In addition to approximate comparison of (sampled) continuous signals, our notion allows for
approximate matching of discrete signals by allowing them to happen within specified time margins. In

M. Mohaqeqi and M.R. Mousavi

63

this sense, it consolidates two earlier notions of hybrid conformance by Abbas and Fainekos [2] and by
van Osch [17].
In the remainder of this section, we present the directions of our ongoing research. As an immediate next step, we would like to prove the conservative extension property of the extended conformance
relation compared to the other conformance relations, namely hioco and hconf. This will generalize our
earlier result in [16]. Moreover, we envisage other important issues such as sound sampling rates [15],
test-case generation algorithms, coverage [8, 9], links to temporal and modal logics [7], and compositionality [1, 6].

References
[1] Houssam Abbas & Georgios E. Fainekos (2015): Towards composition of conformant systems. CoRR
abs/1511.05273. Available at http://arxiv.org/abs/1511.05273.
[2] Houssam Abbas, Hans Mittelmann & Georgios E. Fainekos (2014): Formal property verification in a conformance testing framework. In: Formal Methods and Models for Codesign (MEMOCODE), 2014 Twelfth
ACM/IEEE International Conference on, pp. 155–164, doi:10.1109/MEMCOD.2014.6961854.
[3] Houssam Y. Abbas (2015): Test-Based Falsification and Conformance Testing for Cyber-Physical Systems.
Ph.D. thesis, Arizona State University. Available at http://hdl.handle.net/2286/R.A.150686.
[4] Arend Aerts, Mohammad Reza Mousavi & Michel A. Reniers (2016): Model-based testing of cyber-physical
systems. In: Cyber-Physical Systems: Foundations, Principles and Applications, Elsevier. To appear.
[5] Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger & Pei Hsin Ho (1993): Hybrid automata: An
algorithmic approach to the specification and verification of hybrid systems. In Robert L. Grossman, Anil
Nerode, Anders P. Ravn & Hans Rischel, editors: Hybrid Systems, Springer Berlin Heidelberg, pp. 209–229,
doi:10.1007/3-540-57318-6_30.
[6] Nikola Benes, Przemyslaw Daca, Thomas A. Henzinger, Jan Kretı́nský & Dejan Nickovic (2015): Complete
Composition Operators for IOCO-Testing Theory. In: Proceedings of the 18th International ACM SIGSOFT
Symposium on Component-Based Software Engineering (CBSE 2015), ACM, pp. 101–110.
[7] Jyotirmoy V. Deshmukh, Rupak Majumdar & Vinayak S. Prabhu (2015): Quantifying Conformance Using
the Skorokhod Metric. In Daniel Kroening & S. Corina Păsăreanu, editors: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015), Part II, Springer, pp. 234–250, doi:10.
1007/978-3-319-21668-3_14.
[8] Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin & Jyotirmoy V. Deshmukh (2015): Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems. In Klaus
Havelund, Gerard J. Holzmann & Rajeev Joshi, editors: Proceedings of the 7th International Symposium
of NASA Formal Methods (NFM 2015), Lecture Notes in Computer Science 9058, Springer, pp. 127–142,
doi:10.1007/978-3-319-17524-9_10.
[9] Georgios E. Fainekos (2015): Automotive control design bug-finding with the STaLiRo tool. In: Proceedings
of the American Control Conference (ACC 2015), IEEE, p. 4096, doi:10.1109/ACC.2015.7171969.
[10] Antoine Girard & George J. Pappas (2011): Approximate Bisimulation: A Bridge Between Computer Science
and Control Theory. European Journal of Control 17(5-6), pp. 568–578, doi:10.3166/ejc.17.568-578.
[11] A. Agung Julius, Alessandro D’Innocenzo, Maria Domenica Di Benedetto & George J. Pappas (2009): Approximate equivalence and synchronization of metric transition systems. Systems & Control Letters 58(2),
pp. 94–101, doi:10.1016/j.sysconle.2008.09.001.
[12] A. Agung Julius & George J. Pappas (2009): Approximations of Stochastic Hybrid Systems. IEEE Trans.
Automat. Contr. 54(6), pp. 1193–1203, doi:10.1109/TAC.2009.2019791.

64

Approximate Conformance for Hybrid I/O Automata

[13] Narges Khakpour & Mohammad Reza Mousavi (2015): Notions of Conformance Testing for Cyber-Physical
Systems: Overview and Roadmap (Invited Paper). In: Proceedings of the 26th International Conference on
Concurrency Theory (CONCUR 2015), LIPIcsLeibniz International Proceedings in Informatics.
[14] Nancy Lynch, Roberto Segala & Frits Vaandrager (2003): Hybrid I/O automata. Information and Computation 185(1), pp. 105–157, doi:10.1016/S0890-5401(03)00067-1.
[15] Morteza Mohaqeqi & Mohammad Reza Mousavi (2016): Sound Test-Suites for Cyber-Physical Systems. In:
Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering (TASE
2016), IEEE Computer Society, doi:10.1109/TASE.2016.33.
[16] Morteza Mohaqeqi, Mohammad Reza Mousavi & Walid Taha (2014): Conformance Testing of CyberPhysical Systems: A Comparative Study. In: Proceedings of the 14th International Workshop on Automated
Verification of Critical Systems (AVOCS 2014), Electronic Communications of the EASST 70.
[17] Michiel van Osch (2006): Hybrid input-output conformance and test generation. In: FATES/RV, Springer
Berlin Heidelberg, pp. 70–84.
[18] Paulo Tabuada (2007): Approximate Simulation Relations and Finite Abstractions of Quantized Control
Systems. In: Proceedings of the 10th International Workshop on Hybrid Systems: Computation and
Control (HSCC 2007), Lecture Notes in Computer Science 4416, Springer, pp. 529–542, doi:10.1007/
978-3-540-71493-4_41.
[19] Majid Zamani, Alessandro Abate & Antoine Girard (2015): Symbolic models for stochastic switched systems: A discretization and a discretization-free approach. Automatica 55, pp. 183–196, doi:10.1016/j.
automatica.2015.03.004.

