=Paper=
{{Paper
|id=Vol-2745/paper3
|storemode=property
|title=Towards Plan Recognition in Hybrid Systems
|pdfUrl=https://ceur-ws.org/Vol-2745/paper3.pdf
|volume=Vol-2745
|authors=Diego Aineto,Eva Onaindia,Miquel Ramírez,Enrico Scala,Ivan Serina
|dblpUrl=https://dblp.org/rec/conf/aiia/AinetoORSS20
}}
==Towards Plan Recognition in Hybrid Systems==
https://ceur-ws.org/Vol-2745/paper3.pdf
Towards Plan Recognition in Hybrid Systems?
Diego Aineto1 , Eva Onaindia1 , Miquel Ramı́rez2 , Enrico Scala3 , Ivan Serina3
1
VRAIN, Universitat Politècnica de València
{dieaigar,onaindia}@upv.es
2
Univesity of Melbourne
miquel.ramirezunimelb.edu.au
3
Università degli Studi di Brescia, Italy
{enrico.scala,ivan.serina}@unibs.it
Abstract. Hybrid systems model software-based control systems to deal with
real-world applications that exhibit an interaction of discrete and continuous dy-
namic behaviour. Hybrid automata (HA) is a widely used formalism for model
checking of hybrid systems including reachability analysis, safety and stability
verification. Given a HA model and a set of state observations received at certain
times, we focus on determining if the HA accepts a trajectory that recognizes the
observations. We formulate this task as a planning problem encoded in PDDL+
and use a planner to find a hybrid plan that satisfies the observations while fol-
lowing the HA dynamics. Ultimately, we show the adequacy of PDDL+ to model
HAs with two well-known examples in the literature on HAs.
Introduction
Hybrid system exhibits a combination of a discrete and continuous behavior which
is characteristic of many software-based control systems. Discrete-time linear control
systems are widely used as the abstraction of choice for computer controlled physi-
cal systems. This paradigm models systems whose continuous dynamics are described
by a linear differential equation in combination with transforming measured physical
quantities into digital format to denote the logical modes of operation [12].
The first hybrid systems model the software as a finite-state machine that interacts
with the physical world through converters. This model later evolved into Hybrid Au-
tomata (HA). The HA paradigm builds upon the timed automata model that enables the
description of finitely many states where each state represents infinitely many states of
the timed automaton [2].
Hybrid systems arise in varied contexts such as manufacturing, automotive engine
control, traffic control, communication networks and computer synchronization among
others. Industrial applications usually require safety and stability properties and HAs
have been widely used as a modeling and verification framework for cyber-physical
systems [4].
In this work we present an approach to decide whether a hybrid system modeled
as an HA accepts a sequence of discrete-time state observations. That is, determine if
?
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons Li-
cense Attribution 4.0 International (CC BY 4.0).
the observed behaviour of a system is actually modeled by a given HA. In discrete en-
vironments modeled as finite-state machines, plan recognition is the task of predicting
the plan of an acting agent based on its observed actions [3, 7, 11]. We leverage the ad-
vances on plan recognition and posit our problem as an extension of existing techniques
to mixed discrete-continuous domains.
For our purposes, we use PDDL+, a powerful modelling language to express dis-
crete and continuous change. Planning in mixed discrete-continuous domains is a chal-
lenging problem and it has received increasing attention in the planning community
since it allows to model effectively real-world domains. In this paper, we present a
mapping scheme that transforms the elements of an HA into the constructs of PDDL+.
We also present an example of the transformation scheme to an scenario of a gas burner
modeled through an HA, and run the PDDL+ encoding with the planner ENHSP [9].
The results show the suitability of a planning-based approach for building hybrid tra-
jectories that comply with the state observations.
Background
This section describes background knowledge. The first section is devoted to present
the HA paradigm to model hybrid systems. The second section presents PDDL+, the
planning language we will use to modelling continuous change .
Hybrid automata
In general, the state of a hybrid system is defined by the values of its continuous vari-
ables and a discrete mode. The state changes either continuously, according to a flow
condition, or discretely according to a jumps which correspond to the change of state in
an automaton that transitions in response to external events or to the continuous evolu-
tion. Continuous flow is permitted as long as so-called invariants hold, while discrete
transitions can occur as soon as given jump conditions are satisfied or events occur.
A Hybrid automata (HA) defines trajectories (behaviours) of a hybrid system. It is
formally defined as a finite state machine with a finite set of continuous variables whose
values are described by a set of ordinary differential equations (ODEs). We adopt the
formulation of HA as defined in [5].
A HA with polynomial dynamics is a tuple H = hLoc, Lab, Edg, X, Init, Inv, Flow,
Jump, Finali where:
– Loc is a set of discrete variables also called locations of H
– Lab is a set of labels
– Edg is a set of edges to denote the discrete transitions
– X = {x1 , . . . , xn } a set of real-valued variables
– Init : Loc → PConstr(X) (polynomial constraints over X), states the possible
valuations of X when H starts from a location l
– Inv : Loc → PConstr(X) is the invariant of location l, which constrains the possi-
ble valuations of X when the S control of H is at l
– Flow : Loc → PConstr(X Ẋ) constrains the valuation evolution of X according
to the rate of change given by their time derivative Ẋ
– Jump : Edg → PConstr(X X + ) gives the jump condition of edge e and X +
S
represents updates at the conclusion of a discrete transition
– Final : Loc → PConstr(X) is the final condition of location l.
Depending on the analysis question at hand, final conditions can either specify the
unsafe states of the system or the desired states of the system [4].
The timed transition system defined by a hybrid automata H is a tuple JHK =
hS, S0 , Sf , Σ, →i. The set S = {(l, v)| l ∈ Loc, v ∈ JInv(l)K} is the state space of
H; S0 = {(l, v) ∈ S| v ∈SJInit(l)K} denotes the set of initial states (Sf is the set
v ∈ JFinal(l)K); Σ = Lab Time (Time ∈ R≥0 ) is a finite set of labels. Finally,
→∈ S × Σ × S is the transition relation; that is, tuples of the form (l, v) →σ (l0 , v 0 ),
σ ∈ Σ, such that every tuple belongs to one of the two following cases:
– discrete transition: e = (l, σ, l0 ) ∈ Edg, σ ∈ Lab, and (v, v 0 ) ∈ JJump(e)K
– continuous transition: σ ∈ Time, l = l0 , and there exists δ ∈ R≥0 and a contin-
uously differentiable function ξ : [0, δ] → RX such that ξ(0) = v, ξ(δ) = v 0 and
˙
∀t ∈ [0, δ], (ξ(t), ξ(t)) ∈ JFlow(l)K and ξ(t) ∈ JInv(l)K
This notion of hybrid system is a blend between the automata theoretic models used
for verification of software systems and the differential equations used in control [4].
The paths contained in the timed transition system of H describe in a precise manner
the possible trajectories of the hybrid system modeled by H.
We now show an example of the behaviour of the temperature in a room con-
trolled by an HA (thermostat) with two locations Loc = {lON , lOFF }, two labels Lab =
{ON, OFF}, and two edges that connect both locations and a variable x that represents
the room temperature [8]. Following Table 1, when the thermostat is on, the temperature
increases at a rate given by the differential equation ẋ = 5 − 0.1x; when the thermostat
is off the room cools down at a rate given by the differential equation ẋ = −0.1x. The
heater remains on while the temperature is ≤ 22 and it remains off while the tempera-
ture is ≥ 18. The thermostat turns on the heater when the temperature decreases below
19C and turns off the heater when the temperature increases above 21C. Initially, the
temperature of the room is 15C.
lON lOFF
Inv x ≤ 22 x ≥ 18
Flow ẋ = 5 − 0.1x ẋ = −0.1x
Edg lON →OFF lOFF lOFF →ON lON
Jump x ≥ 21 x ≤ 19
x0 = x x0 = x
Init x = 15 –
Table 1. Example of the behaviour of a thermostat for monitoring the temperature in a room
described as an HA
A hybrid trajectory that illustrates the evolution of the room temperature according
to the above HA is a sequence q0 σ0 q1 σ1 . . . σn−1 qn , where qi = (li , vi ), q0 ∈ S0 ,
q = qn , σi ∈ Σ and (qi , σi , qi+1 ) ∈→. For example, the following path is accepted
by the HA: hlON , 15i →1.9 hlON , 21.08i →OFF hlOFF , 21.08i →1.1 hlOFF , 18.88i →ON
hlON , 18.88i →0.8 hlON , 21.28i →OFF hlOFF , 21.28i →1.2 hlOFF , 18.86i.
Mixed Discrete-continuous Planning Domains in PDDL+
PDDL+ [6] (Planning Domain Definition Language) is the language of reference in the
planning community to represent problems containing a mixture of discrete and con-
tinuous variables together with changes that can be either continuous or instantaneous.
Continuous changes are caused by the execution of autonomous processes while instan-
taneous changes are caused by events or actions. While actions are what is in control
of the agents, PDDL+ processes and events describe what happens in the world when
some condition is met. Processes last for as long as their preconditions are met. A pro-
cess is something like gravity’s effect on an object which increases the velocity of the
object until it reaches the ground. Events correspond to an instantaneous transition that
happens the instant their preconditions are met, usually with the effect of transforming
their state such that their preconditions are no longer met. Events are uncontrollable,
and in the previous example, we might consider an event to be the object hitting the
ground when the position of the object reaches some value, e.g., x = 0.
A PDDL+ problem Π is formally defined by the tuple hX, F, A, P, E, I, Gi where:
– X is a set of numeric variables taking values from Q
– F is a set of Boolean variables
– A is a set of actions. Each a ∈ A is a pair hpre(a), eff(a)i where pre(a) is a
propositional formula containing both numeric and Boolean conditions. A numeric
condition is a comparison of the form ξ ≥ 0 with ξ being a numeric expressions
over X. A Boolean condition is either l = > or l = ⊥ where l ∈ F . ef f (a) is a
set of numeric and propositional assignments
– E is a set of events. An event is structured as an action
– P is a set of processes. A process p ∈ P , as an action and an event, is a pair
hpre(p), eff(p)i. While the preconditions of a process have the same structure of
those used for actions and events, the effect’s set only contain continuous effects. A
continuous effect is a time-dependent effect of the form ẋ = ξ where ξ is a function
representing the derivative of x
– I is an assignment of all variables in X and F , called the initial state
– G is the goal. Its structure is equivalent to that used for action, process and event
preconditions
A plan π for a planning instance Π is a finite set of pairs (t, a) ∈ Q × A, where
t is the timepoint at which a is executed. Each plan induces a continuous trajectory of
states that tells us the value of all the variables in X and F for each timepoint t0 . Such a
trajectory starts at the initial state and is determined by the processes and events that are
triggered spontaneously as time goes by, together with the changes prescribed by the
actions from the plan. Recall that both processes and events are compulsory executed
as their preconditions are met. When a process is triggered, a continuous update of the
numeric variables is triggered according to the prescribed derivatives. When an event
is triggered, the state instantaneously changes according to the event’s effects. It is
required that for each state, the triggered events are non-mutex, so as to avoid non-
determinism in how events are sequenced.
A plan π is said to be a solution for a problem Π if each action (t, a) ∈ π is such
that a is executable at time t provided the continuous trajectory induced by the triggered
events and processes from Π, and there is a tg ≥ 0 such that the state at that timepoint
satisfies the goal and there is no pair (tn , an ) in π such that tn > tg .
More details on the semantics of PDDL+ can be found into the paper by [6].
We consider for the scope of this paper a slightly variant of PDDL+. In such a vari-
ant we can also encode global constraints as those defined in [9, 10]. A global constraint
is a propositional formula as that used in action’s precondition. PDDL+ extended with
global constraints (hereinafter simply PDDL+) is formally the tuple hX, F, A, P, E, I,
G, Ci where all the elements but C are defined as above, whilst C is a set of global
constraints. A plan is a valid solution plan if it is a valid plan for the basic version of
PDDL+ and, in addition, the induced continuous trajectory also satisfies all constraints
from C for any timepoint up to the point in which the goal is satisfied.
Mapping HA to PDDL+
The theory of HA provides an ideal formal basis for the development of a semantics for
PDDL+. The work [6] uses the syntax of HAs as a semantic model to construct a formal
interpretation of PDDL+ semantics and builds a mapping from planning constructs to
constructs of the corresponding HA. In this work, we posit the reverse problem: building
a formal mapping of HA semantics into PDDL+ constructs.
Let be H = hLoc, Lab, Edg, X, Init, Inv, Flow, Jump, Finali a hybrid automata and
Π = hA, P, E, I, G, X, F, Ci a PDDL+ problem. A mapping between H and Π is
depicted below.
– The first observation is that Time and X of an HA are values in R whereas numeric
variables in Π (including time) are rational values (Q). This means PDDL+ plans
are restricted to expressing only a subset of the transitions possible in JHK, mainly
because planners can only make use of timestamps with a finite representation, so
there are only countably many plans that can be expressed [6]. Defining an addi-
tional metric in planning problems to specify the set of acceptable plans may be an
interesting research line to overcome this shortcoming.
– A location l ∈ Loc is simply represented with a Boolean variable of F to denote
whether or not the hybrid automata H is in location l.
– The set of actions A of Π are the constructs to encode the edges of H. Specifically,
given a ∈ A and e = (l, σ, l0 ) ∈ Edg:
• the action name is an item of Lab
• pre(a) encodes the guards (conditions) of Jump(e) and the condition that H is
in location l
• ef f (a) encodes the reset (updates) of Jump(e); additionally, the location of H
is updated to l0
The set A is the source of non-determinism in planning. In contrast, non-deterministic
HAs often appear when different locations partially share the invariants, or the
guards of an edge e = (l, σ, l0 ) partially overlap with JInv(l)K (in this latter case,
if overlapping occurs at only one point on the frontier of JInv(l)K, then the HA is
deterministic).
For many of the HA typically discussed in the literature, it commonly happens that
T edges of a location l, e1 = (l, σ1 , l1 ) and e2 = (l, σ2 , l2 ), it
for any pair of outgoing
holds JJump(e1 )K JJump(e2 )K = ∅. Particularly, given the following grammar
rule that defines a formula ϕ
ϕ ::= PTerm(X) 1 0|, 1∈ {<, ≤, =, ≥, >} (1)
, if we restrict PConstr(X) to a subset of PConstr(X) defined by conjunctive for-
mulas (ϕ ∧ ϕ), and there is no other source of non-determinism, we can then ensure
a deterministic discrete behaviour of the HA. In this case, the edges of a location
can be represented with PDDL+ events (E ∈ Π) instead of actions, thus reducing
the branching factor of the search.
– It must hold I ∈ Init(l) for some l of H. This means the assignments of the numeric
variables X of Π in the initial state must hold in some state s ∈ S0 . Additionally,
a Boolean variable of F is used to represent that H is initially at l.
– It must hold G ∈ Final(l) for some l of H. This means the assignments of the
numeric variables that appear in G must hold in some state s ∈ Sf . Additionally, a
Boolean variable of F is used to represent that H is finally at location l.
– Invariants of a location are represented with PDDL+ constraints (C ∈ Π), encod-
ing an implication of the form if Loc = l then Inv(l). Specifically, given a valua-
tion for X ∈ H, the constraints of PDDL+ verify that ∀x ∈ X, v(x) ∈ JInv(l)K.
This effectively constraints any continuous trajectory of a solution plan for Π to
comply with the invariant conditions of the hybrid automata.
– The continuous flows that occur in a location of H are naturally represented with
processes of PDDL+. More specifically, for each location l we devise a process
whose precondition constrains the process to be active only when the hybrid au-
tomata is in state l; we do so by preconditioning the process with the Boolean vari-
able from F relative to l (see above). Then we set the effects of the process with
derivatives constraints expressed by Flow(l), which are the differential constraints
exhibited by the hybrid system when in that specific location.
An example of the mapping between the elements of a HA and a PDDL+ planning
problem is shown in the section Illustrative Example: Gas burner.
Decoding problem
Our objective is to verify if an automata H accepts a hybrid path that satisfies a sequence
of discrete-time state observations. This problem, known as observation decoding, has
been addressed to uncover the state trajectory of a planning agent from a sequence of
gapped observations with probabilistic sensor models [1]. In this paper, however, we
assume that observations contain precise measurements for all variables in X, and we
leave the management of uncertainty and partial observations for future work.
We note that the sampling rate of the real system that H is simulating may not
match every possible change of mode in JHK; that is, since the observations input may
be produced at any unknown rate, this leads to scenarios in which two consecutive ob-
servations may belong to the same location of H or scenarios in which two consecutive
observations belong to two non-consecutive states of a hybrid path accepted by H. This
highlights the unbounded nature of the decoding problem and justifies the use of plan-
ning for solving it.
Definition 1 (Observation) An observation of an automata H is a pair o = ht, φi,
where t ∈ T is a time point and φ is a measurement of variables X.
Definition 2 (Observation sequence) We define an observation sequence of length K
as ω = (ok )K k=1 , where each ok = htk , φk i, is a measurement (valuation) φ for
variables X that was collected at time tk . For any pair of consecutive observations
hok , ok+1 i, it holds that tk+1 > tk .
Let τ = q0 σ0 q1 σ1 . . . σn−1 qN be a hybrid trajectory. Since every transition label
belongs to Lab or Time, σi ∈ R≥0 . We define the time at which the system reaches
state qi recursively as clock(q0 ) = 0 and clock(qi ) = clock(qi−1 ) + σi−1 , 1 ≤ i ≤ N .
Definition 3 (Decoding problem) Given a hybrid automata H and an observation se-
quence w = (ht1 , φ1 i, ht2 , φ2 i . . . , htK , φK i), the solution to the decoding problem
hH, wi is a hybrid trajectory τ = (l0 , v0 )σ0 (l1 , v1 )σ1 . . . σn−1 (lN , vN ) such that there
exists only one state qi ∈ τ that satisfies tk = clock(qi ) and φk = vi .
Among all trajectories accepted by H that solve the decoding problem, we aim
to find τ ∗ = minτ ∈H f (q0 , q1 , . . . , qN ), the hybrid trajectory that minimizes the path
length. The ability to find the optimal path will depend on the planner functionalities.
Intuitively, this means finding a trajectory q0 σ0 q1 σ1 . . . σn−1 qN ∈ Σ ∗ that minimizes
the number of discrete transitions. Since planners are typically designed for this metric,
this amounts to finding a PDDL+ plan with minimal plan length.
Illustrative example: Gas burner
In this section we present the PDDL+ encoding of a well-known hybrid system formal-
ized as an hybrid automaton. We solved the problem with the planner ENHSP [9], a
heuristic search planner that can read and solve the targeted PDDL+. We run ENHSP
with default parameters (corresponding to running a plain state-space search guided by
the AIBR heuristic) but change the discretization-based approach so as to represent the
example of interest with a suitable time granularity. In particular, we set the discretiza-
tion factor of the Gas burner example to 0.1s.
The hybrid system consists of a single gas-burner that is used for heating alterna-
tively two water tanks. The HA that models this problem is shown in Figure 1. The
problem description as well as the figure are borrowed from [5].
Figure 1 shows that the HA comprises three locations: in l1 the burner is heating
tank1 whose temperature is represented with variable x1 ; in l2 the burner increases the
temperature x2 of tank2 ; in location l0 the burner is switched off. The dynamics in each
location is given by predicates ONi and OFFi (i = 1, 2): the constants ai model the
heat exchange rate of tank i with the room, bi model the heat exchange rate between
the two tanks and hi depends on the power of the gas-burner. In this example, constant
values are h1 = h2 = 2, a1 = a2 = 0.01 and b1 = b2 = 0.005.
With initial values x1 = 0, x2 = 50 and starting in location l1 , the burner heats
up tank1 until it reaches a temperature of 100 degrees. At this time, the temperature of
tank2 is below 80 degrees and the HA takes the discrete transition toggle to location
l2 , where the burner heats up tank2 until it reaches 100 degrees. Since x1 is still above
80 degrees, the HA transits via turnoff2 to l0 where the burner is off. It briefly remains
here until x1 falls to 80 degrees, at which point it takes transition turnon1 to l1 where
the burner heats up tank1 .
Fig. 1. HA representing a gas burner task (the figure is taken from [5])
Figure 2 shows the process that encodes the Flow in location l1 , where #t is a
syntactical device to explicit the fact that the effect is a time-dependent effect. Figure 3
depicts the edge (l1 , v1 , l2 ) represented as a PDDL+ action. When the HA is in l1 and
the temperature of tank1 reaches 100C, the planner chooses between action toggle or
action turnoff1 . In contrast, when the HA is at l0 and x1 takes value 80C, the required
jump to l1 is represented with an event since there is no other available choice (see
Figure 4).
Figure 5 shows the mandatory conditions of Inv(l0 ) that must be satisfied when the
system is in l0 . Finally, Figure 6 shows the implementation of an event to capture the
(:process flow_l1
:parameters ()
:precondition
(and
(l1)
)
:effect
(and
(increase (x1) (* #t (+ 2 (+ (* -0.01 (x1))(* 0.005 (x2))))))
(increase (x2) (* #t (+ (* -0.01 (x2))(* 0.005 (x1)))))
)
)
Fig. 2. Flow of location l1 encoded as a process
(:action toggle_l1_l2
:parameters ()
:precondition
(and
(l1)
(or
(and (>= (x1) 99) (<= (x1) 101) (<= (x2) 81))
(and (>= (x2) -1) (<= (x2) 1) (>= (x1) 19))
)
)
:effect (and (not (l1)) (l2))
)
Fig. 3. Edge toggle from l1 to l2 encoded as an action
input observation. We note that for an observation o = ht, φi, where φ = [x1 , x2 ] repre-
sents the temperature of tank1 and tank2 , respectively, (i) we set the time granularity of
o to 0.1s; and (ii) the precision of the temperature reading is set to ±1 its actual value.
(:event turn_on1
:parameters ()
:precondition (and
(l0)
(>= (x1) 79)
(<= (x1) 81)
)
:effect (and (not (l0)) (l1))
)
Fig. 4. Edge turnon1 from l0 to l1 encoded as an event
We tested a decoding problem with observation sequence w = (h50, [87.4, 40.2]i,
h100, [85.7, 96.3]i, h150, [80.8, 98.4]i, h200, [81.8, 94.6]i, where each tuple corresponds
(:constraint inv_l0
:parameters ()
:condition (and
(or
(not (l0))
(and
(<= (x1) 101)
(>= (x1) 79)
(<= (x2) 101)
(>= (x2) 79)
)
)
)
)
Fig. 5. Invariant of l0 encoded as a constraint
to an observation, being the first element the time of the observation and the values in
brackets the values of x1 and x2 . The ENHSP planner found a plan in 127s correspond-
ing to a hybrid trajectory accepted by the HA that explains the four observations (see
Figure 7). The 2013 actions of the plan are broken down into 2000 wait actions corre-
sponding to 200s of continuous flow with a time discretization of 0.1s, 9 actions and
events for the discrete transitions, and 4 events for the validation of the observations.
The validate events are used for reading the observations and the waiting lines de-
note the continuous trajectory in a location. The hybrid trajectory starts in location l1 ,
which satisfies the first observation. At t = 60, the HA jumps to location l2 . Subse-
quently, at t = 94.0 the action turnoff2 is executed and the system enters location l0 .
At t = 97 the event turnon1 is triggered as the temperature of tank1 cools down to 80.
The second observation matches a state whose location is l1 . The plan goes on until the
last observation is validated.
(:event validate
:parameters ( ?x - observation)
:precondition
(and
(not (observed ?x))
(> (time_observation ?x) (- (running_time) 0.05))
(< (time_observation ?x) (+ (running_time) 0.05))
(>= (x1) (- (x1_observation ?x) 1))
(<= (x1) (+ (x1_observation ?x) 1))
(>= (x2) (- (x2_observation ?x) 1))
(<= (x2) (+ (x2_observation ?x) 1))
)
:effect (and (observed ?x))
)
Fig. 6. Event for validating an input observation
0.0: -----waiting---- [50.0]
50.0: (validate o1)
50.0: -----waiting---- [60.2]
60.2: (toggle_l1_l2)
60.2: -----waiting---- [93.8]
93.8: (turn_off2)
93.8: -----waiting---- [96.8]
96.8: (turn_on1)
96.8: -----waiting---- [100.0]
100.0: (validate o2)
100.0: -----waiting---- [108.7]
108.7: (turn_off1)
108.7: -----waiting---- [135.2]
135.2: (turn_on2)
135.2: -----waiting---- [147.6]
147.6: (turn_off2)
147.6: -----waiting---- [149.7]
149.7: (turn_on1)
149.7: -----waiting---- [150.0]
150.0: (validate o3)
150.0: -----waiting---- [162.0]
162.0: (turn_off1)
162.0: -----waiting---- [190.5]
190.5: (turn_on2)
190.5: -----waiting---- [200.0]
200.0: (validate o4)
Plan-Length:2013
Fig. 7. Plan returned by ENHSP for the observation sequence
We illustrate now a portion of the hybrid trajectory corresponding to the plan in
Figure 7 until t = 108.7. We show the states traversed by the HA and highlight in bold
the states that satisfy the first two observations ((validate o1) and (validate
o2)). A reminder that we are using a precision of 0.1s for the time and ±1 for the
temperature of the tanks.
hl1 , [0, 50]i →50 hl1 , [87.1, 40.3]i →10.2 hl1 , [100, 40.9]i →toggle
hl2 , [100, 40.9]i →33.6 hl2 , [81.9, 99.1]i →turnoff2 hl0 , [81.9, 99.1]i →3
hl0 , [81, 97.4]i →turnon1 hl1 , [81.1, 97.4]i →3.2 hl1 , [86.2, 95.6]i →8.7
hl1 , [99.6, 91.5]i →turnoff1 hl0 , [99.6, 91.5]i →26.5 . . .
Conclusions and Discussion
This work presents a first step towards recognition of trajectories in cyber-physical
systems that exhibit a hybrid dynamics. Our proposal lies in using the Hybrid Au-
tomata formalism to model the system behaviour, mapping the semantics of a HA into
a PDDL+ planning problem and then solving the problem with a planner. As a result,
we obtain a plan which defines the trajectory that matches the discrete-time state obser-
vations gathered from the hybrid system.
One question underlying our proposal is the added value of encoding the semantics
of a HA into a mixed discrete-continuous planning problem over other techniques such
as for example the use of verification tools for HAs. In this regard, model-checking
tools are widely used in formal verification of safety properties of hybrid systems. This
is commonly addressed as a reachability analysis that computes the set of all possible
states the system can reach and checks whether every execution of the system always
stays within a set of safe states. There are several distinctive features in our problem
that justifies the use of planning technology:
– between two gathered observations, the hybrid system may go through an indefinite
number of states; that is, the length of the trajectory that links two observations is
unknown
– state reachability is a satisfiability problem aimed at verifying whether or not the
system reaches a safe state. In plan recognition, we seek to optimize the length of
the trajectory or any other metric.
The paper illustrates the behaviour of a simple HA that models a gas burner to
heat two water tanks, its encoding in PDDL+ and resolution with the ENHSP planner.
We have recently initiated an experimentation with more complex examples that fea-
ture composition of various hybrid automata. The promising results highlight that the
PDDL+ modeling of the problem allows synchronization of HAs wherein each presents
a different dynamics. All in all, this paper is a first step towards the modeling of HA
with planning technology.
References
1. Diego Aineto, Sergio Jiménez, and Eva Onaindia. Observation decoding with sensor models:
Recognition tasks via classical planning. In 30th International Conference on Automated
Planning and Scheduling ICAPS, pages 11–19. AAAI Press, 2020.
2. Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Automata, Lan-
guages and Programming, 17th International Colloquium, ICALP90, volume 443 of Lecture
Notes in Computer Science, pages 322–335. Springer, 1990.
3. Sandra Carberry. Techniques for plan recognition. User Model. User-Adapt. Interact., 11(1-
2):31–48, 2001.
4. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors.
Handbook of Model Checking. Springer, 2018.
5. Laurent Doyen, Goran Frehse, George J. Pappas, and André Platzer. Verification of hybrid
systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem,
editors, Handbook of Model Checking, pages 1047–1110. Springer, 2018.
6. Maria Fox and Derek Long. Modelling mixed discrete-continuous domains for planning. J.
Artif. Intell. Res., 27:235–297, 2006.
7. Miquel Ramı́rez and Hector Geffner. Plan Recognition as Planning. In 21th International
Joint conference on Artifical Intelligence, IJCAI, pages 1778–1783. AAAI Press, 2009.
8. Jean-François Raskin. An introduction to hybrid automata. In Dimitrios Hristu-Varsakelis
and William S. Levine, editors, Handbook of Networked and Embedded Control Systems,
pages 491–518. 2005.
9. Enrico Scala, Patrik Haslum, Sylvie Thiébaux, and Miquel Ramı́rez. Interval-based relax-
ation for general numeric planning. In ECAI 2016 - 22nd European Conference on Artificial
Intelligence, volume 285 of Frontiers in Artificial Intelligence and Applications, pages 655–
663. IOS Press, 2016.
10. Enrico Scala, Miquel Ramı́rez, Patrik Haslum, and Sylvie Thiébaux. Numeric planning with
disjunctive global constraints via SMT. In Proceedings of the Twenty-Sixth International
Conference on Automated Planning and Scheduling, ICAPS 2016, London, UK, June 12-17,
2016, pages 276–284. AAAI Press, 2016.
11. Gita Sukthankar, Robert P. Goldman, Christopher Geib, David V. Pynadath, and Hung Bui.
Plan, Activity, and Intent Recognition: Theory and Practice. Morgan Kaufmann, 2014.
12. Paulo Tabuada. Verification and Control of Hybrid Systems - A Symbolic Approach. Springer,
2009.