Platform-Aware Mission Planning with Task-Level Contracts

1 Introduction

Temporal planning is the problem of synthesizing a schedule of durative actions to reach a desired goal from an initial state, in a domain description subject to temporal constraints. A temporal planning domain, described in languages such as PDDL 2.1 [Fox and Long, 2003] and ANML [Smith et al., 2008], is deterministic, in the sense that an executable plan is associated with exactly one run.

Recently, Panjkovic et al. (2025a; 2025b) introduced the "Platform-Aware Mission Planning" (PAMP) problem, an extension to temporal planning where a mission-level temporal domain is coupled with the description of an execution platform (in the form, for example, of a timed automaton or a timed transition system) upon which mission-level plans can be executed. Notably, the platform can contain a rich set of features, may be nondeterministic, and subject to integrity constraints, so that a valid temporal plan at mission level can be associated with multiple (and possibly invalid) runs at the platform level.

A PAMP problem consists of synthesizing a valid, goalachieving temporal plan at the mission level that is at the same time guaranteed to be executable and safe w.r.t. an invariant property at the platform level. The PAMP framework integrates, while keeping them separate, (i) an easily solvable, deterministic temporal planning problem, and (ii) the non-determinism in the execution of the plan on the platform, subject to safety constraints. The algorithms proposed in [Panjkovic et al., 2025a; Panjkovic et al., 2025b] leverage the separation of the mission and platform levels by tightly combining an enumeration of temporal mission plans with a platform validity check that corresponds to a model checking problem at the platform level. Despite the effectiveness of the optimizations proposed in [Panjkovic et al., 2025a], solving a PAMP problem in its general form turns out to be significantly more challenging than classical temporal planning.

In this paper, we propose an alternative approach based on the idea of limiting the freedom in which the platform can be executed. The mission plan is no longer allowed to be freely connected to the behavioral model of a platform, with arbitrary parallel and overlapping temporal actions. Rather, the operation of the platform is restricted to a set of predefined atomic tasks, each associated with a durative action or a composition of durative actions. The tasks are atomic in the sense that they are activated sequentially and cannot overlap. Each task is associated with (i.e., abstracted into) a contract, an assumption-guarantee pair over a set of platform and timing variables. The assumptions indicate the platform-level preconditions, i.e., the set of configurations in which the task can be safely activated, while the guarantees represent the postconditions of the task. This contract view is intended to capture all the non-deterministic platform executions under restricted conditions. The PAMP problem is therefore reduced to two key subproblems. The first one, named PlatformAware Mission Planning with Task-Level Contracts (PAMPTLC), is the problem of finding a temporal plan that is valid according to the temporal planning model and that yields a robust composition of task-level contracts. The second is the problem of ensuring that the platformmodel satisfies specific requirements induced by the task contracts, which intuitively means that the relevant aspects of the platform are properly characterized in the contracts of the tasks. This ensures that a solution of PAMP-TLC is also a solution for the original PAMP problem.

The approach is structured in the following contributions. We formalize the PAMP-TLC problem in an algebraic contract framework [Incer et al., 2025], and provide an efficient algorithm for the synthesis of valid PAMP-TLC solutions that combines temporal planning and contract reasoning. We characterize the proof obligations a platform must satisfy for a PAMP-TLC solution to be a PAMP solution, and propose an automated approach to verify them on a given platform model. The approach is implemented and experimentally evaluated on a realistic case study taken from [Rouquette et al., 2023] and on several synthetic benchmarks. The comparison with the PAMP algorithm in [Panjkovic et al., 2025a] demonstrates that, despite the introduced limitations in the activation of the platform, the new approach, equipped with the proper task abstractions, retains the ability to solve all the problems in the benchmark set, while at the same time demonstrating superior performance.

Related Work. In addition to [Panjkovic et al., 2025a], which we will compare against in the rest of this paper, this work has some similarities with conformant planning [Ghallab et al., 2004], where there is no runtime observation and actions can have non-deterministic effects. To the best of our knowledge, the temporal case is not addressed in the conformant planning literature, and our setting differs in that we consider two models at different layers of abstraction. Viehmann et al. [2021] consider the problem of checking whether an abstract sequential plan can be executed on a platform modeled as a timed automaton, where the relationship between the high-level and low-level models is expressed with Metric Temporal Logic (MTL) constraints. However, this work is limited to verifying whether there exists a single platform execution compliant with the plan, while we consider plan robustness w.r.t. all possible platform behaviors. Bozzano et al. [2021] propose a formal autonomy framework integrating plan generation, plan execution, monitoring and fault detection identification and recovery that is based on symbolic model-based reasoning. The controlled system is represented as a finite-state non-deterministic planning problem, with resource estimation functions. A form of mission planning based on contracts was previously considered in [Mallozzi et al., 2023], where, given a library of components, the goal is to produce an implementation that satisfies a toplevel LTL property, expressed as a contract. In this approach, the components in the library are expressed as LTL contracts, and timing aspects are not considered. There are also several works in the literature on plan execution, where the model of the underlying environment is known, like PRS-style architectures [Ingrand et al., 1992], SkiROS [Rovida et al., 2017] and approaches based on hierarchical task-oriented refinement methods [Patra et al., 2021]. However, these works are fundamentally different from our setting as they are online methods, while we address the problem of providing safety and executability guarantees at planning time.

2 Background

In this section, we report the background notions for the rest of the paper.

Temporal Planning. We define the syntax of a temporal planning problem, borrowing from [Gigante et al., 2022].

Definition 1 (Temporal Planning Problem). A temporal planning problem Π is a tuple ⟨P,A, I,G⟩, where P is a set of propositions, A is a set of durative actions, I ⊆ P is the initial state and G ⊆ P is the goal condition. A snap (instantaneous) action is a tuple h = ⟨pre(h), eff+(h), eff-(h)⟩, where pre(h) ⊆ P is the set of preconditions and eff+(h), eff-(h) ⊆ P are two disjoint sets of propositions, called the positive and negative effects of h, respectively. We write eff(h) for eff+(h) ∪ eff-(h). A durative action a ∈ A is a tuple ⟨a⊢, a⊣, pre↔(a), [La,Ua]⟩, where a⊢ and a⊣ are the start and end snap actions, respectively, pre↔(a) ⊆ P is the overall condition, and La ∈ Q>0 and Ua ∈ Q>0 ∪ {∞} are the bounds on the action duration.

Intuitively, the solution to a planning problem is a schedule of actions, each respecting its duration bounds, such that starting from the initial state and applying the effects of every action at the right time, all action conditions are satisfied and the goal is reached in the final state. For the sake of brevity, we do not report the full planning semantics here (a complete account can be found in [Gigante et al., 2022]). We formalize the structure of a plan that will be used for our definitions.

Definition 2 (Plan). Let Π = ⟨P,A, I,G⟩ be a temporal planning problem. A plan for Π is a set of tuples π = {⟨a1, t1, d1⟩, . . . , ⟨an, tn, dn⟩}, where, for each 1 ≤ i ≤ n, ai ∈ A is a durative action, ti ∈ Q≥0 is its start time, and di ∈ Q>0 is its duration.

Definition 3 (Set of timed snap actions). A timed snap action (TSA) is a pair (t, h), where t ∈ Q≥0 and h is a snap action. Given a plan π = {⟨a1, t1, d1⟩, . . . , ⟨an, tn, dn⟩}, the set of TSAs of π is defined as: H(π) = {(t1, a1⊢), (t1 + d1, a1⊣), . . . , (tn, an⊢), (tn + dn, an⊣)}.

An important property of a planning problem is whether action self-overlapping is allowed. Gigante et al. (2022) proved that temporal planning without action selfoverlapping is PSPACE-complete, and we adopt this semantics (i.e., we disallow self-overlapping) for this paper.

Definition 4 (Action self-overlapping). A plan {⟨a1, t1, d1⟩, . . . , ⟨an, tn, dn⟩} is without self-overlapping if there exist no i, j ∈ {1, . . . , n} with i ̸= j such that ai = aj and ti ≤ tj < ti + di.

Symbolic Timed Transition Systems. To formalize the comparison between this work and [Panjkovic et al., 2025a], we report here the syntax of a symbolic timed transition system.

Definition 5 (Symbolic Timed Transition System). A (symbolic) Timed Transition System (TTS) is a tuple T = ⟨V, X , Σ, I(V ), T (V, Σ, V ′ ), Z(V )⟩, where:

• V is a set of state variables;
• X ⊆ V is a set of clock variables;
• Σ is a set of input variables;
• I(V ) is the initial condition;
• T(V,Σ, V ′ ) is the transition condition;
• Z(V ) is the invariant condition.

For brevity, we refer the reader to [Panjkovic et al., 2025a] for the formal semantics. Here, it suffices to say that a TTS models a dynamical system that performs two types of transitions: discrete transitions, where the variables in V change according to the transition relation T (V, Σ, V ′ ), where V ′ denotes the values of the variables after the transition is taken; delay transitions, where the clocks increase their values by the same quantity δ and all other variables keep their value.

Given a TTS T , there exist off-the-shelf model-checking algorithms [Cimatti et al., 2019] for proving and disproving properties expressed in Linear Temporal Logic (LTL) [Pnueli, 1977]. In this paper, we use some simple LTL checks as away to link the PAMP problem to our PAMP-TLC framework.

IO Contracts. In the following, we consider formulas of a given logic L. The logic comes with a background theory and a corresponding satisfaction relation |=. Thus, for any formula φ over a set of variables V and any assignment µ to V , we write µ |= φ to denote that φ is satisfied under the assignment µ. In this paper, we focus on the QF LRA (Quantifier-Free Linear Real Arithmetic) logic. In essence, QF LRA formulas are Boolean combinations of inequalities between linear polynomials over real variables: a term is of the form ∑i aixi, where every xi is a real variable and every ai is a rational constant; an atom is either a Boolean variable or an expression of the form φ ▷◁ c, where φ is a term, ▷◁ ∈ {>, <, ≥, ≤, ̸=, =}, and c is a rational constant; finally, a formula in QF LRA is a conjunction (∧), disjunction (∨) or negation (¬) of atoms. Given a formula φ, we denote with Vars(φ) the set of variables appearing in φ. An assignment µ : Vars(φ) → B∪R to the variables of φ satisfies φ, denoted µ |= φ, if it evaluates φ to true.

In this setting, an Input-Output (IO) Contract is a pair of formulae, denoting an input assumption on some variables I and a guarantee defined over I and output variables O. The following definition adapted from [Incer et al., 2025] provides the syntax for an IO contract.

Definition 6 (IO Contract). Let V = VB ∪ VR be a finite set of variables with domain B∪R. An IO contract in QF LRA is a tuple C = (I,O, a, g), where I,O ⊆ V are disjoint sets of input and output variables respectively, and a, g are QF LRA formulas representing the assumptions and guarantees of C respectively. The assumptions of IO contracts only depend on input variables (Vars(a) ⊆ I), and the guarantees only depend on input and output variables (Vars(g) ⊆ I ∪O).

An environment of a contract C = (I, O, a, g) is a set of assignments E to the variables in I such that for each µE ∈ E, µE : I → B ∪ R, we have that µE |= a. An implementation is a set of assignments M to the variables in I ∪ O such that for each µM ∈ M, µM : I ∪ O → B ∪ R, we have that µM |= (a → g).

We define the notions of refinement for IO contracts, and the operations of composition, quotient and merging. We adapt the definitions provided in [Benveniste et al., 2018; Incer et al., 2025] to the case of IO contracts in QF LRA.

Definition 7 (Refinement). Given two contracts C1 = (I1, O1, a1, g1) and C2 = (I2, O2, a2, g2), we say that C1 is a refinement of C2 (written C1 ≤ C2), or equivalently that C2 is a relaxation of C1, if every environment of C2 is an environment of C1 and every implementation of C1 is an implementation of C2: C1 ≤ C2 iff (a2 → a1) ∧ ((a1 → g1) → (a2 → g2)) is valid.

The operation of composition returns a specification for a system obtained by composing implementations of the contracts being composed.

Definition 8 (Composition). Let C1 = (I1,O1, a1, g1) and C2 = (I2,O2, a2, g2) be two IO contracts, such that I1 ∩ O2 = ∅. A composition of C1 and C2 is a contract Cc = (Ic, Oc, ac, gc) such that:

1. Ic = (I1 ∪ I2) \ O1;
2. Oc = O1 ∪O2;
3. Combining respective implementations of each contract yields an implementation for the composition: ((a1 → g1) ∧ (a2 → g2)) → (ac → gc) is valid;
4. Combining an environment for the resulting composition with an implementation for C2 yields an environment for C1 and vice-versa: (ac ∧ (a2 → g2)) → a1 and (ac ∧ (a1 → g1)) → a2 is valid.

The quotient operation determines the specification of a subcomponent which, when composed with the provided contract, refines a top-level specification.

Definition 9 (Quotient). Let C1 = (I1,O1, a1, g1) and C2 = (I2,O2, a2, g2) be two IO contracts, such that I1 ∩ I2 = ∅ and O2 ⊆ O1. A quotient of C1 by C2 is a contract Cq = (Iq, Oq, aq, gq) such that:

1. Iq = I1;
2. Oq = (O1 \ O2) ∪ I2;
3. The composition of the quotient with the divisor is a refinement of the dividend: Cq ∥ C2 ≤ C1.

The composition and quotient operations can be implemented in several ways [Benveniste et al., 2018; Incer et al., 2025]. In [Benveniste et al., 2018] the composition between two contracts C1 and C2 is defined as the Greatest Lower Bound w.r.t. refinement order of all the contracts that satisfy Definition 8 (i.e. the largest contract that is a refinement of all the contracts that are a composition of C1 and C2), while the quotient is the Least Upper Bound of all the contracts satisfying Definition 9 (i.e. the smallest contract that is a relaxation of all the contracts that are a quotient of C1 by C2). Several approaches compute a relaxation or refinement of the exact composition or quotient respectively, for efficiency or representational reasons [Incer et al., 2025]. In this paper, we assume that we are given a procedure that computes any composition between two contracts satisfying Definition 8 (denoted with C1 ∥ C2), and a procedure computing the quotient of two contracts satisfying Definition 9 (denoted with C1/C2). We do not make any assumption on the strength of the computed contracts, and we will discuss in Section 4 the impact of this on the overall approach.

One additional operation, merging, is used to fuse into a single contract multiple contracts that describe distinct aspects of an object under specification.

Definition 10 (Merging). Let C1 = (I1,O1, a1, g1) and C2 = (I2, O2, a2, g2) be two IO contracts. The merge of C1 and C2 is a contract C1 · C2 = (Im,Om, am, gm) such that Im = I1 ∪ I2, Om = O1 ∪ O2, am = a1 ∧ a2, and gm = g1 ∧ g2.

3 PAMP with Task-Level Contracts

In this section, we present the formalization of the PlatformAware Mission Planning with Task-Level Contracts (PAMPTLC) problem. We couple a high-level temporal planning problem with a low-level model defined using Input-Output (IO) Contracts. In our model, every action of the planning problem and every allowed parallel interleaving of actions is modeled with a contract, describing the assumptions and the guarantees of applying these high-level events on the platform and environment, in terms of low-level variables. Note that we assume a finite set of allowed parallel compositions of planning actions, because at this level of abstraction, composing the contracts of parallel tasks highly depends on the platform specifics.

The problem that we consider is the generation of a solution plan for the planning problem, such that for every possible outcome of its execution, as described by the contracts associated to the actions, a safety property is maintained.

Example. Consider a setting in which a spacecraft needs to take some observations of an asteroid. We have a very simple temporal planning problem with durative actions SBO (Small Body Observation) and CHARGE. The SBO action sets a boolean variable obs to true, meaning that the asteroid was observed, and the goal of the planning problem is to have obs set to true. The CHARGE action affects some other variables which are not related to the preconditions of SBO. Suppose that these actions are associated to the following contracts, modeling the fact that there is a low-level soc variable (state of charge), and that SBO and CHARGE have assumptions and guarantees on it:

• cSBO = (ISBO,OSBO, aSBO, gSBO), where
• ISBO = {t1, t2, soc}
• OSBO = {soc′ }
• aSBO := (t2 - t1 ≥ 0) ∧ (soc ≥ 3(t2 - t1))
• gSBO := 2(t2 - t1) ≤ soc - soc′ ≤ 3(t2 - t1)
• cCHARGE = (ICHARGE,OCHARGE, aCHARGE, gCHARGE), where
• ICHARGE = {t1, t2, soc}
• OCHARGE = {soc′ }
• aCHARGE := (t2 - t1 ≥ 0) ∧ (soc ≥ 0)
• gCHARGE := 2 3 (t2 - t1) ≤ soc′ - soc ≤ 2(t2 - t1)

In both contracts, the input variables t1 and t2 denote the starting time and the ending time of the action, respectively. Basically, cSBO specifies that the duration of the action must be non-negative, and that the initial state of charge must be above 3(t2 - t1). The guarantee after applying the SBO action is that the decrease in the state of charge will be between 2(t2-t1) and 3(t2-t1). Instead, the contract cCHARGE guarantees that after applying the CHARGE action, the state of charge will be increased by an amount between 23 (t2 - t1) and 2(t2 - t1). The safety property that we consider is that the state of charge cannot go below 20: soc ≥ 20.

Now, we formally define the overall framework and the problem that we are considering. Let Π = ⟨P,A, I,G⟩ be a temporal planning problem. Let SeqA denote the set of all the totally ordered sequences of snap actions from A. Let V be a finite set of Boolean and real variables, and let V ′ be the set of primed variables from V . Let T = {τ1, τ2, . . .} be a set of time variables with domain in R. Let C be a set of IO contracts defined on V , V ′ and T, where the input variables are from V ∪ T and the output variables are from V ′ . Given a contract c = (I,O, a, g) ∈ C, we denote with Tc ⊆ T the set of time variables appearing in I.

In our formalization, we associate with a partial function λ a contract to each durative action, and to each allowed parallel interleaving of actions, which is represented by a sequence of start and end snap actions (a single durative action A is represented by the sequence ⟨A⊢, A⊣⟩, where A⊢ and A⊣ are the start and end snap actions of A respectively).

Formally, let λ : SeqA ⇀ C be a partial function associating sequences of snap actions to contracts in C, such that if λ(⟨h1, . . . , hn⟩) = c then Tc = {τ1, . . . , τn} ⊆ T (c has one time variable for each snap action in the sequence).

Given a plan π, we want to identify the maximal groups of parallel actions appearing in it; the plan π is then a sequence of these groups, each associated to a contract by the function λ. We formalize this concept as follows. Let π = {⟨a1, t1, d1⟩, . . . , ⟨an, tn, dn⟩} be a plan for Π. We say that a value t ∈ R is an empty time in π if there doesn't exist i ∈ {1, . . . , n} such that ti ≤ t ≤ ti + di. We indicate with ρπ = ⟨(t′1 , e1), . . . , (t′2n , e2n)⟩ the ordered sequence of timed snap actions of π, with t′i < t′i+1 for all i ∈ {1, . . . , 2n - 1}. We say that σπ = ⟨(t′i , ei), . . . , (t′j , ej)⟩ is a maximal overlapping subsequence of ρπ if: 1) there is no empty time in [t′i , t′j ]; 2) t′i -ε and t′j +ε are empty times for every ε ∈ (0, δ], for a δ > 0. We indicate with Σπ = ⟨σπ 1 , . . . , σπ r ⟩, where σπ i = ⟨(t1i , e1i ), . . . , (t|σπ i | i , e|σπ i | i )⟩, the sequence of maximal overlapping subsequences of π.

Given a contract c = (I, O, a, g) with Tc = {τ1, . . . , τn}, we denote with [c]ij the contract that is obtained by renaming the variables τ1, . . . , τn to τi, . . . , τi+n-1, all the variables v ∈ I \ Tc to vj and all the variables v ∈ O to vj+1.

Now, we can define the top-level contract associated to a plan π by composing the contracts associated to the maximal overlapping subsequences in Σπ . Before performing the composition, we set the time variables appearing in the contracts to the values specified in the plan (by merging the contracts with a contract encoding the specific timings of the snap actions in π), and we rename the variables in such a way that the output variables of one contract become the input variables of the next contract in the sequence.

Formally, we define the contract cπλ associated with π and the mapping function λ, as cπλ = [Φ1 ·∆1]k1 1 ∥ . . . ∥ [Φr ·∆r]kr r , where ki = 1 + ∑i-1 j=1 |σπ j |, Φi = λ(σπ i ), and ∆i = (Ii,Oi, ai, gi) is an IO contract such that Ii = {τ1, . . . , τ|σπ i |}, Oi = ∅, ai = ∧|σπ i | j=1 τj = tji and gi = ⊤.

Example. Consider the plan π = {⟨CHARGE, 0, 15⟩, ⟨SBO, 16, 10⟩}. In this case, since there is no parallelism, we simply have Σπ = ⟨σπ 1 , σπ 2 ⟩, where σπ 1 = ⟨(0, CHARGE⊢), (15, CHARGE⊣)⟩ and σπ 2 = ⟨(16, SBO⊢), (26, SBO⊣)⟩. We have Φ1 = λ(σπ 1 ) = cCHARGE and Φ2 = λ(σπ 2 ) = cSBO. By merging with ∆1 and ∆2, we add the assumptions (t1 = 0 ∧ t2 = 15) and (t1 = 16 ∧ t2 = 26) to cCHARGE and cSBO respectively. In the contract [Φ1 ·∆1]k1 1 , we perform the renamings soc ↦→ soc1 and soc′ ↦→ soc2, while in the contract [Φ2 ·∆2]k2 2 we perform the renamings t1 ↦→ t3, t2 ↦→ t4, soc ↦→ soc2 and soc′ ↦→ soc3. One possible contract cπλ = (I π λ , Oπ λ , aπλ , gπ λ ) that can be obtained by the composition (satisfying Definition 8) is the following:

• I π λ = {t1, t2, t3, t4, soc1}
• Oπ λ = {soc2, soc3}
• aπλ := (t1 = 0) ∧ (t2 = 15) ∧ (t3 = 16) ∧ (t4 = 26) ∧
• gπ λ := ( 23 (t2 - t1) ≤ soc2 - soc1 ≤ 2(t2 - t1)) ∧ (2(t4 - t3) ≤ soc2 - soc3 ≤ 3(t4 - t3))

Finally, we define the PAMP-TLC problem, where we want to generate a solution plan π for a temporal planning problem Π, such that the resulting top-level contract cπλ refines a contract cS encoding the desired safety property φS. In the following definition, we use the notation [φ]i, where φ is a formula in V , to denote the formula obtained by renaming every v ∈ Vars(φ) to vi.

Definition 11 (PAMP-TLC). Let V be a set of Boolean and real variables, and let V ′ be the set of primed variables from V . Let T = {τ1, τ2, . . .} be a set of time variables with domain R. A Platform-Aware Mission Planning with Task-Level Contracts (PAMP-TLC) problem is a tuple Υ = ⟨Π, C, λ, φI , φS⟩, where Π = ⟨P, A, I, G⟩ is a temporal planning problem, C is a set of IO contracts defined on variables V , V ′ and T, λ : SeqA → C is a function associating sequences of snap actions to contracts in C, φI(V ) is a formula describing the initial state, and φS(V ) is a safety property. A solution for Υ is a plan π such that:

1. π is a valid solution plan for Π;
2. cπλ ≤ cS, where cS = (IS,OS, aS, gS) is the following IO contract:
3. IS = {v1 : v ∈ V };
4. OS = {vi : v ∈ V, 1 < i ≤ |Σπ | +1};
5. aS := [φI]1;

Example. Consider an initial condition φI := 40 ≤ soc ≤ 100, and the safety property φS := soc ≥ 20. The plan in which only the SBO action is applied is invalid, as starting from this initial state the contract cSBO does not guarantee that φS is satisfied in the end, as shown in Fig. 1. On the other hand, the plan in Fig. 2 where we apply the CHARGE action before the SBO action is a valid solution for the PAMP-TLC problem, as the contract resulting from the composition (previously shown) refines the following contract cS = (IS, OS, aS, gS) encoding the safety property φS:

• IS = {soc1}
• OS = {soc2, soc3}
• aS := 40 ≤ soc1 ≤ 100
• gS := (soc1 ≥ 20) ∧ (soc2 ≥ 20) ∧ (soc3 ≥ 20)

Relationship between PAMP-TLC and PAMP. The Platform-Aware Mission Planning (PAMP) problem [Panjkovic et al., 2025a] considers a similar setting, but the lowlevel layer is modeled with an explicit timed-transition system (TTS). Every snap action appearing in a plan represents a command that triggers at the scheduled time a special transition in the platform associated to that event. In the time between two high-level commands, the platform is assumed to be non-deterministic, and it can perform internal transitions. The PAMP problem consists in generating a solution plan π for a temporal planning problem, such that it is guaranteed to be safe and executable for any non-deterministic platform behavior compliant with π. The executability notion is formalized by stating that for every plan prefix, for every state r of the platform reachable by applying the plan commands in that prefix at the prescribed times, if the time in r equals the time of the next snap action in the plan, the corresponding transition can be taken in r. The safety notion is defined by stating that every platform state r reachable in a trace compliant with the plan must satisfy a certain safety property φ.

If there is a proper abstraction relationship between the contracts associated to the planning actions and the TTS modeling the platform, we can guarantee that any plan that is a solution for a PAMP-TLC problem, is also a solution for the PAMP problem sharing the same planning problem. Semiformally, given a contract c = (I,O, a, g) with time variables Tc = {τ1, . . . , τn}, associated to a sequence of snap actions ϱ = ⟨e1, . . . , en⟩, we say that c is an abstraction of the execution of ϱ on TTS T with bound L and safety property φ if, in the TTS T ′ obtained from T by setting the initial condition to the assumptions of c, the following three proof obligations hold for any initial state s0 of T ′ : (1) ϱs0 = ⟨(s0(τ1), e1), . . . , (s0(τn), en)⟩ is executable on T ′ ; (2) in any run compliant with the execution of ϱs0 on T ′ , the guarantees of c hold in the interval [s0(τn), s0(τn) +L]; (3) in any run compliant with the execution of ϱs0 on T ′ , if the safety property φ holds in s0 and at s0(τn), then it holds up to s0(τn) + L.

Intuitively, the first condition can be used to prove that a solution for PAMP-TLC is executable on T , as all the actions appearing in the plan will be executable considering that the assumptions of the respective contracts will hold at their start; the second condition guarantees that the safety property will

1 procedure CONTRACTPLANNING(Π, C, λ, φI , φS) 2 bad seqs = {} 3 while True do 4 πSTN ← PLAN(Π, bad seqs) 5 pass, bad seqsπ , π ← CHECK(C, λ, πSTN, φI , φS) 6 if pass then return π 7 else bad seqs ← bad seqs ∪ bad seqsπ 8 procedure CHECK(C, λ, πSTN, φI , φS) 9 σπ 1 , . . . , σπ r ←maximal subseqs(πSTN) 10 for i = 1 to r do 11 Φi ← λ(σπ i ) 12 ∆i ← BUILDDURATIONSCONTRACT(πSTN, i) 13 if i == 1 then 14 c1 ← [Φ1 · ∆1]k1 1 15 else 16 ci ← ci-1 ∥ [Φi · ∆i]ki i 17 ciS ← BUILDSAFETYCONTRACT(φI , φS, i) 18 ciQ = (I iQ, OiQ, aiQ, giQ) ← ciS/ci 19 if giQ is satisfiable then 20 if i == r then 21 return true, ∅, GETPLAN(giQ, πSTN) 22 else continue 23 else 24 j ′ ← ∑ij=1 |σπ j | 25 bad seqsπ ← (e1, . . . , ej′ ) ∪ BADSUBS(πSTN, i) 26 return false, bad seqsπ , ∅

hold on the platform at the ending times of the actions, and in the time between two actions (we are assuming that we are given an upper bound L on the maximum distance between two actions); the third condition guarantees that the safety property is preserved during the execution of each action.

The full formalization and proof of this result, as well as the presentation of the necessary formal background on the PAMP problem, is available in the additional material.

The first two proof obligations can be checked by applying directly the validation subroutine of the algorithm for solving the PAMP problem [Panjkovic et al., 2025a], with a safety property ψ expressing the fact that when the global time is in [s0(τn), s0(τn) + L], the guarantees of c hold: ψ := (s0(τn) ≤ γ ≤ s0(τn) + L) → g|s0 , where γ is the global clock of T ′ (denoting the time since the start), and g|s0 is the formula obtained by substituting every v ∈ V in g with s0(v), and every v′ ∈ V ′ in g with v. The third proof obligation can be checked with the following LTL property, specifying that if φ holds in the initial state, and eventually in the run the global time is s0(τn) and φ holds, then in every state of the run with global time up to s0(τn) + L, φ holds: φ ∧ F (γ = s0(τn) ∧ φ) → G(γ ≤ s0(τn) + L → φ).

4 Solving PAMP-TLC

In this section, we present an approach for solving the PAMPTLC problem. A temporal planner is used to solve the planning problem and enumerate candidate solution plans. In order to check that a plan satisfies the low-level safety property, we compute the top-level contract associated to the plan by composing the contracts of each action (and each allowed interleaving) in the plan, and then by computing the quotient between a contract encoding the safety property and the plan contract. This determines (if it exists) a scheduling of the actions that satisfies the safety property.

For temporal planning, we assume a sound planner that can return plans in the form of Simple Temporal Networks (STN) [Dechter et al., 1991]: a solution πSTN is characterized by a fixed ordering of snap actions e1, . . . , en, where each snap action ei is associated to a time variable ti representing the moment in which it is applied, and a set of constraints between time variables enforcing the duration constraints and the ordering. We assume that the planner search can avoid plans containing a given set of actions sequences. In principle, any heuristic-search planner can be instrumented to satisfy these requirements by using plan de-ordering methods [B¨ackstr ¨om, 1998] and by checking the prefixes of plans for pruning.

The approach is detailed in Algorithm 1. First, the planning problem Π is solved, obtaining a set of solution plans πSTN characterized by a fixed sequence of snap actions e1, . . . , en and a set of constraints between the time variables t1, . . . , tn associated to them. Then, the solution πSTN, and the formulas φI and φS encoding the initial state and safety property are passed to the CHECK procedure. In the CHECK procedure, we first determine the sequence σπ 1 , . . . , σπ r of maximal overlapping subsequences of πSTN. We iterate over all prefixes i ∈ {1, . . . , r}, and we consider the contract Φi = λ(σπ i ) that is associated to σπ i . We compute the contract ∆i, whose assumption is the conjunction of all the constraints in πSTN (expressed as QF LRA formulas) containing time variables in {t1, . . . , ti}, and whose guarantee is ⊤. We merge these contracts and rename the resulting contract obtaining [Φi ·∆i]ki i , which is such that the input and output variables have index i and i + 1 respectively, and the time variables start with index ki = 1 + ∑i-1 j=1 |σπ j |, i.e. the next index after the time variables of the previous contracts in the sequence. We then compose this contract with the contract considered in the previous step: ci = ci-1 ∥ [Φi ·∆i]ki i . We compute the contract ciS encoding the safety property for the first i steps: the assumption is [φI]1 and the guarantee is ∧i+1 j=1 [φS]j. We then compute the quotient ciQ = ciS /ci, whose output variables are the time variables for the subsequence of the plan σπ 1 , . . . , σπ i . By the properties of the quotient operation, the values for the time variables satisfying the guarantees of ciQ are such that ci ≤ ciS . If giQ is satisfiable, we extract a value for the time variables, for which it is guaranteed that the plan π satisfies the safety property φS. Otherwise, the current prefix of snap actions is not schedulable in a way that guarantees the safety property, and therefore we return to the planner this invalid prefix, which can then be used for pruning in the continuation of the planning search. In addition to that, we analyze this prefix with the BADSUBS procedure, to determine whether there is a shorter subsequence that is guaranteed to violate the safety property, which is a stronger information that the planner can learn. For an invalid prefix ⟨e1, . . . , ei⟩, we consider subsequences ⟨ej , . . . , ei⟩, where j goes from i to 1, and we determine whether the composition of the respective contracts can refine the safety contract, starting from any initial state. If that is not the case, we avoid in the planning search every plan containing such a subsequence.

Theorem 1. Let Υ = ⟨Π, C, λ, φi, φS⟩ be a PAMPTLC problem, and let π be a plan returned by CONTRACTPLANNING(Π, C, λ, φI, φS). Then, π is a valid solution for Υ.

Proof. (Sketch) We show that π satisfies Definition 11. (1) Let πSTN be the last plan in STN form returned by PLAN(Π, bad seqs). Because of the soundness of the planner, every plan that has the specified ordering of snap actions and a timing for each snap action that satisfies the STN constraints of πSTN is a valid solution for Π. The plan π is returned by GETPLAN(gQ, πSTN) when iteration i = r of the CHECK(C, λ, πSTN, φI, φS) procedure is reached. Since i = r, the assumptions of ci contain all the constraints in πSTN. Since cQ = cS/ci, by the properties of the quotient operation the value for the timings extracted from the guarantee gQ of cQ will satisfy the assumptions of ci, which include the STN constraints. Since the ordering of the snap actions is preserved, we can conclude by the planner soundness that π is a solution for Π. (2) Since π is obtained by extracting a value for the timings of the snap actions from gQ, we have that cπλ ≤ cQ ∥ cr. By the properties of the quotient operation, we have that cQ ∥ cr ≤ cS. Therefore, cπλ ≤ cS.

The specific way in which the composition and quotient operations are implemented can have an impact on the performance of the algorithm (while the soundness is always preserved): looser implementations can lead to the invalidation of plans that could have passed the refinement check with the safety contract, if a tighter implementation was used.

5 Experimental Evaluation

We developed the presented approach in a solver written in Python based on Pacti, a Python framework for carrying out compositional system analysis and design by reasoning on IO Contracts [Incer et al., 2025]. For temporal planning we use the TAMER planner [Valentini et al., 2020]. Finally, for checking the contracts w.r.t. a platform modeled as a TTS we use NUXMV [Cimatti et al., 2019], a symbolic model checker that is able to prove temporal properties of TTSs.

We experimentally evaluated the new approach against the PAMP implementation in [Panjkovic et al., 2025a] both on the JPL case-study modeled as IO contracts presented in [Rouquette et al., 2023], where we added two versions of the planning problem to show our synthesis capabilities, and a simple platform model compliant with the contracts to compare against PAMP. Moreover, we added the contract layer to the benchmark set used in [Panjkovic et al., 2025a].

All the experiments were performed on a cluster of identical machines with AMD EPYC 7413 24-Core Processor and running Debian GNU/Linux 13. We used a timeout of 14400 seconds and a memory limit of 20GB.

Table 1 reports the coverage table comparing our approach PAMP-TLC with PAMP. It reports the number of solved instances for each domain, the average number of abstractionrefinement loops that were necessary in each domain before finding a valid solution plan, and the time required by PAMPTLC with the additional check that each contract is a correct abstraction w.r.t. the platform model. The results show that PAMP-TLC generally solves more instances compared to PAMP, and with faster solving times, as highlighted by the cactus plot in Fig. 3. The number of required iterations for validating the plans produced by the planner is also lower for PAMP-TLC. Moreover, the cost of checking that a contract is a correct abstraction for the platform models is very low, between 5 and 30 seconds for the considered benchmarks.

These results highlight that by having a more abstract representation of the platform, using contracts to model the effect of applying each planning action on the controlled platform, we can generate robust plans more effectively, compared to reasoning on the platform model directly. With the additional checking that each contract is a correct abstraction of the execution of the corresponding action on the platform, the returned plans are also valid solutions for the PAMP problems, and the cost of these checks is shown to be very low.

6 Conclusions

In this paper, we presented a novel approach to tackle the Platform-Aware Mission Planning (PAMP) problem, by exploiting a Task-Level abstraction provided in the form of Input-Output contracts. We showed a planning schema that finds plans that are valid according to this abstraction, and we defined the proof obligations that need to be checked on a concrete platform for the plan to be valid according to the PAMP semantics. As future work, we plan to explore the problem of synthesis for the contracts from a prototypical platform implementation.

Acknowledgments

Andrea Micheli has been partially supported by the STEP-RL project funded by the European Research Council under GA n. 101115870. The initial collaboration for this paper was established during the Contract Languages Workshop at the Lorentz Center (March 2024).