Hybrid systems model software-based control systems to deal with real-world applications that exhibit an interaction of discrete and continuous dynamic 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 following the HA dynamics. Ultimately, we show the adequacy of PDDL+ to model HAs with two well-known examples in the literature on HAs.
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 physical 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
Automata (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 [
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 [
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
License Attribution 4.0 International (CC BY 4.0).
the observed behaviour of a system is actually modeled by a given HA. In discrete
environments modeled as finite-state machines, plan recognition is the task of predicting
the plan of an acting agent based on its observed actions [
For our purposes, we use PDDL+, a powerful modelling language to express discrete and continuous change. Planning in mixed discrete-continuous domains is a challenging 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 trajectories that comply with the state observations.
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 .
In general, the state of a hybrid system is defined by the values of its continuous variables 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 evolution. 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 [
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 = fx1; : : : ; xng 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 possible valuations of X when the control of H is at l – Flow : Loc ! PConstr(X S X_ ) constrains the valuation evolution of X according to the rate of change given by their time derivative X_ – Jump : Edg ! PConstr(X S X+) gives the jump condition of edge e and X+ 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 [
The timed transition system defined by a hybrid automata H is a tuple JHK = hS; S0; Sf ; ; !i. The set S = f(l; v)j l 2 Loc; v 2 JInv(l)Kg is the state space of H; S0 = f(l; v) 2 Sj v 2 JInit(l)Kg denotes the set of initial states (Sf is the set v!22 SJFinal(l)KS); is th=e trLaanbsiStioTni mreelat(iToinm; etha2t isR, tu0p)leiss oaffithneitefosremt o(lf; vla)be!ls. F(lin0;avll0y),, 2 , such that every tuple belongs to one of the two following cases: – discrete transition: e = (l; ; l0) 2 Edg, 2 Lab, and (v; v0)22RJJu0mapn(de)aKcontin– continuous transition: 2 Time, l = l0, and there exists uously differentiable function : [0; ] ! RX such that (0) = v, ( ) = v0 and 8t 2 [0; ], ( (t); _(t)) 2 JFlow(l)K and (t) 2 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 [
We now show an example of the behaviour of the temperature in a room
controlled by an HA (thermostat) with two locations Loc = flON; lOFFg, two labels Lab =
fON; OFFg, and two edges that connect both locations and a variable x that represents
the room temperature [
A hybrid trajectory that illustrates the evolution of the room temperature according to the above HA is a sequence q0 0q1 1 : : : n 1qn, where qi = (li; vi), q0 2 S0, q = qn, i 2 and (qi; i; qi+1) 2!. 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.
PDDL+ [
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 2 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 2 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 2 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 x_ = 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) 2 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 nondeterminism in how events are sequenced.
A plan is said to be a solution for a problem if each action (t; a) 2 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 [
We consider for the scope of this paper a slightly variant of PDDL+. In such a variant 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.
The theory of HA provides an ideal formal basis for the development of a semantics for
PDDL+. The work [
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 [
For many of the HA typically discussed in the literature, it commonly happens that for any pair of outgoing edges of a location l, e1 = (l; 1; l1) and e2 = (l; 2; l2), it holds JJ ump(e1)K TJJ ump(e2)K = ;. Particularly, given the following grammar rule that defines a formula ' ' ::= PTerm(X) 1 0j; 12 f<; ; =; ; >g (1) , if we restrict PConstr(X) to a subset of PConstr(X) defined by conjunctive formulas (' ^ '), 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 2 ) instead of actions, thus reducing the branching factor of the search. – It must hold I 2 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 2 S0. Additionally, a Boolean variable of F is used to represent that H is initially at l. – It must hold G 2 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 2 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 2 ), encoding an implication of the form if Loc = l then Inv(l). Specifically, given a valuation for X 2 H, the constraints of PDDL+ verify that 8x 2 X, v(x) 2 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 automata is in state l; we do so by preconditioning the process with the Boolean variable 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.
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 [
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 observations 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 planning for solving it.
Definition 1 (Observation) An observation of an automata H is a pair o = ht; i, where t 2 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)kK=1, where each ok = htk; ki, is a measurement (valuation) for variables X that was collected at time tk. For any pair of consecutive observations hok; ok+1i, it holds that tk+1 > tk.
Let = q0 0q1 1 : : : n 1qN be a hybrid trajectory. Since every transition label belongs to Lab or Time, i 2 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 sequence w = (ht1; 1i; ht2; 2i : : : ; 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 2 that satisfies tk = clock(qi) and k = vi.
Among all trajectories accepted by H that solve the decoding problem, we aim to find = min 2H 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 0q1 1 : : : n 1qN 2 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.
In this section we present the PDDL+ encoding of a well-known hybrid system formalized 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 discretization factor of the Gas burner example to 0.1s.
The hybrid system consists of a single gas-burner that is used for heating
alternatively 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 [
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 turno 2 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.
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 turno 1. 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 input observation. We note that for an observation o = ht; i, where = [x1; x2] represents 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
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 ) 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 corresponding 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 corresponding 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 denote 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. Subsequently, at t = 94:0 the action turno 2 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
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 !turno 2 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 !turno 1 hl0; [99:6; 91:5]i !26:5 : : :
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 Automata 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 observations 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 feature 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. 9. Enrico Scala, Patrik Haslum, Sylvie Thie´baux, and Miquel Ram´ırez. Interval-based relaxation 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 Thie´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.