Modeling Hybrid Systems in the Concurrent Constraint
Paradigm
Damián Adalid

Marı́a del Mar Gallardo

Laura Titolo

Dept. Lenguajes y Ciencias de la Computación
E.T.S.I. Informática University of Málaga∗
[damian,gallardo,laura.titolo]@lcc.uma.es

Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate
and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contrast to the variable/value style typical of imperative languages. Several extensions of
ccp have been proposed in order to model reactive systems. One of these extensions is the Timed
Concurrent Constraint Language (tccp) that adds to ccp a notion of discrete time and new features to
model time-out and preemption actions.
The goal of this paper is to explore the expressive power of tccp to describe hybrid systems. We
introduce the language Hy-tccp as a conservative extension of tccp, by adding a notion of continuous
time and new constructs to describe the continuous dynamics of hybrid systems. In this paper, we
present the syntax and the operational semantics of Hy-tccp together with some examples that show
the expressive power of our new language.

1

Introduction

In the last years, concurrent, reactive and hybrid systems have become essential to model a large number
of modern applications. Often, systems of this kind are classified as critical, i.e., an error in the software
can have tragic consequences in terms of human lives or money. This is the case of avionic or automotive
software, e-banking, or financial applications.
Description, verification and analysis of concurrent and reactive systems are very hard tasks, due
to the concurrent execution of different agents and to issues of synchronization. In the case of hybrid
systems, these phases are even harder due to the combination of discrete and continuous dynamics and
the presence of real-valued variables. Therefore, it is important to develop high-level description languages that allow these systems to be modeled with enough precision and at the same time that ease the
application of formal methods techniques.
Many formalisms have been developed to describe concurrent systems. One of these is the Concurrent Constraint paradigm (ccp) [10], a simple but powerful model for concurrent systems. It differs
from other paradigms mainly due to the notion of store-as-constraint that replaces the classical storeas-valuation model. In this paradigm, the agents running in parallel communicate by means of a global
constraint store. The Timed Concurrent Constraint Language [2] (tccp in short) is a concurrent logic language obtained by extending ccp with the notion of time and a suitable mechanism to model time-outs
and preemptions.
∗
This work has been supported by the Andalusian Excellence Project P11-TIC7659 and the Spanish Ministry of Economy
and Competitiveness project TIN2012-35669

S. Escobar (Ed.): XIV Jornadas sobre Programación
y Lenguajes, PROLE 2014, Revised Selected Papers
EPTCS 173, 2015, pp. 1–15, doi:10.4204/EPTCS.173.1

© Adalid, Gallardo & Titolo
This work is licensed under the
Creative Commons Attribution License.

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

2

In this paper, we present the language Hy-tccp: an extension of tccp over continuous time. Hytccp is a non-deterministic and synchronous language that incorporates continuous variables that follow
dynamics determined by an ordinary differential equation (ODE). Its declarative nature facilitates a high
level description of hybrid systems in the style of hybrid automata [8]. Furthermore, its logical nature
facilitates the development of semantics based program manipulation tools for hybrid systems (verifiers,
analyzers, debuggers. . . ). Parallel composition of hybrid automata is naturally supported in Hy-tccp
due to the existence of a global shared store and to the synchronization mechanism inherited from tccp.
By defining Hy-tccp, we show that the extension of a declarative constraint language with continuous
dynamics is not only possible, but it leads to a powerful and expressive language able to describe complex
hybrid systems.
In this paper, we have only considered the modeling of multi-rated [5] hybrid systems, i.e., systems
whose continuous variables follow a constant dynamics. However, in the future we aim to relax this
restriction in order to describe more complex dynamics such as those defined by rectangular sets.
The paper is organized as follows. In Section 2, we briefly introduce the language tccp and the
essential aspects of hybrid automata. In Section 3, we introduce the new language Hy-tccp together with
its operational semantics, and we describe the new features that have been added to tccp in order to
model hybrid systems. Section 4 contains some examples to highlight the expressive power of Hy-tccp.
Section 5 presents some related work and, finally, Section 6 concludes the paper and outlines future
work.

2

Background

In this section we present some background to clarify the contributions of the paper. In Subsection 2.1,
we introduce the language tccp, the starting point for the definition of Hy-tccp. In Subsection 2.2, we
introduce the basic notions of hybrid automata, which is the formalism commonly used to describe hybrid
systems.

2.1 The Timed Concurrent Constraint Language
The Timed Concurrent Constraint Language (tccp, [2]) is a time extension of ccp. It adds to ccp the
notion of time and the ability to capture the absence of information. With these features, one can specify
behaviors typical of concurrent and reactive systems.
The computation in tccp proceeds as the concurrent execution of several agents that can monotonically add constraints in a global store or query information from it. As are all the languages from the cc
paradigm, tccp is parametric w.r.t. a cylindric constraint system.
D EFINITION 2.1 (C YLINDRIC
braic structure of the form:

CONSTRAINT SYSTEM

[2]) A cylindric constraint system is an alge-

C = ⟨C, ⪯, ∧, true, false, Var, ∃⟩
such that:
1. ⟨C, ⪯, ∧, true, false⟩ is a complete lattice where ∧ is the least upper bound (lub) operator, and true
and false are, respectively, the least and the greatest elements of C. We often use the inverse order
⊢ (the entailment relation) instead of ⪯ over constraints. Formally ∀c,d ∈ C c ⪯ d ⇔ d ⊢ c.
2. Var is a denumerable set of variables.

Adalid, Gallardo & Titolo

3

3. For each element x ∈ Var, a function (also called cylindric operator) ∃x ∶C → C is defined such that,
for any c,d ∈ C the following axioms hold:
(a) c ⊢ ∃x c
(b) if c ⊢ d then ∃x c ⊢ ∃x d
(c) ∃x (c ∧ ∃x d) = ∃x c ∧ ∃x d
(d) ∃x (∃y c) = ∃y (∃x c)
The entailment relation ⊢ intuitively states that if c contains more information than d then c ⊢ d. The
lub operator ∧ merges the information from two constraints (e.g. x > 0 ∧ x > 5 ∧ y = 9 ∶= x > 5 ∧ y = 9 and
x = 0 ∧ x = 7 ∶= false). The cylindrification (or hiding) operator is defined in terms of a general notion
of existential quantifier. It is used to project away information about the considered variable in order to
make it local to the constraint and hide it from the context (e.g. ∃x (x = 0 ∧ y = x ∧ z > 7) ∶= y = 0 ∧ z > 7).
The tccp global store is monotonic in the sense that once a constraint is added to the store, it cannot
be removed. Thus, given the store x > 0 ∧ y > 2 we can add the information x > 5 and obtain the store
x > 5 ∧ y > 2. Furthermore, by adding x = 0 we obtain the inconsistent store false since the constraint x = 0
is in contradiction with the information already present in the store.
The syntax of tccp agents is given by the grammar:
x)
A ∶∶= stop ∣ tell(c) ∣ A ∥ A ∣ ∃x A ∣ ∑ni=1 ask(ci ) → A ∣ now c then A else A ∣ p(⃗
where c, c1 ,... ,cn are finite constraints in C, p is a process symbol, and x⃗ ∈ Var × ⋅⋅⋅× Var. A tccp program
is a pair D .A, where A is the initial agent and D is a set of process declarations of the form p(⃗
x) ∶ −A.
The operational semantics of tccp [2] is described by a transition system T = (Conf ,→). Configurations in Conf are pairs ⟨A, c⟩ representing the agent A to be executed in the current global store c. The
transition relation → ⊆ Conf × Conf is the least relation satisfying the rules in Figure 1. Each transition
step takes exactly one time-unit. The notion of time is introduced by defining a global clock which
synchronizes all agents.
As can be seen from the rules, the stop agent represents the successful termination of the computation. The tell(c) agent adds the constraint c to the current store by means of the ∧ operator and then stops.
It takes one time-unit, thus the constraint c is visible to the other agents from the following time instant.
The choice agent ∑ni=1 ask(ci ) → Ai consults the store and non-deterministically executes (at the following
time instant) one of the agents Ai whose corresponding guard ci is entailed by the current store; otherwise, if no guard is entailed by the store, the agent suspends. The conditional agent now c then A else B
behaves (in the current time instant) like A (respectively B) if c is (respectively is not) entailed by the
store. This conditional agent is able to process negative information (lack of some information): it can
capture when some information is not present in the store since the agent B is executed both when ¬c is
satisfied, but also when neither c nor ¬c are satisfied. A ∥ B models the parallel composition of A and B in
terms of maximal parallelism, i.e., all the enabled agents of A and B are executed at the same time. The
agent ∃x A makes variable x local to A, to this end, it uses the ∃ operator of the constraint system. More
specifically, it behaves like A with x considered local, i.e., the information on x provided by the external
environment is hidden to A, and the information on x produced by A is hidden to the external world.
In the corresponding rule, the store l in the agent ∃l xA represents the store local to A. This auxiliary
operator is linked to the hiding construct by setting the initial local store to true, thus ∃x A ∶= ∃true xA.
Finally, the agent p(⃗
x) takes from D a declaration of the form p(⃗
x) ∶ −A and then executes A.

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

4

∃1 ≤ j ≤ n.d ⊢ c j
n
⟨∑i=1 ask(ci ) → Ai , d⟩ → ⟨A j , d⟩

⟨tell(c), d⟩ → ⟨stop, c ∧ d⟩
⟨A, d⟩ → ⟨A′ , d ′ ⟩, d ⊢ c
⟨now c then A else B, d⟩ → ⟨A′ , d ′ ⟩

⟨A, d⟩ →,
/ d ⊢c
⟨now c then A else B, d⟩ → ⟨A, d⟩

⟨B, d⟩ → ⟨B′ , d ′ ⟩, d ⊬ c
⟨now c then A else B, d⟩ → ⟨B′ , d ′ ⟩

⟨B, d⟩ →,
/ d ⊬c
⟨now c then A else B, d⟩ → ⟨B, d⟩

⟨A, d⟩ → ⟨A′ , d ′ ⟩ ⟨B, d⟩ → ⟨B′ , c′ ⟩
⟨A ∥ B, d⟩ → ⟨A′ ∥ B′ , d ′ ∧ c′ ⟩

⟨A, d⟩ → ⟨A′ , d ′ ⟩ ⟨B, d⟩ →
/
′
′
⟨A ∥ B, d⟩ → ⟨A ∥ B, d ⟩
⟨B ∥ A, d⟩ → ⟨B ∥ A′ , d ′ ⟩

⟨A, l ∧ ∃x d⟩ → ⟨B, l ′ ⟩
⟨∃l x A, d⟩ → ⟨∃l′ xB, d ∧ ∃x l ′ ⟩

p(⃗
x) ∶− A ∈ D
⟨p(⃗
x), d⟩ → ⟨A, d⟩

Figure 1: The transition system for tccp.

2.2 Introduction to hybrid automata
Many real systems have complex behaviors and evolve following both discrete and continuous dynamics. These systems are called hybrid systems. For instance, a cooler system is a hybrid system: it has
two discrete states (on or off ) that are chosen according to the temperature of the room, which evolves
continuously over time.
Hybrid automata [8] are an extension of finite-state automata used to describe hybrid systems. Intuitively, the discrete behavior of a hybrid automaton is defined by means of a finite set of discrete states
(called locations) and a set of (instantaneous) discrete transitions from one location to another. The continuous behavior of hybrid automata is described at each location by means of some Ordinary Differential
Equations (ODEs) which describe how continuous variables evolve over time (continuous transitions).
D EFINITION 2.2 (H YBRID

AUTOMATON )

A hybrid automaton H is a tuple

⟨Loc, T, Σ, X , Init, Inv, Flow,Jump⟩
where:
• Loc is a finite set {loc1 ,... ,locn } of discrete states (locations).
• T ⊆ Loc × Loc is a finite set of discrete transitions.
• Σ is a set of event names, associated with a labelling function Λ ∶ T → Σ.
• X = {x1 ,... ,xm } is a finite set of real-valued variables. The set Ẋ = {x˙1 ,... , x˙m } represents the first
derivatives of the elements in X . In addition, the set X ′ = {x′1 ,...,x′m } represents the updates of the
variables when a discrete transition takes place. In this section, we assume that discrete variables
are continuous variables whose derivative is zero at all locations.
• The functions Init, Inv and Flow assign predicates to each location loc ∈ Loc. Init(loc) establishes
the possible initial values for the continuous variables at location loc. Inv(loc) constrains the
values of the continuous variables at location loc. Flow(loc) contains the differential equations
describing the evolution of the continuous variables at location loc.

Adalid, Gallardo & Titolo

5
T ≥ 26

T = 26

Ṫ = −0.5
on

T ≤ 30
Ṫ = +2.0

T = 30

off

Figure 2: Hybrid automaton for the cooler system
• Function Jump assigns to each discrete transition t ∈ T a guard that must be satisfied in order to
allow the transition to take place, and a reset predicate which updates the value and/or the flow of
a continuous variables.
E XAMPLE 2.3 Figure 2 shows a hybrid automaton modeling a cooler system. The automaton has two
locations on and off and a continuous variable T storing the room temperature. When the automaton is
at location on (the cooler is turned on) the temperature decreases at rate −0.5. When the location is off
(the cooler is turned off) the temperature increases at rate +2.0. Transitions between locations represent
the turning on or off of the cooler. These transitions are guarded with conditions. For instance, transition
on-off takes place when the temperature is 26, while transition off -on takes place when the temperature
is 30.
A hybrid automaton behaves like a timed transition system (TTS), where each step is labelled either
with a positive real value τ (continuous transition of duration τ ) or with σ (discrete transition). Let
[X → R] be the set of maps from X to R. An automaton state, called hybrid state from now on, is a pair
(loc,v) ∈ (Loc × [X → R]), where loc ∈ Loc is a location of the automaton, and v ∈ [X → R] maps each
continuous variable to its current value.
Let p be a predicate over X ∪ Ẋ or X ∪ X ′ , then ⟦p⟧ denotes all functions v ∈ [X → R] that satisfy p.
D EFINITION 2.4 (T RAJECTORIES ) Let H = ⟨Loc, T, Σ, X , Init, Inv, Flow,Jump⟩ be a hybrid automaton. We consider two types of transitions:
Discrete transitions Let (loc,loc′ ) ∈ T , (loc,v) →σ (loc′ ,v′ ), iff v,v′ ∈ [X → R], and (v,v′ ) ∈ ⟦Jump(t)⟧.
Continuous transitions For each τ ∈ R+ , we have (loc,v) →τ (loc,v′ ) iff there exists a differentiable
function f ∶ [0, τ ] → Rm , f˙ ∶ [0, τ ] → Rm being its first derivative, such that:
• f (0) = v
• f (τ ) = v′
• ∀τ ′ ∈ [0, τ ], f (τ ′ ) ∈ ⟦Inv(loc)⟧
• ( f (τ ′ ), f˙(τ ′ )) ∈ ⟦Flow(loc)⟧
A trajectory is a (possible infinite) sequence of hybrid states such as (loc0 ,v0 ) →λ1 (loc1 ,v1 ) →λ2
... →λn (locn ,vn ) →λn ... , where for all i ≥ 0, vi ∈ ⟦Inv(loci )⟧ and λi ∈ R ∪ {σ }.
It is worth noting that the system is free to select non-deterministically at each moment any enabled
transition, either discrete or continuous.
E XAMPLE 2.5 Considering the hybrid system in Figure 2, the following trajectory represents a possible evolution of the automaton starting at hybrid state (on,27): (on,27) →1 (on,26.5) →1 (on,26) →σ
(off ,26) →0.5 (off ,27) →1.5 (off ,30) →σ (on,30)...

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

6

3

Hy-tccp:

an extension of tccp over continuous time

In this section, we present the language Hy-tccp, which subsumes tccp and includes new agents in order
to model the continuous behavior typical of hybrid systems in the style of hybrid automata. In contrast
to tccp, in Hy-tccp we consider a notion of continuous time by means of a global continuous clock.
H y-tccp uses a tccp monotonic store (called discrete store) to model the information about the current
location and the associated invariants of a hybrid automaton. Discrete transitions are modeled as instantaneous transitions in Hy-tccp and they are used to synchronize parallel agents/automata. In summary,
the features offered by tccp are used to model the discrete behavior of hybrid automata. However, hybrid automata are characterized by the use of continuous variables whose values change following some
ODEs. For this reason, the tccp store is extended by adding a component called continuous store. The
continuous store is not monotonic, instead it records the dynamical evolution of the continuous variables.
We distinguish the set of discrete variables Var, whose information is accumulated monotonically,
̃ whose values change continuously over time (Var ∩ Var
̃ = ∅).
and the set of continuous variables Var,
̃
Constraints in C are now defined over Var ∪ Var.
A continuous store is a function that associates a continuous variable with two real numbers: its value
and its flow, which indicates how its value changes over time. In this work, we consider only ODEs of
the form ẋ = n with n ∈ R. In the future, we intend to also consider ODEs of the form ẋ ∈ [n1 ,n2 ] with
n1 ,n2 ∈ R in order to model rectangular hybrid systems.
̃ the
̃ ↪ (R × R)] the set of all possible continuous stores, and as t̃
We denote as C˜ = [Var
rue and false
̃ the domain of c̃.
empty and the inconsistent continuous store, respectively. We denote with dom(c̃) ⊆ Var
˜
Given c̃ ∈ C and x ∈ dom(c̃), c̃(x) = ⟨v, f ⟩ means that x has value v (denoted as c̃(x).v) and flow f (denoted
as c̃(x). f ). The binary operator ∧˜ ∶ C˜ × C˜ → C˜ merges the information from two continuous stores. In the
case the same variable appears in both stores with different values or flows, their merge is inconsistent.
˜
Given c̃, d˜ ∈ C:
̃ = false
̃
c̃ ∧˜ t̃
rue = c̃ c̃ ∧˜ false
̃ if ∃x ∈ dom(c̃) ∩ dom(d).
˜ c̃(x) ≠ d(x)
˜
c̃ ∧˜ d˜ = false
⎧
⎪
⎪c̃(y) if y ∈ dom(c̃)
˜ c̃(x) = d(x)
˜
if ∀x ∈ dom(c̃) ∩ dom(d).
c̃ ∧˜ d˜ = λ y. ⎨
˜
˜
⎪
d(y)
if
y
∈
dom(
d)
⎪
⎩
̃ ∃˜ x c̃ deletes the information about
We define the operator ∃˜ ∶ Var × C̃ → C˜ such that, given c̃ ∈ C˜ and x ∈ Var,
x in c̃.
˜ x ∈ dom(c̃) and v ∈ R, we denote as c̃[v/x] the continuous store that is equal to c̃ except
Given c̃ ∈ C,
for the value of x that becomes v.
⎧
⎪
⎪c̃(y) if y ∈ dom(c̃),y ≠ x
c̃[v/x] = λ y. ⎨
⎪
⎪
⎩(v, c̃(x). f ) if y = x
A Hy-tccp store is a pair ⟨c, c̃⟩ where c ∈ C (discrete store) is a monotonic constraint store as in tccp
and c̃ ∈ C˜ (continuous store) is such that c ∧ ⋀x∈dom(c̃) (x = c̃(x).v) ≠ false, i.e., discrete and continuous
store are consistent1 . We denote as Γ the set of all possible Hy-tccp stores. We define the extension of
˜ if
the entailment relation ⊢ over Hy-tccp stores as ⊢˜ ∶ Γ × C such that given ⟨c, c̃⟩ ∈ Γ and d ∈ C, ⟨c, c̃⟩⊢d
c ∧ ⋀x∈dom(c̃) (x = c̃(x).v) ⊢ d. In other words, a store ⟨c, c̃⟩ entails a constraint d if the discrete store c
1

We assume that our underlying constraint system handles equality constraints.

Adalid, Gallardo & Titolo

7

merged with the projection of the current values of the continuous variables entails d in the underlying
constraint system.
Given τ ∈ R+ we denote as ⟨c, c̃τ ⟩ the continuous projection of the store ⟨c, c̃⟩ at time τ : the values of
the continuous variables are updated at time τ , while the flows are unchanged: c̃τ = λ y. c̃[ny /y] where y ∈
dom(c̃) and ny = c̃(y).v + (c̃(y). f ∗ τ ). For instance consider the store ⟨x > 10, y ↦ (2,5)⟩, its projection
at time 3 is the store ⟨x > 10, y ↦ (17,5)⟩. We say that ⟨c, c̃τ ⟩ is a continuous projection of ⟨c, c̃⟩ at time
˜
For instance, the above
τ that satisfies d (denoted as ⟨c, c̃⟩ ↝τd ⟨c, c̃τ ⟩) if for all τ ′ ∈ [0, τ ] ⟨c, c̃τ ′ ⟩⊢d.
y>0
projection satisfies y > 0: ⟨x > 10, y ↦ (2,5)⟩ ↝3 ⟨x > 10, y ↦ (17,5)⟩.
˜ = {x1 ,...,xn }, updates c̃ with the
The update operator ⊲, given c̃, d˜ ∈ C˜ such that dom(c̃) ∩ dom(d)
information of d˜ as follows: c̃ ⊲ d˜ ∶= (∃˜ x1 ,...,xn c̃) ∧˜ d.˜ Note that it is impossible to obtain an inconsistent
continuous store since the common variables are hidden from c̃ and replaced by the new values and flows
from d.˜
In order to model the typical behaviors of hybrid systems we introduce two new constructs w.r.t. the
̃
syntax of tccp: change and ask.
The agent change updates the current continuous store with a new value and/or flow for a given
continuous variable. It roughly corresponds to the reset predicate of hybrid automata.
̃
Continuous transitions are modeled by the new construct ask(inv)
that makes continuous variables
evolve over continuous time while the invariant inv is satisfied. The tccp choice agent is extended by
allowing the non-deterministic choice between discrete and continuous transitions in the following way:
̃
∑ni=1 ask(ci ) → A + ∑mj=1 ask(inv
j ).
̃ branches can be non-deterministically selected when the corresponding invariant inv j
Here, the ask
is entailed in the current store. The continuous variables evolve over time while inv j holds and until
another ask branch is selected.
The syntax of Hy-tccp agents is given by the following grammar:
A ∶∶= stop ∣ tell(c) ∣ A ∥ A ∣ now c then A else A ∣ ∃x A ∣ p(⃗
x) ∣
̃
change(y,v, f ) ∣ ∑n ask(ci ) → A + ∑m ask(inv
j)
i=1

j=1

̃ v, f ∈ R, p is a process
where c, ci and inv j are finite constraints in C, y is a continuous variable in Var,
̃
̃
̃
symbol, x ∈ Var ∪ Var, x⃗ ∈ (Var ∪ Var) × ⋅⋅⋅ × (Var ∪ Var), n ≥ 0 and m ≥ 0.
̃ ,→σ ,→τ ). ConThe operational semantics of Hy-tccp is described by a transition system T = (Conf
̃
figurations in Conf are triples ⟨A, c, c̃⟩ representing the agent A to be executed in the current extended
̃ × Conf
̃ does not
store ⟨c, c̃⟩. In contrast to the tccp approach, the discrete transition relation →σ ⊆ Conf
represent the passage of one time unit. Instead, it models a computational step which does not consume
time but it is needed to synchronize the agents in parallel. The continuous passage of time is modeled
̃ × Conf
̃ where τ ∈ R+ is a (strictly) positive real number that indicates
by the transition relation →τ ⊆ Conf
the duration of the transition. In Figure 3, we formally describe the operational semantics of Hy-tccp.
Wherever possible we will use the subindex λ ∈ R+ ∪ {σ } to represent both kinds of transitions (discrete
and continuous).
Rule R1 shows the effects of adding a constraint c ∈ C to the current discrete store. In Rule R1’, the
agent change updates the continuous store d˜ with a new initial value v and a new flow f for the variable
y by using the update operator ⊲.
Rules R2 and R2’ describe the non-deterministic choice behavior. Rule R2 represents the discrete
transition that is performed when one of the ask guards is entailed in the current store. In this case the

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

8

corresponding agent is executed in the next step. Rule R2’ models the continuous evolution of the system
̃ invariants holds in the store. After a continuous transition of duration τ , the values
while one of the ask
of the variables in the continuous store d˜ are updated while the discrete store is unchanged. At the end
of that transition the non-deterministic choice is executed again allowing another discrete or continuous
branch to be selected. In the case no guard or invariant holds this agent suspends.
Rules R3, R3’, R4 and R4’ describe the behavior of agent now. This agent behaves as A if c is
entailed by the constraint store, otherwise it behaves as B.
Rule R5 represents the parallel execution of two discrete transitions in terms of maximal parallelism,
i.e., all the enabled agents of A and B are executed at the same time. Rule R6 represents the parallel
execution of two continuous transitions, note that their duration must coincide. Rule R7 expresses the
parallel composition of a discrete and a continuous transition. In this case, the discrete transition is
executed before the continuous one. Rule R8 states that when an agent is blocked, the other one performs
its transition (discrete or continuous).
˜
In Rule R9, the agent ∃⟨l, l⟩ xA makes variable x local to A. It behaves like A with x considered local,
i.e., the information on x provided by the external environment is hidden from A by using the ∃˜ operator,
and, in the same way, the information on x produced by A is hidden from the global environment. The
˜ in the agent ∃⟨l, l⟩˜ x A represents the store local to A. This auxiliary operator is linked to the
store ⟨l, l⟩
rue⟩
hiding construct by setting the initial local store to ⟨true, t̃
rue⟩, thus ∃x A ∶= ∃⟨true, t̃
xA.
Finally, in Rule R10, the agent p(⃗
x) takes from D a declaration of the form p(⃗
x) ∶− A and executes
A.
Let us formalize the notion of behavior of a Hy-tccp program P in terms of the transition system
described in Figure 3. The small-step operational behavior of Hy-tccp collects all the small-step computations associated with P (in terms of sequences of Hy-tccp stores closed by prefix) for each possible
initial store. We assume that subsequent continuous transitions are considered as a unique (maximal) one
whose length is equal to the sum of all the subsequent transition lengths. For instance, a sequence of continuous transitions of the form ⟨A0 , c0 , c̃0 ⟩ →τ1 ... →τn ⟨An , cn , c̃n ⟩ is considered as the unique transition
⟨A0 , c0 , c̃0 ⟩ →τ ⟨An , cn , c̃n ⟩ where τ = ∑ni=1 τi 2 .
D EFINITION 3.1 Let P = D .A be a
defined as:
B ss ⟦D .A⟧ ∶=

⋃
⟨c0 , c̃0 ⟩∈Γ

H y-tccp

program. The small-step (observable) behavior of P is

{⟨c0 , c̃0 ⟩ ⋅ ⟨c1 , c̃1 ⟩ ⋅ ... ⋅ ⟨cn , c̃n ⟩ ∣ ⟨A, c0 , c̃0 ⟩ →λ1 ⟨A1 , c1 , c̃1 ⟩

→λ2 ... →λn ⟨An , cn , c̃n ⟩, ∀1 ≤ i ≤ n. λn ∈ R+ ∪ {σ }} ∪ {ε }

4

Examples

In order to show the expressivity of Hy-tccp, we present some examples of hybrid systems described in
this language. For each case, we present the Hy-tccp code and the corresponding hybrid automaton.

4.1 Cooler system
In Figure 4 we model in Hy-tccp the cooler system introduced in Example 2.5. The initial state of
the cooler is set to off and the temperature T initially has value 29 and changes with a rate of +2.0. The
̃ until the temperature is lower than or equal
temperature value increases continuously over time (first ask)
2

We assume that our system does not exhibit Zeno behaviors.

Adalid, Gallardo & Titolo

9

˜ →σ ⟨stop, c ∧ d, d⟩
˜
⟨tell(c), d, d⟩
˜ →σ ⟨stop, d, d˜ ⊲ (y ↦ (v, f ))⟩
⟨change(y,v, f ), d, d⟩
˜ ⊢c
˜ k
∃1 ≤ k ≤ n.⟨d, d⟩
m ̃
n
˜ →σ ⟨Ak , d, d⟩
˜
⟨∑ ask(ci ) → Ai + ∑ ask(inv j ), d, d⟩
i=1

(R1)
(R1’)
(R2)

j=1

k
˜ ↝inv
˜
∃1 ≤ k ≤ m, τ ∈ R+ .⟨d, d⟩
τ ⟨d, dτ ⟩
m ̃
n
n
̃
˜ →τ ⟨∑i=1 ask(ci ) → Ai + ∑mj=1 ask(inv
˜
⟨∑i=1 ask(ci ) → Ai + ∑ j=1 ask(inv j ), d, d⟩
j ), d, dτ ⟩

˜ ⊢c
˜ →λ ⟨A′ , d ′ , d˜′ ⟩ λ ∈ R+ ∪ {σ } ⟨d, d⟩
˜
⟨A, d, d⟩
˜ →λ ⟨A′ , d ′ , d˜′ ⟩
⟨now c then A else B, d, d⟩
˜ →
˜ ⊢c
˜
⟨A, d, d⟩
/ λ λ ∈ R+ ∪ {σ } ⟨d, d⟩
˜
˜
⟨now c then A else B, d, d⟩ →σ ⟨A, d, d⟩
˜ →λ ⟨B′ , d ′ , d˜′ ⟩ λ ∈ R ∪ {σ } ⟨d, d⟩
˜ ⊬c
˜
⟨B, d, d⟩
˜ →λ ⟨B′ , d ′ , d˜′ ⟩
⟨now c then A else B, d, d⟩
˜ →
˜ ⊬c
˜
⟨B, d, d⟩
/ λ λ ∈ R ∪ {σ } ⟨d, d⟩
˜
˜
⟨now c then A else B, d, d⟩ →σ ⟨B, d, d⟩
˜ →σ ⟨A′ , d ′ , d˜′ ⟩ ⟨B, d, d⟩
˜ →σ ⟨B′ , d ′′ , d˜′′ ⟩
⟨A, d, d⟩
˜ →σ ⟨A′ ∥ B′ , d ′ ∧ d ′′ , d˜′ ∧˜ d˜′′ ⟩
⟨A ∥ B, d, d⟩
˜ →τ ⟨B, d, d˜′ ⟩ τ ∈ R+
˜ →τ ⟨A, d, d˜′ ⟩ ⟨B, d, d⟩
⟨A, d, d⟩
˜ →τ ⟨A ∥ B, d, d˜′ ⟩
⟨A ∥ B, d, d⟩
˜ →σ ⟨A′ , d ′ , d˜′ ⟩ ⟨B, d, d⟩
˜ →τ ⟨B, d, d˜′′ ⟩ τ ∈ R+
⟨A, d, d⟩
˜ →σ ⟨A′ ∥ B, d ′ , d˜′ ⟩
⟨A ∥ B, d, d⟩
˜ →λ ⟨A′ , d ′ , d˜′ ⟩ ⟨B, d, d⟩
˜ →
⟨A, d, d⟩
/ λ ′ λ , λ ′ ∈ R+ ∪ {σ }
˜ →λ ⟨A′ ∥ B, d ′ , d˜′ ⟩
⟨A ∥ B, d, d⟩
˜
⟨B ∥ A, d, d⟩ →λ ⟨B ∥ A′ , d ′ , d˜′ ⟩
˜ →λ ⟨B, l ′ , l˜′ ⟩ λ ∈ R+ ∪ {σ }
⟨A, l ∧ ∃x d, l˜∧˜ ∃˜ x d⟩
˜ →λ ⟨∃⟨l′ , l˜′ ⟩ x B, d ∧ ∃x l ′ , d˜ ∧˜ ∃˜ x l˜′ ⟩
⟨∃⟨l, l⟩˜ x A, d, d⟩
p(⃗
x) ∶− A ∈ D
˜ →σ ⟨A, d, d⟩
˜
⟨p(⃗
x), d, d⟩

Figure 3: The transition system for Hy-tccp.

(R2’)
(R3)
(R3’)
(R4)
(R4’)
(R5)
(R6)
(R7)
(R8)

(R9)
(R10)

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

10

init ∶− ∃ St,T ( tell(St = [off ∣ ]) ∥ change(T,29,+2.0) ∥ tell(T ≥ 26 ∧ T ≤ 30) ∥ cooler(St,T ))
̃
cooler(St,T ) ∶− ∃ St ′ ( ask(St
= [off ∣ ] ∧ T ≤ 30)
+ ask(St = [off ∣ ] ∧ T = 30) → (tell(St = [off ∣ St ′ ]) ∥ tell(St ′ = [on ∣ ]) ∥ change(T,30,−0.5) ∥ cooler(St ′ ,T ))

̃
+ ask(St
= [on ∣ ] ∧ T ≥ 26)

+ ask(St = [on∣ ] ∧ T = 26) → (tell(St = [on ∣ St ′ ]) ∥ tell(St ′ = [off ∣ ]) ∥ change(T,26,+2.0) ∥ cooler(St ′ ,T )))

Figure 4: Hy-tccp model for the cooler system
to the value of 30. When the temperature reaches this limit, the cooler is turned on and the flow of the
temperature changes from +2.0 to −0.5 (first ask). At this point, the temperature starts decreasing until
̃ When this happens, the cooler is turned off and the flow of the
it reaches the value of 26 (second ask).
temperature is changed again to +2.0 (second ask).
It is worth noting that, due to the monotonicity of the discrete constraint store, streams (written
in a list-fashion way) are used to model imperative-style variables [2]. A stream is a list of the form
St = [on ∣ St′ ] where the head on represents the current value of St, and the tail St′ is a free variable that
will be instantiated with the future values of St. Observe that we use the global constraint T ≥ 26∧ T ≤ 30
to add a global invariant of the cooler system ensuring that the temperature always stays in the interval
[26,30].
The following partial trace represents the small-step behavior (see Definition 3.1) of cooler(St,T )
starting from the initial store ⟨St = [off ∣ ]∧T ≥ 26∧T ≤ 30, T ↦ (29,+2.0)⟩. This means that, initially, the
cooler is turned off and the temperature has a value of 29 and a flow of +2.0. Moreover, the temperature
is constrained to be between the values 26 and 30. Observe how the values on and off are accumulated
in the stream St in order to model the evolution of the state. The current state corresponds to the last
value added to the stream. We use to indicate that the tail of the stream St is a free variable that can be
instantiated with future values. The continuous variables evolve over time until another discrete transition
is executed. The repeated equal stores occurring in the trace correspond to the discrete computational
steps taken in Hy-tccp (as well as in tccp) to evaluate one of the ask guards or to perform a procedure
call. These steps are necessary to synchronize parallel agents. For sake of clarity, we explicitly indicate
the kind of transition occurring between two states (we write σ for discrete transitions and the duration
τ ∈ R+ for continuous ones).
⟨St = [off ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (29, +2.0)⟩ ⋅0.5 ⟨St = [off ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (30, +2.0)⟩⋅σ
⟨St = [off ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (30, +2.0)⟩ ⋅σ ⟨St = [off , on ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (30, −0.5)⟩⋅σ
⟨St = [off , on ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (30, −0.5)⟩ ⋅8 ⟨St = [off , on ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (26, −0.5)⟩⋅σ
⟨St = [off , on ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (26, −0.5)⟩ ⋅σ ⟨St = [off , on, off ∣ ] ∧ T ≥ 26 ∧ T ≤ 30, T ↦ (26, +2.0)⟩ . . .

4.2 Cat and mouse race
We consider the cat and mouse problem proposed in [7] (see Figure 5 for the corresponding hybrid
automaton). The Hy-tccp code of this model is shown in Figure 6. The positions of the cat and the mouse
are modeled by two continuous variables, called C and M respectively. A mouse starts running from the
point of origin at a speed of 10 meters/second (change(M,0,10.0)) towards a hole that is 100 meters

Adalid, Gallardo & Titolo

11

C ≤ 100
go

Ċ = 0.0

Ċ = 20.0

sleeping

chasing

true

Ċ = 0.0

Ṁ = 0.0

loser

winC
true

true

M ≤ 50

true
C = 100 ∣ endC

M ≤ 100
M = 50 ∣ go

Ċ = 0.0
finished

winner

winM

Ṁ = 10.0

Ṁ = 10.0

1st half

2nd half

winM

true
M = 100 ∣ endM

Ṁ = 0.0
finished

winC

true

true

Ċ = 0.0

Ṁ = 0.0

winner

loser

Figure 5: Hybrid automata for the cat and mouse problem
init ∶− mouse ∥ cat ∥ controller
mouse ∶− ∃M (change(M,0,10.0) ∥
̃
( ask(M
≤ 50)

̃
+ ask(M = 50) → (tell(go) ∥ (ask(M
≤ 100)

+ ask(M = 100) → (tell(endm ) ∥ ask(winm ) → claimPrize(...)
+ ask(winc ) → stop)))))

cat ∶− ∃C ( ask(go) → (change(C,0,20.0) ∥
̃ ≤ 100)
( ask(C

+ ask(C = 100) → (tell(endc ) ∥ ask(winc ) → claimPrize(...)
+ ask(winm ) → stop))))

controller ∶− ask(endm ) → tell(winm ) + ask(endc ) → tell(winc )

Figure 6: Hy-tccp model for the cat and mouse race
away. After it has run 50 meters it sends a signal to the cat (tell(go)) and continues its run. When the cat
receives the signal go, it starts chasing the mouse from the point of origin at a speed of 20 meters/second
(change(C,0,20.0)). The cat wins if it catches the mouse before it reaches the hole, otherwise it loses.
At the end of their run, the mouse and the cat send a message to the controller (endM and endC ,
respectively), which decides non-deterministically the winner and informs of it through a signal (winm
or winc ). The winner, at this point, can claim his prize.

4.3 Gear shift system
The hybrid automaton in Figure 7 represents a car gear shift system. Each location models a gear (1, 2
or 3) and the fact that the speed is either increasing or decreasing (↑ or ↓ respectively). When the speed
increases (respectively decreases) over time and it reaches a given threshold, the current gear is changed
to the upper (respectively lower) one. When a signal of danger (dng) is received, the system changes
the current gear to the lower one and the speed starts decreasing. At this point, when a signal of safe
situation (safe) is received, the system is allowed to stay in the current location as well as to increase the

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

12

V ≤ 60 ∧ ¬dng

V ≤ 20
V̇ = +4.0

V = 20

1↑
V ≤ 20 ∧ safe

1↓

V = 60

2↑

dng

V ≥0
V̇ = −4.0

V̇ = +5.0

V ≤ 100 ∧ ¬dng

V ≤ 60 ∧ safe

V̇ = +6.0
3↑

dng

V ≥ 20

V = 20

V̇ = −5.0
2↓

Figure 7: Hybrid automaton for the gear shift system
speed. The latter case is modeled by the transitions from location 1 ↓ to location 1 ↑, and from 2 ↓ to 2 ↑.
The Hy-tccp program modeling this system is shown in Figure 8. The stream G stores the evolution
̃ statements model the five locations of the automaton of Figure 7, i.e., the
of the gear state. The ask
possible cases in which a continuous transition is performed. It is worth noting that the invariant of
̃ statement. The first three ask statements
each location is modeled by the guard of the corresponding ask
model the gearbox shifting automatically into a higher (respectively lower) gear if the speed V reaches
the upper (respectively lower) threshold of the current gear. The watcher informs to the gearbox about
the current external situation (danger or safe), through channel WG. When gearbox receives a danger
signal dng and the speed is growing (fourth and fifth ask branches), it moves to a lower gear, and changes
the speed flow from positive to negative by means of a change agent. Otherwise, when it receives a safety
signal safe and the speed is decreasing (sixth and seventh ask branches), it is allowed to change the speed
flow from negative to positive.

5

Related Work

In [7], hcc was introduced as the first extension over continuous time of the concurrent constraint
paradigm. Although both Hy-tccp and hcc are declarative languages with a logical nature, there are
some important differences between them. First of all, Hy-tccp is a non-deterministic language, while
hcc is deterministic. We believe that this is an essential feature for modeling hybrid systems, which are
inherently non-deterministic. Hy-tccp has been defined as a modeling language for hybrid systems in
the style of hybrid automata. This means that we aim to obtain programs with a structure similar to that
of hybrid automata, but described in a more abstract way. The non-deterministic choice is a powerful
construct that allows the set of all possible transitions of an hybrid automata to be expressed as a list of
̃ branches. Furthermore, in hcc, the information on the value and flow of continuous variables
ask and ask
is modeled as a constraint of the underlying continuous constraint system. On the contrary, in Hy-tccp,

Adalid, Gallardo & Titolo

13

init ∶− ∃ V,G,WG( tell(G = [1 ↑∣ ]) ∥ change(V,0,+4.0) ∥ tell(V ≥ 0 ∧V ≤ 100) ∥ gearbox(G,WG,V) ∥ watcher(WG))
gearbox(G,WG,V) ∶− ∃ G′ ,WG′ (
̃
̃
̃
= [2 ↑∣ ] ∧V ≤ 60 ∧ WG ≠ [dng ∣ ]) + ask(G
= [3 ↑∣ ] ∧V ≤ 100 ∧ WG ≠ [dng ∣ ])
ask(G
= [1 ↑∣ ] ∧V ≤ 20) + ask(G

̃
̃
= [2 ↓∣ ] ∧V ≥ 20)
+ ask(G
= [1 ↓∣ ] ∧V ≥ 0) + ask(G

+ ask(G = [1 ↑∣ ] ∧V = 20) → ( tell(G = [1 ↑∣ G′ ]) ∥ tell(G′ = [2 ↑∣ ]) ∥ change(V, ,+5.0) ∥ gearbox(G′ ,WG,V))
+ ask(G = [2 ↑∣ ] ∧V = 60) → ( tell(G = [2 ↑∣ G′ ]) ∥ tell(G′ = [3 ↑∣ ]) ∥ change(V, ,+6.0) ∥ gearbox(G′ ,WG,V))
+ ask(G = [2 ↓∣ ] ∧ V = 20) → ( tell(G = [2 ↓∣ G′ ]) ∥ tell(G′ = [1 ↓∣ ]) ∥ change(V, ,−4.0) ∥ gearbox(G′ ,WG,V))
+ ask(G = [2 ↑∣ ] ∧ WG = [dng ∣ ]) → ( tell(G = [2 ↑∣ G′ ]) ∥ tell(G′ = [1 ↓∣ ]) ∥ tell(WG = [dng ∣ WG′ ]) ∥
change(V, ,−4.0) ∥ gearbox(G′ ,WG′ ,V))
+ ask(G = [3 ↑∣ ] ∧ WG = [dng ∣ ]) → ( tell(G = [3 ↑∣ G′ ]) ∥ tell(G′ = [2 ↓∣ ]) ∥ tell(WG = [dng ∣ WG′ ]) ∥
change(V, ,−5.0) ∥ gearbox(G′ ,WG′ ,V))
+ ask(G = [1 ↓∣ ] ∧ WG = [safe ∣ ] ∧V ≤ 20) → ( tell(G = [1 ↓∣ G′ ]) ∥ tell(G′ = [1 ↑∣ ]) ∥ tell(WG = [safe ∣ WG′ ]) ∥
change(V, ,+4.0) ∥ gearbox(G′ ,WG′ ,V))
+ ask(G = [2 ↓∣ ] ∧ WG = [safe ∣ ] ∧V ≤ 60) → ( tell(G = [2 ↓∣ G′ ]) ∥ tell(G′ = [2 ↑∣ ]) ∥ tell(WG = [safe ∣ WG′ ]) ∥
change(V, ,+5.0) ∥ gearbox(G′ ,WG′ ,V)))
̃
watcher(WG) ∶− ∃ WG′ ( ask(true)
+ ask(true) → (tell(WG=[safe ∣ WG′ ]) ∥ watcher(WG′ ))
+ ask(true) → (tell(WG=[dng ∣ WG′ ]) ∥ watcher(WG′ )))

Figure 8: Hy-tccp model for a gear shift system

Modeling Hybrid Systems in the Concurrent Constraint Paradigm

14

there is a clear distinction between discrete and continuous variables. In hcc the positive information in
the store must be transferred by using the agent hence. In contrast, in Hy-tccp the positive information
in the discrete store is transferred automatically from one step to the next.
In [1] and [4], two process algebras for hybrid systems have been defined: Hybrid Chi and HyPa,
respectively. The process algebra Hybrid Chi [1] shares with Hy-tccp the separation between discrete
and continuous variables, the synchronous nature and the concept of delayable guard (corresponding
to the suspension of the non-deterministic choice). HyPa [4] was introduced as an extension of the
process algebra ACP. It differs from Hybrid Chi mainly in the way time-determinism is treated, and in
the modeling of time passing.

6

Conclusions

In this paper we have presented Hy-tccp, an extension of tccp over continuous time with the aim of
modeling hybrid systems in a declarative and logical way by abstracting away from all the implementation details. Hy-tccp has been introduced as a synchronous and non-deterministic language defining
computations similar to that of hybrid automata.
H y-tccp has several advantages that make it suitable for modeling hybrid systems. Its declarative
nature facilitates a high level description close to that of hybrid automata. In addition, the logical nature
of Hy-tccp eases the development of formal methods techniques for the static analysis and verification of
hybrid systems. Furthermore, since Hy-tccp is a conservative extension of tccp, it is possible to describe
with the same syntax concurrent, reactive and hybrid systems.
In the future, we plan to develop a framework for the description and simulation of Hy-tccp programs.
In this way, we will be able to model complex hybrid systems in Hy-tccp. Given the affinity of the two
formalisms, we are interested in defining a translation rules system from Hy-tccp to hybrid automata
and viceversa, in order to transfer verification and analysis results from one formalism to the other.
Furthermore, we plan to use model checking and abstract interpretation techniques to verify temporal
properties of hybrid systems written in Hy-tccp (as done in [6] for SPIN and in [3] for tccp). Another
feature we would like to explore is the adjustment of the language to make it compatible with rectangular
hybrid automata [9].

References
[1] D. A. van Beek, K. L. Man, M. A. Reniers, J. E. Rooda & R. R. H. Schiffelers (2006): Syntax and consistent
equation semantics of hybrid Chi. Journal of Logic and Algebraic Programming 68(1-2), pp. 129–210,
doi:10.1016/j.jlap.2005.10.005.
[2] F. S. de Boer, M. Gabbrielli & M. C. Meo (2000): A Timed Concurrent Constraint Language. Information
and Computation 161(1), pp. 45–83, doi:10.1006/inco.1999.2879.
[3] M. Comini, L. Titolo & A. Villanueva (2014): Abstract Diagnosis for tccp using a Linear Temporal Logic.
Theory and Practice of Logic Prog. 14(4-5), pp. 787–801, doi:10.1017/S1471068414000349.
[4] P. J. L. Cuijpers & M. A. Reniers (2005): Hybrid process algebra. Journal of Logic and Algebraic Programming 62(2), pp. 191–245, doi:10.1016/j.jlap.2004.02.001.
[5] C. Daws & S. Yovine (1995): Two Examples of Verification of Multirate Timed Automata with Kronos.
In: Proceedings of the 16th IEEE Real-Time Systems Symposium, RTSS ’95, IEEE Computer Society,
Washington, DC, USA, pp. 66–75, doi:10.1109/REAL.1995.495197.

Adalid, Gallardo & Titolo

15

[6] M. M. Gallardo & L. Panizo (2013): Extending Model Checkers for Hybrid System Verification: the case
study of SPIN. Software Testing, Verification and Reliability, doi:10.1002/stvr.1505.
[7] V. Gupta, R. Jagadeesan, V. A. Saraswat & D. G. Bobrow (1994): Programming in Hybrid Constraint Languages. In P.J. Antsaklis, W. Kohn, A. Nerode & S. Sastry, editors: Hybrid Systems II, Lecture Notes in
Computer Science 999, Springer, pp. 226–251, doi:10.1007/3-540-60472-3 12.
[8] T. A. Henzinger (1996): The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS ’96, IEEE Computer Society, Washington, DC, USA, pp.
278–292.
[9] P. W. Kopke (1996): The Theory of Rectangular Hybrid Automata. Technical Report, Ithaca, NY, USA.
[10] V. A. Saraswat (1989): Concurrent Constraint Programming Languages. Ph.D. thesis, Pittsburgh, PA, USA.

