Explaining the Behaviour of Hybrid Systems with PDDL+ Planning

1 Introduction

A hybrid system (HS) is a dynamical system that exhibits a discrete and continuous behaviour, and captures the control of continuously evolving physical activities typical in automated manufacturing, chemical engineering and robotics systems. A hybrid trajectory is a particular execution of the HS that interleaves discrete and continuous behaviour. We aim to solve the problem of finding an explanation, i.e., a hybrid trajectory, for some observations of an HS. We will call this the HS explanation (HSE hereinafter) problem. To this end, we build on the formalism of hybrid automata (HA) to formulate the problem and on planning technology to solve it.

The formalism of HA [Henzinger, 2000] is extensively used in Model Checking (MC) of hybrid systems, specifically for verification of safety properties. The safety verification problem is traditionally formulated as a reachability analysis aimed at certifying that a trajectory that violates the property does not exist, thereby a correspondence between this problem and our HSE problem can be found. A common approach is to compute a conservative over-approximation of the reachable state space that is used to guarantee that the HS is safe if none of the states defined as unsafe is reachable. The issue with MC tools that use over-approximation [Henzinger et al., 1997; Frehse, 2008] is that they are generally unable to produce a concrete trajectory, i.e., a counter-example, for an HS that is deemed unsafe. Exceptionally, tools such as DREACH [Kong et al., 2015] and HYCOMP [Cimatti et al., 2015], both built on top of Satisfiability Modulo Theories (SMT) solvers, are able to generate counterexamples. Another mechanism to directly seek a trajectory that violates a safety condition in an HS is falsification [Plaku et al., 2009]. Falsification tools [Annpureddy et al., 2011; Zhang et al., 2018] find the inputs required to steer the system towards violating the property and use optimization techniques guided by robustness metrics. They generally assume that the system dynamics are governed by a black-box model whose behaviour is only observed from the input signals and their corresponding outputs via a simulator [Zutshi et al., 2014; Corso et al., 2020]. Simulation-based techniques for falsification, in addition, heavily rely on urgent discrete transitions, i.e., a discrete transition is immediately taken once the condition is satisfied, which makes them unsuitable for the nondeterministic behaviour in our benchmarks.

We characterize the language of explanations through a network of HA in parallel composition, where one automaton describes the HS and the other accepts the given observations. This composition effectively restricts the trajectories of the HS to those that are consistent with the observations. We then formalize the HSE problem as an optimization problem that looks over the language of explanations to find the most suitable one. In principle, this problem can be solved as a model checking problem but the aforementioned approaches followed by state-of-the-art MC tools struggle to find concrete trajectories, or assume limited knowledge of the systems dynamics, or only handle simple dynamics. To overcome this limitation, we further provide a formal mapping from HA to PDDL+ [Fox and Long, 2006], which enables the use of offthe-shelf automated planners. AI Planning heuristics have in the past proven very effective for finding trajectories [Wehrle and Helmert, 2009].

The connection between HA and PDDL+ has been mainly explored as the translation from PDDL+ planning to HA to underpin the formal interpretation of PDDL+ semantics with the HA formalism [Fox and Long, 2006; Bogomolov et al.,

2015]. Mapping PDDL+ into HA enables solving a hybrid planning problem using model-checking tools. Another research advocates encoding hybrid planning problems with SMT [Bryce et al., 2015; Cashmore et al., 2020] as a way to overcome the general limitation of PDDL+ planners to address nonlinear changes. We exploit the reverse mapping, encoding the network of HA as PDDL+ planning.

Our algorithmic solution to the HSE problem comes down to a plan recognition (PR) problem in an HS as we need to infer the trajectory (plan) that fulfills the observations of the HS (agent) in a continuous space. Unlike approaches to PR that use planners [Ram´ırez and Geffner, 2009], our aim is not goal prediction and our observations are not sub-sequences of actions as it is commonly the case in the PR approaches. We focus on finding the best sequence of states traversed by a system that explains some observations [Aineto et al., 2020].

Our main contributions are: (a) a crisp formulation of the HSE problem that draws on the HA formalism; (b) a planning-based approximation to the HSE problem that exploits PDDL+ models and algorithms to scale up to large state spaces; and (c) an experimental analysis that includes a comparison between our planning-based approach and MC tools.

2 Preliminaries

A hybrid automaton is formally defined as an FSM, where states (locations) prescribe constraints over a set of variables, and transitions are governed by ordinary differential equations. We adopt the HA formulation used in [Doyen et al., 2018] with explicit input variables. Firstly, we introduce some notation: X is a set of variables; Constr(X) is the set of constraints over X defined by the Backus Naur rule ϕ ::= θ < 0 | θ ≤ 0 | θ = 0 | θ > 0 | θ ≥ 0 | ϕ ∧ ψ, being θ a polynomial expression over X; �ϕ� refers to all valuations of ϕ over X, and �ϕ�v to a particular valuation v.

The tuple H = ⟨Loc, Lab, Edg, X, U, Init, Inv, Flow, Jump, Final⟩ defines a hybrid automaton, where:

• Loc is a set of discrete variables called locations of H.
• Lab is a set of labels.
• Edg ⊆ Loc × Loc is a set the discrete transitions.
• X = {x1, . . . , xn}, set of real-valued state variables.
• U = {u1, . . . , um}, set of real-valued input variables.
• Init : Loc → Constr(X) states the possible valuations of X when H starts in location l, i.e., H can start in l with an initial valuation v ∈ �Init(l)�.
• Flow : Loc → Constr( ˙X ∪X ∪ U) specifies what differential constraints apply on the behaviour of X when H is at l.
• Inv : Loc →Constr(X ∪U) is the invariant of location l, which constrains the possible valuations of X and U when H is at l. H can stay in l as long as the valuation v ∈ �Inv(l)�.
• Jump : Edg → Constr(X+ ∪ X ∪ U) gives the jump condition of edge e, often as a conjunction of a guard, Guard : Edg → Constr(X ∪ U), and a reset constraint, Reset(e) : Edg → Constr(X+), where variables in X+ refer to the updated values of X after edge e is traversed.
• Final : Loc → Constr(X) is the final condition of location l. H can only finish in l if the final valuation v ∈ �Final(l)�.

The semantics of H is the transition system �H� = ⟨S, S0, Sf , Σ,→⟩; a state is a pair q = (l, v), where l ∈ Loc and v is the valuation over X in l; S is the state space; S0 is the set of possible initial states; Sf is the set of final states; Σ = Lab ∪ R≥0 , where R≥0 denotes duration; and → is the transition relation that contains all tuples ((l, v), σ, (l′ , v′ )), which belong to any of these two types:

• discrete transition: σ ∈ Lab, e = (l, σ, l′ ) ∈ Edg, and (v, v′ ) ∈ �Jump(e)�. These transitions have no duration and are instantaneous.
• continuous transition: σ ∈ R≥0 , l = l′ , and Flow(l) determines the evolution of X, which changes from valuation v to valuation v′ while remaining in location l as long as the valuation satisfies �Inv(l)�. The duration of continuous transitions is given by σ.

A trajectory is a run of �H� defined as τ = q0σ1q1σ2 . . . σnqn or, equivalently, as τ = q0 σ1 -→ q1 σ2 -→ . . . σn --→ qn, where q0 ∈ S0, and (qi-1, σi, qi) is a transition from →, ∀i 1 ≤ i ≤ n. We define d(qi) as the sum of the duration for every transition between q0 and qi, and it represents the time at which state qi is reached. If qn ∈ Sf , we say that τ is a trajectory accepted by H. The set of all trajectories accepted by H is the language of H, denoted as L(H).

PDDL+ (Planning Domain Definition Language) is a high-level language to formulate planning instances that require reasoning over a mixture of discrete and continuous variables [Fox and Long, 2006]. A PDDL+ instance is given by the tuple Π = ⟨V, F,A, P,E, I,G⟩, where V and F are numeric and Boolean state variables, respectively, I is the initial state, and G is the goal condition. PDDL+ explicitly differentiates three types of state transitions, namely, actions A, events E and processes P. An action a ∈ A is a pair ⟨prea, effa⟩ where prea is a formula containing both propositional and numeric conditions, and effa is a set of propositional and numeric assignments that cause instantaneous changes. The execution of an action a is decided by the planner as long as prea holds in the current state. An event e ∈ E is structured as an action but its execution is triggered by the satisfaction of its preconditions rather than being decided by the planner. A process p ∈ P is a pair ⟨prep, effp⟩, where prep has the same structure as prea, and effp only contains continuous effects, which are time-dependent effects of the form ˙x = ξ (ξ represents the first derivative of x w.r.t. time).

Actions are in control of the agents while P and E describe what happens in the world when some condition is met. Processes last for as long as their conditions are met. For example, heating up a tank is a process which increases its temperature until a max value (e.g. t = 100◦C) is reached. Events correspond to instantaneous transitions that happen the instant their conditions are met, usually transforming the state in such a way that the conditions are no longer met. Events are uncontrollable; in the previous example, we might consider an event when the tank hits t = 100◦C, at which time the tank turns off.

We consider PDDL+ problems extended with a set C of global constraints (propositional formulae as the ones used in actions' preconditions) [Scala et al., 2016]. C constrains state trajectories to those that always satisfy the formula in C. A PDDL+ plan is a set of timed actions, i.e., pairs from R≥0 ×A plus the ending time te ∈ R≥0 . Informally speaking, a plan is said to be valid iff i) the induced trajectory of states conforming to prescribed events, processes and global constraints, and obtained by starting from the initial state, is such that all actions have their precondition satisfied when

they are applied, ii) the plan satisfies the goal at time te.

3 The HS Explanation Problem

The HSE problem is about finding a trajectory of an HS that matches some observations. This problem is formulated through two HA: one automaton models the behaviour of the HS, the other one tracks the run of the HS and checks when the produced trajectory matches the observations. We will refer to the first one as the HS automaton, and to the second one as the monitor automaton. Let H = ⟨Loc, Lab, Edg,X, Init, Inv, Flow, Jump, Final⟩ be the HS automaton:

Definition 3.1 (Observation). An observation, z, on the behaviour of H, z ∈ R≥0 ×Constr(X), is the pair ⟨t, ϕ⟩, where t is a time point, and ϕ is a constraint over X.

By defining observations as constraints, ϕ is actually denoting a region of values, and so we can express qualitative uncertainty in the observations and partial observability over the state variables X. From a practical standpoint, sensors are rarely completely accurate and the dynamics that govern some variables in X may not be directly measurable, e.g. the linear acceleration of an aircraft.

Example 3.2. Consider that the behaviour of an aircraft flying at a fixed altitude is modeled by the hybrid automaton H of Figure 3. H defines three control modes or locations, Loc = {FS,AL,AR}, representing, respectively, 'flying straight', 'adjusting course left' and 'adjusting course right'. Let X = {x, y, θ} be the set of state variables of H, where (x, y) ∈ R2 describes the planar position, and θ is the angular orientation. Moreover, during the flying trajectory of the aircraft, its position is observable but θ is not. Initially, the aircraft is at position (0, 0) and pointing at a direction given by the angle θ = 4.84. An observation of the aircraft during flight is defined as

where (cx, cy) ∈ R2 is the center of a circle of radius r ∈ R. For instance, at time t=1, the observation is z1 = ⟨1, (5.593x)2 + (-19.117 - y)2 ≤ 102 ⟩, meaning that the position of the aircraft is somewhere within a circular region of radius r = 10 centered around (5.593, -19.117).

A sequence of observations is denoted as ω = (zk)Kk=1 , where each zk is an observation as expressed in definition 3.1. Let ω be an observation sequence of the behaviour of a system that is modeled through an HS automaton H. We define a monitor automaton, Hω , which contains as many locations as the number of observations in ω, aimed at determining when the trajectory produced by H matches the observations in ω. The monitor automaton Hω = ⟨Locω , Labω , Edgω , Xω , U ω Initω , Invω , Flowω , Jumpω , Finalω ⟩ is formalized as:

• Locω := {l0, . . . , lK}. Hω contains one location for each observation zk ∈ ω; l0 is the initial location of Hω .
• Labω is a set of labels (labels in Hω are meaningless).
• Edgω := {(lk-1, σk, lk) | 1 ≤ k ≤ K}. Discrete transitions move from one location to the next one.
• Xω := {t}. Hω explicitly models the passage of time through the time variable t for matching purposes.
• U ω ⊆ X. The input variables of Hω are the subset of the state variables X of H that are observable.
• Initω := {Initω (l0) := t = 0}. Time starts at t = 0.
• Invω := {Invω (lk) := t ≤ tk+1 +∆t | 0 ≤ k ≤ K - 1}. The automaton can remain at location lk until the last instant allowed to validate observation zk+1. Invω is redudant with Jumpω and can be omitted.
• Flowω = {Flowω (l) := ˙ t = 1 | l ∈ Locω }, meaning that time advances normally.
• Jumpω = {Jumpω ((lk-1, σk, lk)) := tk -∆t ≤ t ≤ tk + ∆t ∧ ϕk | (lk-1, σk, lk) ∈ Edgω }. For observation zk = ⟨tk, ϕk⟩, the jump condition ensures that there is one time point within a specified interval around tk where the valuation of the constraint ϕk holds.
• Finalω := {Finalω (lK) := true}.

As specified in Jump, for each observation zk = ⟨tk, ϕk⟩, we define a time window [tk -∆t, tk +∆t], being ∆t a time precision parameter, as the interval where we accept that the constraint ϕk can be matched. Hω models the passage of time via the variable t, and it is constantly tracking the observable variables of H comprised in U ω . The task of Hω is to check that the values of U ω match the constraint ϕk within the interval [tk-∆t, tk+∆t]; that is, it checks that �ϕk�u holds at any point in the interval. More specifically, Hω awaits in location lk-1 for the input values u to match the observation zk in the specified interval, moment at which Hω transits to location lk. The run of �Hω � produces a trajectory that traverses all the locations in Locω . We will denote this trajectory as τ ω .

Ultimately, our objective is to build a network of HA in parallel composition, N = {H,Hω }, that characterize the set of trajectories of H that explain the observed behaviour given by ω. For the network, we use global-time compositional semantics [Henzinger, 2000] where time elapses for all the HA in the network and for the same duration, and communication is achieved through shared variables, specifically through the variables U ω .

Definition 3.3 (Synchronized trajectory of N). A synchronized trajectory of N = {H,Hω } is the pair τS = ⟨τ, τ ω ⟩ such that τ = q0σ0 . . . qn and τ ω = qω 0 σω 0 . . . qωm are concurrent local trajectories of H and Hω , respectively, and have the same duration (d(qn) = d(qwm)). A synchronized trajectory τS = ⟨τ, τ ω ⟩ is accepted by N, denoted τS ∈ L(H,Hω ), iff τ ∈ L(H) and τ ω ∈ L(Hω ).

Definition 3.4 (Explanation & Support). τ ∈ L(H) is an explanation for an observation sequence ω under H iff there exists a support τ ω ∈ L(Hω ) such that ⟨τ, τ ω ⟩ ∈ L(H, Hω ). We define the language of explanations as E(H, ω) = {τ | ⟨τ, τ ω ⟩ ∈ L(H, Hω )}.

Then, an explanation τ is the trajectory that explains the behaviour of the hybrid system 1 , and a support τ ω is the trajectory that determines when τ matches the observations.

Example 3.5. We extend the Example 3.2 of the aircraft assuming an observation sequence ω of the HS automaton H (Figure 3) given by the following two observations:

Our HSE problem is to find a trajectory of the aircraft modeled by H that explains ω = (z1, z2). We define a monitor automaton Hω that contains one location for z1 and one for z2 using time precision ∆t = 0.125. Fig. 1 shows a solution to the problem; i.e, a synchronized trajectory ⟨τ, τ ω ⟩ of the network N = {H,Hω } where τ is the aircraft explanatory trajectory for ω, and τ ω determines when τ matches z1 and z2. The lower part of Fig. 1 details the synchronization of τ and τ ω (only the observable variables of H, U ω = {x, y}, and the single variable t of Hω are shown). Discrete transitions σω 1 and σω 2 happen at t1 = 0.88 and t2 = 1.88 when τ validates (matches) the observations z1 and z2. ϵ transitions are 'stutters' representing self-loops ((l, v), ϵ, (l, v)) that replicate the state of one automaton when the other performs a discrete transition [Alur et al., 1995].

There may exist multiple trajectories of Hω that support the validation of the observations by an explanation τ. For instance, in Example 3.5, the trajectory τ ω = (L0, 0) 1.12 --→ (L0, 1.12) σω 1 --→ (L1, 1.12) 0.76 --→ (L1, 1.88) σω 2 --→ (L2, 1.88) also synchronizes with τ. This happens because the matching of an observation < tk, ϕk > can occur at any point in the continuous time interval [tk -∆t, tk +∆t]. We refer to a support composed only of urgent discrete transitions, i.e., transitions that are immediately taken once the Jump condition is enabled, as a greedy support and denote it as τ ω g . The question that arises here is whether using a greedy support to match the observations of an explanation compromises the completeness of an HSE problem. Theorem 3.7 proves this is not the case.

1 Our notion of explanation is not to be confused with planning explanations [Fox et al., 2017] which also account for the process that generated the trajectory.

Definition 3.6 (Prefix). Given two trajectories τ ′ and τ, τ ′ is a prefix of τ, τ ′ ⊆ τ, if either they are identical, or τ ′ is a finite sequence and τ begins with τ ′ .

Theorem 3.7. Let Lg(H,Hω ) ⊆ L(H,Hω ) be the subset of synchronized trajectories formed with a greedy support τ ω g , and Eg(H, ω) = {τ | ⟨τ, τ ω g ⟩ ∈ Lg(H,Hω )}. For every τ ∈ E(H, ω) , there exists a τ ′ ∈ Eg(H, ω) such that τ ′ is a prefix of τ.

Proof : We show that for any explanation τ in E(H, ω), it is possible to construct a greedy trajectory τ ω g that supports a prefix τ ′ ⊆ τ. Let τ be an explanation for ω = (zk)Kk=1 , zk = ⟨tk, ϕk⟩, and Ik = [ak, bk], with tk - ∆t ≤ ak ≤ bk ≤ tk + ∆t, be all the time points at which τ matches the observation; i.e., �ϕk�u holds ∀t ∈ Ik. A greedy support τ ω g for τ ′ ⊆ τ is built by taking discrete transitions ((lk-1, ak), σω , (lk, ak)) at time mk = max(mk-1, ak) for 1 ≤ k ≤ K. So observation zk is matched as soon as the matching of zk-1 allows within the interval Ik = [ak, bk].

The maximum difference in duration between an explanation τ in E(H, ω) and its prefix τ ′ in Eg(H, ω) is bK - aK, which is bounded by 2∆t. Then, for a sufficiently small ∆t there is no significant difference between both languages. Particularly, when ∆t = 0 we have E(H, ω) = Eg(H, ω) since the explanation τ and its prefix τ ′ are identical. We can thus assume urgent transitions for Hω , which effectively narrow the language of the network N = {H, Hω }, while guaranteeing that Eg(H, ω) contains an almost complete prefix of any possible explanation in E(H, ω).

Definition 3.8 (HS-explanation problem). An HSE problem is given by the tuple ⟨H, ω⟩, where H is the description of an HA, and ω is a sequence of observations.

The solution to ⟨H, ω⟩ is defined as follows

Problem (1)-(5) is an optimization problem over the language of explanations L(H,Hω ). Subproblem (2)-(5) is the underlying reachability problem of searching trajectories that belong to L(H,Hω ). Solutions π(H,Hω ) are synchronized trajectories τS = ⟨τ, τ ω ⟩ accepted by N, as ensured by constraints (4)-(5) that minimize a user-defined function f (·) that measures the implausibility of an explanation.

Figure 2 illustrates graphically the HSE problem for our aircraft example. A 100-sec trajectory (black line) represents the original trajectory of the aircraft produced by the HS automaton H. In order to generate the observations of the aircraft position, the original trajectory was sampled at 1-sec intervals with different radius, r ∈ {5, 10, 20, 40}. The colored lines are the trajectories that explain the observed behaviour of the aircraft under the different values of r.

4 HS Explanation as Planning

We present our proposal to approximate the solution to the HSE problem as for equations (1)-(5) using PDDL+.

Optimization function. As commented in Def. 3.8, the user defines a function to measure the quality of a solution. In our approximation, we use f(τ) = |τ|, which measures the length or number of discrete transitions of the explanation 2 . Discrete transitions are the ones that truly determine the evolution of the HS as the continuous transitions merely indicate the awaiting of the system in a location. Therefore, we believe minimizing |τ| is a reasonable proxy for more complicated objective functions. In general, the quality of the solution is subject to the range of values encompassed by the definition of the observations; the smaller the region of values, the more accurate the solution. This can be observed in Fig. 2, where the explanation under r = 5 generates a trajectory that basically covers the original flight trajectory.

Mapping the network of HA to PDDL+. The goal is to map the network of HA, N = {H,Hω }, into a PDDL+ planning instance Π(H,Hω ) and solve it with off-the-shelf planners. We will call π+(H,Hω ) the solution returned by a PDDL+ planner to the HSE problem. A solution π+(H, Hω ) will contain actions corresponding to discrete transitions of �H� such that f(τ) = |τ| is minimized, and it will reach a state satisfying the constraints in equation (5).

Let H be any hybrid automaton (either an HS or a monitor automaton). We first describe the mapping of H to a PDDL+ problem Π(H) = ⟨V, F,A, P,E, I,G,C⟩ that preserves the semantics of �H�:

• The state variables X of H map directly to numeric variables (V =X).
• The locations of H are represented using Boolean variables (F = Loc).
• A discrete transition of H is represented with a = ⟨prea, effa⟩ ∈ A, reflecting the non-determinism of H. Jump(e) is decomposed into Guard(e), encoded in prea, and Reset(e), encoded in effa (change to next location).
• The continuous transitions of H that model the evolution of X as time passes are represented with processes P, P = {⟨l, Flow(l)⟩ | l ∈ Loc}.

2 The length of a support τ ω is always bounded by the K observations in ω

• I |= Init, we assume that the initial space S0 induced by the initial condition Init of H is a singleton.
• G = lfinal. Without loss of generality, we assume there is a single location lfinal such that Final(lfinal) = true and Final(l) = false for all l ̸= lfinal as any HA can be reduced to this form.
• Inv of H is represented as the global constraints C = ∧l∈Loc ¬l ∨ Inv(l): as long as H is in location l, Inv(l) must hold (if specified). As locations are mutually exclusive, only one constraint will be active in a state.

PDDL+ events can be used, instead of actions, to encode urgent discrete transitions. Intuitively, discrete transitions of the HS automaton map into actions that represent the actual control of the agent (e.g., adjusting course left); while discrete transitions of the monitor automaton map into actions (or PDDL+ events if we want a greedy support) that are only executable when the trajectory matches with an observation.

Mapping a network N = {H,Hω } into a PDDL+ planning problem Π(H,Hω ) is done by composing the elements of Π(H) and Π(Hω ) via the union operator for sets X, F, A, P and I, and via the conjunction operator for constraints C and goal condition G. A solution plan is a set of timed instantaneous transitions π+(H,Hω ) = ({⟨t0, a0⟩, . . . , ⟨tn, an⟩}, te) such that ai ∈ A, 0 ≤ i ≤ n, and te is the ending time of the plan. π+(H,Hω ) models the discrete transitions of both H and Hω and represents a synchronized trajectory of N = {H,Hω }. Extracting the local plans for H and Hω is a straightforward process that only requires checking whether ai belongs to Lab or Labω . For instance, a PDDL+ plan for Ex. 3.5 is: {⟨0.88, validate 1⟩, ⟨0.90, adjust left⟩, ⟨1.88, validate 2⟩}, te), which includes i) the local plan for H, ({⟨0.9, adjust left⟩}, te = 1.88), representing an explanation τ of the HS, and ii) the local plan for Hω , ({⟨0.88, validate 1⟩, ⟨1.88, validate 2⟩}, te = 1.88), representing a support τ w that specifies when the HS matches the two observations. Both local plans can effectively be used to generate a synchronized trajectory to the HSE problem.

5 Empirical Evaluation

We evaluate our approach computationally on three domains with different types of dynamics: piece-wise constant, linear and nonlinear. All domains feature non-deterministic (even arbitrary) discrete mode switches.

Thermostat (constant). This domain uses Henzinger's thermostat [Henzinger, 2000] hybrid automaton. The flows are made piece-wise constant; invariants and guards leave a window of 1ºC where the system may non-deterministically switch modes. Temperature is the only observable variable.

Platoon (linear). This domain [Makhlouf andKowalewski, 2014] is a staple in the linear dynamics competition for formal verification of HS. The domain depicts a platoon of networked vehicles following each other switching between two discrete modes: a normal operation and a communicationfailure mode. We handle a platoon of 4 vehicles for a total of 9 continuous variables: relative distance and velocity to the vehicle ahead, and acceleration of each vehicle save for the leader. The observable variables are the 3 relative distances.

Flight (nonlinear). This models the domain of Ex. 3.5. Assuming a simplified physics model that ignores wind and gravitation, the in-flight dynamics of an aircraft can be described by the following differential equations:

where v and w are the linear and angular velocity. In our experiments v is made constant, so w is the only control parameter (Figure 3). The flow constraints (6)[w := a] shown in each location are abbreviations of the dynamics of equation (6) with w replaced by the angular velocity a of the respective location. We observe the planar coordinates (x,y).

We computed 10 trajectories for each domain using a simulator, and extracted observation sequences by sampling the trajectories at a fixed rate of 1sec. For each trajectory we scale the number of observations from 2 to 100: the smallest instance asks to find a trajectory explaining 2 observations over 2 secs of execution while the largest 100 observations over 100 secs of execution.

We attempt to solve the HSE problem with 3 configurations: HSE MC (via Model-Checking), and 2 configurations via Planning, HSE P and HSE Pe differing in how discrete transitions of Hω are encoded: HSE P uses actions and HSE Pe uses greedy supports; i.e., events. The comparison with HSE MC aims at evaluating the usefulness of our mapping into planning against the long-established technique of MC. We tested DREACH and HYCOMP, two MC tools that are able to generate counter-examples. Encoding the HSE

problem into the MC tools simply requires defining the unsafe condition as Finalω .

We tried different PDDL+ planners [Piotrowski et al., 2016; Penna et al., 2009; Cashmore et al., 2020], but focused on ENHSP [Scala et al., 2020] as it was the one giving us the better performance with support for the dynamics of all our domains. We ran ENHSP using the hmrp max heuristic on top of plain A∗ with a random tie-breaking. ENHSP is a discretization based planner that decouples time-discretization for planning (δp) from the one of plan execution (δe) [Ram´ırez et al., 2017]. Keeping δe small ensures that i) the generated explanations remain valid and ii) far more states can match the observations. We keep δp = δe = 0.01 over all domains when ENHSP run using HSE P, and set δp = 0.1 in Thermostat and Platoon, and δp = 0.4 in Flight when ENHSP run with HSE Pe. All experiments run on an Intel Core i5 3.1GHz x 4, time and memory limits set to 300s and 8GB, respectively.

Results. For each domain-configuration and problem size, we show the number of problems solved and the median time over successful runs (shown in parentheses in Table 1). A problem is solved if a solution was found within a time frame of 300s. Solutions found by HSE P and HSE Pe were validated in a simulator using the plan found by ENHSP as a controller automaton in parallel composition with H and Hω . We can observe that HYCOMP and DREACH scale up poorly (no results of Platoon and Flight are shown for HYCOMP as it only supports constant derivatives; 0 indicates no solution found within the time budget). We attribute the poor performance of DREACH to the large size of the variables domain. HSE P, the configuration that uses actions to match observations in Hω , shows better performance than the MC tools, but still unable to solve the full suite of problems as computation times quickly ramp up for the linear and nonlinear domains. HSE Pe, however, solves all the problems. Indeed, HSE Pe would be able to scale to much larger instances. The nonlinear dynamics of the Flight domain are clearly more computationally expensive for the planner as evidenced by the reported times and a higher difficulty to scale up. The quality of the solutions found by both versions of HSE P are the same for thermostat and platoon domains. HSE P slightly outperformed HSE Pe in the flight domain where it found solutions up to 10% shorter in average for problem sizes 8 and 10. The MC tools produced plans of the same size as the best plan obtained between HSE P and HSE Pe.

6 Conclusions

This paper has shown a novel and general method to explain the observed behaviour of an HS that exhibits different control modes. Our HSE specification uses the HA formalism, which enables already existing model checking tools to tackle the problem. We, however, propose a planning-based approach that exploits the capabilities of heuristic PDDL+ planners to explore the state space and obtain good quality solutions. Our empirical evaluation shows a significant increase in performance with respect to model checking tools. In light of these results, exploring the combination of PDDL+ planning with model checking to tackle falsification problems seems to be a promising line of research.

Acknowledgments

This work is supported by the Spanish MINECO project TIN2017-88476-C2-1-R and partially supported by the EU ICT-48 2020 project TAILOR (No. 952215). Diego Aineto is partially supported by the FPU16/03184. Enrico Scala and Ivan Serina are partially supported by Regione Lombardia, Call Hub Ricerca e Innovazione, within the project "MoSoRe@Unibs-Infrastrutture e servizi per la Mobilit`a Sostenibile e Resiliente", 2020-2022 and by AIPlan4EU, a project funded by EU Horizon 2020 research and innovation programme under GA n. 101016442 (since 2021).