Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications

1 Introduction

Markov decision processes (MDPs) are a widely used formalism to model sequential decision-making problems for scenarios where there is inherent uncertainty about a system's evolution. In general, planning for MDPs is performed by defining a reward structure over the model, and using dynamic programming techniques such as value or policy iteration [Puterman, 1994] to generate a policy that maximises the cumulative discounted reward over an infinite horizon. This approach has the drawback of requiring the designer to map the planning goal into a reward structure over the MDP, which can be quite cumbersome and error-prone.

Thus, in recent years, there has been increasing interest in the use of higher-level formalisms to specify the planning problems, in order to allow the designer to tackle intricate goal behaviours more naturally. In particular, linear temporal logic (LTL) [Pnueli, 1981] has been proposed as a suitable specification language, due to it being a powerful and intuitive formalism to unambiguously specify a variety of tasks. Furthermore, algorithms and tools exist to generate provably correct policies from an MDP model of the system and an LTL task specification. These approaches build upon techniques from the field of formal verification, in particular, probabilistic model checking, which provides tools to reason not just about the probability of satisfying an LTL specification, but also other quantitative metrics using cost (or reward) functions. These might represent, for example, execution time or energy consumption.

In this paper, we are interested in generating policies that minimise the undiscounted expected cumulative cost 1 to achieve a task specified in the co-safe fragment of LTL (i.e., a task that can be completed in a finite horizon). Our novel contribution is to generate cost-optimal policies for tasks that cannot be achieved with probability one in the model (i.e., there is some probability that part of the LTL specification cannot be achieved). Defining cost-optimal policies for such tasks presents an additional challenge as, in general, the undiscounted cumulative cost calculation will not converge. Furthermore, we tackle the question of what to do when the task becomes unsatisfiable during execution. In many cases, even if the probability of satisfying the overall task is zero, it is still possible to fulfil part of it. An illustrative example is a robot that needs to navigate to every office in a building to perform security checks. During execution some doors might be closed, making offices inaccessible. This will make the overall task unsatisfiable, yet we still want the robot to check as many offices as it can.

To allow this partial task satisfaction, we define a task progression metric for co-safe LTL formulas, which can be encoded as a reward function on the MDP. Using this, we show that the problems of (i) maximising the probability of satisfying a co-safe LTL formula; (ii) maximising the task progression reward (i.e., fulfilling as much of the formula as possible); and (iii) minimising a cost function while performing (i) and (ii) can be solved independently by standard techniques in a trimmed product MDP. As there is a trade-off between these problems, we apply multi-objective probabilistic model checking techniques [Forejt et al., 2011b] to find the best policy for the three objectives, in decreasing order of priority. We also describe how to analyse the resulting policy to calculate conditional expectations such as expected cost to success or expected cost to failure. This analysis provides extra information about the policy that can be used to, for example, monitor execution, or inform a higher-level task scheduler, e.g., [Mudrova and Hawes, 2015]. Finally, we evaluate the approach on the illustrative example described above.

1 Our goal is to provide meaningful formal guarantees on the system's performance, e.g., expected time for completion. For such properties, following the more typical approach of optimising the cumulative sum using a discount factor strips the optimisation result of a well-defined meaning.

2 RelatedWork

Finding cost-optimal policies for MDPs using LTL specifications has been tackled in several ways. [Svoreˇnov´a et al., 2013; Ding et al., 2014] study the problem of maximising the probability of satisfying a LTL specification, while minimising the long-term average cost to pass between two states that satisfy an "optimising" atomic proposition, which must be visited infinitely often. In [Lacerda et al., 2014], cost-optimal policies for co-safe LTL are generated, and a mechanism for the dynamic addition of tasks during execution is presented. In these cases, the cost minimisation is done only over states where the probability of satisfying the specification is one. Conversely, [Ulusoy et al., 2012; Cizelj and Belta, 2014; Wolff et al., 2013; Lahijanian et al., 2012] deal with maximising the probability of satisfying temporal logic specifications but cost-optimality is not taken into account.

Other work on policy generation for MDPs with temporal logic specifications have focused on using the more traditional approach of finding policies that maximise discounted cumulative rewards over an infinite horizon, while constraining such policies to the class that satisfies a set of "until" specifications [Teichteil-K¨onigsbuch, 2012a; Sprauel et al., 2014]. In these works, the temporal logic constraints are disconnected from the reward structure. This means that, in general, no optimal policies exist for such a problem. However, the authors prove that one can always build randomised policies that achieve a notion of ϵ-optimality. In our work, the main focus is the LTL specification, and the generation of cost-optimal policies that maximise its probability of satisfaction. This makes our class of optimal policies simpler: given that we prioritise maximisation of the probability of satisfaction over minimisation of the expected cost, the class of deterministic finite-history policies suffices to solve our problem.

There has also been work on generation of cost-optimal policies for specifications where the probability of success is not one. [Teichteil-K¨onigsbuch, 2012b; Kolobov et al., 2012] present approaches to generate cost-optimal policies to reach a target state, in the presence of unavoidable dead ends, i.e., states which cannot be avoided with probability one from the initial state, and for which the probability of reaching the target is zero. Our work extends these approaches by focusing on co-safe LTL, instead of simpler single-state reachability. This fact requires the construction of a product MDP from the original model and the co-safe LTL specification, and also introduces the notion of partial satisfiability, which is not present when the goal is reaching a single state. [Ding et al., 2013] present an approach, based on constrained MDPs, to generate cost-optimal policies for co-safe LTL, where the probability of satisfying the specification is kept above a threshold. Contrary to our approach, this requires the threshold for probability of satisfaction to be provided by the designer beforehand, and does not include the notion of partial task specification.

In terms of dealing with the unsatisfiability of temporal logic specifications during execution, [Tumova et al., 2013; Castro et al., 2013] deal with the generation of controllers that only violate sets of safety rules for the shortest possible amount of time as possible. [Maly et al., 2013] also defines a metric for task progression for co-safe LTL, and generates plans that satisfy as much of the specification as possible. Contrary to our work however, the focus of these works is on controlling a hybrid model of the system, thus they have no notion of probabilistic outcomes. Our contribution goes beyond these previous works by both dealing with the partial satisfaction of LTL and doing this in a cost-optimal manner.

3 Preliminaries

3.1 Markov Decision Processes

We model systems using Markov decision processes (MDPs) with atomic propositions labelling states. An MDP is a tuple M = ⟨S, s, A, δM, AP, Lab⟩, where: S is a finite set of states; s ∈ S is the initial state; A is a finite set of actions; δM ∶ S×A×S → [0, 1] is a probabilistic transition function, where ∑s′ ∈S δM(s, a, s′ ) ∈ {0, 1} for all s ∈ S, a ∈ A; AP is a set of atomic propositions; and Lab ∶ S → 2AP is a labelling function, such that p ∈ Lab(s) iff p is true in s ∈ S.

We define the set of enabled actions in s ∈ S as As = {a ∈ A ∣ δM(s, a, s′ ) > 0 for some s′ ∈ S}. An MDP model represents the possible evolutions of the state of a system: in each state s, any of the enabled actions a ∈ As can be selected and the probability of evolving to a successor state s′ is then δM(s, a, s′ ). An infinite path through an MDP is a sequence σ = s0 a0→ s1 a1→ . . . where δM(si, ai, si+1) > 0 for all i ∈ N. A finite path ρ = s0 a0→ s1 a1→ ... an-1 → sn is a prefix of an infinite path. We denote the sets of all finite and infinite paths of M starting from state s by FPathM,s and IPathM,s.

The choice of action to take at each step of the execution of an MDP M is made by a policy, which can base its decision on the history ofMup to the current state. Formally, a policy is a function π ∶ FPathM,s → A such that, for any finite path σ ending in state sn, π(σ) ∈ Asn . Important classes of policy include those that are memoryless (which only base their choice on the current state) and finite-memory (which need to track only a finite set of "modes"). The set of all policies of MDP M is denoted by ΠM.

Under a particular strategy π for M, all nondeterminism is resolved and the behaviour of M is fully probabilistic. Formally, we can represent this using an (infinite) induced discrete-time Markov chain, whose states are finite paths of M. This leads us, using a standard construction [Kemeny et al., 1976], to the definition of a probability measure Pr πM,s over the set of infinite paths IPathM,s, which allows us to determine the probability of certain events holding under policy π. For an event b ∶ IPathM,s → {0, 1}, we write Pr πM,s (b) for the probability of b holding under π. Given a (measurable) function f ∶ IPathM,s → R, we can define the expected value EπM,s (f ) of f with respect to the probability measure Pr πM,s . We can then consider the maximum probabilities or expected values over all policies: Prmax M,s (b) = supπ PrπM,s (b) and Emax M,s (f) = supπ EπM,s (f), respectively. Minimum values P rmin M,s (b) or Emin M,s (f) are defined analogously.

The probabilistic reachability problem is the problem of calculating Prmax M,s (reachS′), along with the corresponding optimal policy. Given S′ ⊆ S, we define the event of reaching a state in S′ as reachS′ ∶ IPathM,s → {0, 1} where reachS′ (s0 a0→ s1 a1→ ...) = 1 iff si ∈ S′ for some i. The expected cumulative reward problem is the problem of calculating Emax M,s (cumul r), along with the corresponding optimal policy. Let r ∶ S ×A → R≥0 be a reward structure over M. We define the cumulative reward cumulr ∶ IPathM,s →R≥0 as cumulr(s0 a0→ s1 a1→ ...) = ∑∞i=0 r(si, ai). Emin M,s (cumul r) is defined analogously, and in this case we write c instead of r, and call it a cost structure.

We can solve the probabilistic reachability and expected cumulative reward problems by using standard MDP algorithms such as value or policy iteration [Puterman, 1994] (which for these problems yield memoryless policies). Note that for cumulative rewards, the expected value might not converge. Thus, we first perform a graph analysis to identify states for which the reward is infinite [Forejt et al., 2011a].

In this paper, we also consider multi-objective properties, which optimise two or more distinct objectives, such as the probability of an event or the cumulative value of a cost or reward structure. To mix objective values, it is common to consider their Pareto set. However, as we need to prioritise certain values (to favour task completion over cost incurred, for example) our approach uses constrained queries, such as:

which maximises expected cumulated reward over all policies for which the probability of reaching S′ is at least p:

3.2 Syntactically Co-Safe Linear Temporal Logic

Linear temporal logic (LTL) is an extension of propositional logic which allows us reasoning about infinite sequences of states. It was developed as a means for formal reasoning about concurrent systems [Pnueli, 1981], and provides a convenient and powerful way to formally specify a variety of qualitative properties. In this work, we use the syntactically co-safe class of LTL formulas. Co-safe LTL formulas ϕ over propositions AP are defined using the following grammar:

The X operator is read "next", meaning that the formula it precedes will be true in the next state. The U operator is read "until", meaning that its second argument will eventually become true in some state, and the first argument will be continuously true until this point. See, e.g., [Pnueli, 1981] for the formal semantics of the logic.

Given an infinite path σ, we write σ ⊧ ϕ to denote that σ satisfies formula ϕ. Furthermore, we write Pr max M,s (ϕ) to denote the maximum probability of satisfying ϕ from s in M. It is known that this problem can be reduced to a reachability problem in a product MDP [Vardi, 1985].

Even though their semantics is defined over infinite sequences, co-safe LTL formulas always have a finite good prefix [Kupferman and Vardi, 2001]. Given an LTL formula ϕ and an infinite sequence of sets of atomic propositions w = w0w1... ∈ (2AP )ω such that w ⊧ ϕ, we say w has a good prefix if there exists n ∈ N for which the truncated finite sequence w∣n = w0w1...wn is such that the concatenation w∣n⋅w′ ⊧ ϕ for any infinite sequence w′ ∈ (2AP )ω .

Furthermore, for any co-safe LTL formula ϕ written over AP, we can build a deterministic finite automaton (DFA) Aϕ = ⟨Q, q, QF , 2AP , δAϕ ⟩, where: Q is a finite set of states; q ∈ Q is the initial state; QF ⊆ Q is the set of accepting (i.e., final) states; 2AP is the alphabet; and δAϕ ∶ Q × 2AP → Q is a transition function. Aϕ accepts exactly the good prefixes for ϕ [Kupferman and Vardi, 2001]. We extend δAϕ to a function over finite sequences δ+Aϕ ∶ Q × (2AP )∗ → Q in the usual manner, by applying it sequentially to the finite sequence. Given that a good prefix satisfies ϕ regardless of how it is "completed', an accepting state qF ∈ QF is such that δAϕ (qF , α) ∈ QF for all α ∈ 2AP .

4 Policy Generation for Partially Satisfiable Task Specifications

Given an MDP M, a cost structure c ∶ S × A → R≥0, and a co-safe LTL specification ϕ such that Pr max M,s (ϕ) > 0, our goal is to find a policy that: (1) maximises the probability of satisfying ϕ; (2) when ϕ becomes unsatisfiable (i.e., when we reach a state s such that Pr max M,s (ϕ) = 0), gets as close as possible to satisfying ϕ; and (3) has a minimal expected cost to achieve (1) and (2). Before we formally define this problem, we define what we mean by "as close as possible".

4.1 Task ProgressionMetric

We propose a notion of task progression, defined from a distance metric dϕ ∶ Q → Q≥0 that maps each state of Aϕ to a value representing how close we are to reaching an accepting state. In the following, we write q →∗ q′ if there is a sequence of transitions in Aϕ that leads it from state q to state q′ .

Let Sucq ⊆ Q be the set of successors of state q, and ∣δq,q′ ∣ ∈ {0, ..., 2∣AP∣} be the number of transitions from q to q′ . We define the following distance metric:

This metric represents the number of states that need to be visited, starting in q, to reach a state in QF , balanced by the number of transitions between these states. This balancing is done because we assume that, if there are more transitions between two DFA states, then it should be easier for the system to evolve to a state that makes the DFA move between them. Furthermore, if a state in QF is reachable from q, then dϕ(q) ≤ ∣Q∣ - 1. So, if there is no path from q to QF , we set dϕ(q) to the maximum value ∣Q∣. The values dϕ can be calculated recursively by the following fixed-point calculation:

Using this distance metric, we can also define the progression pϕ ∶ Q×Q → Q≥0 between two states of Aϕ as a measure of how much the distance to an accepting state is reduced by moving between q and q′ :

We require q′ /→∗ q in the first condition to guarantee that there are no cycles in the DFA with non-zero values for pϕ. This is needed in order to guarantee convergence of infinite sums of values of pϕ, as will be explained below. We can check existence of paths between q′ and q by computing the strongly connected components (SCCs) of Aϕ. Finally, given that we are only interested in getting closer to accepting states, we only take positive progression values into account.

Example. Consider the DFA in Fig. 1. Inside each state qi, we show the value dϕ(qi) and we label each edge with the number of transitions corresponding to that edge ∣δ∣, and the value of pϕ for the states connected by that edge. Note that moving from any state to the accepting state q3 has a positive progression, as once we get to the accepting state we cannot leave it, due to the co-safe assumption. Also, dϕ(q4) = 5 because there is no path from q4 to the accepting state.

4.2 Problem Statement

We are now in a position to formalise the problem stated at the beginning of this section, which is sub-divided into three objectives. First, let us consider each problem in isolation. Let M be an MDP and ϕ a co-safe LTL formula.

Problem 1 CalculatePr max M,s (ϕ), and find the corresponding policy:

Problem 2 Let σ = s0 a0→ s1 a1→ ... ∈ IPathM,s, and qσ i = δ+Aϕ (q,Lab(s0)Lab(s1) . . .Lab(si)). We define the total progression of σ as prog(σ) = ∑∞i=0 pϕ(qσ i , qσ i+1 ). Calculate Emax M,s (prog), and find the corresponding policy:

Note that, by construction, the value of prog(σ) always converges: any infinite sequence of visited states of a DFA always has an (infinite) suffix formed of only SCCs. Thus, we are guaranteed that for all σ ∈ IPathM,s, ∃k ∈ N such that pϕ(qσ i , qσ i+1 ) = 0, for all i ≥ k. We denote the minimum such k as kσ pϕ . Also, if σ ⊧ ϕ, then Lab(s0)...Lab(skσ pϕ ) is a good prefix for ϕ.

Problem 3 Let σ = s0 a0→ s1 a1→ ... ∈ IPathM,s. We define the cumulated cost until progression pϕ is 0 as cumul kσ pϕ c (σ) = ∑kσ pϕ i=0 c(si, ai). Calculate Emin M,s (cumul kσ pϕ c ), and find the corresponding policy:

These three problems are pairwise conflicting. For example, when the cost of reaching a state from where ϕ is not satisfiable is lower than the cost of reaching an accepting state, the solution for Problem 3 will be a policy that tries to make ϕ not satisfiable as soon as possible. Also, maximising progression might lead to policies that get close to an accepting state with high probability but have probability zero of reaching it, instead of policies that reach an accepting state with some probability. While the solution for each independent problem does not meet our overall goal, we can employ multi-objective probabilistic model checking techniques to look for a solution for the three problems in decreasing order of priority.

4.3 Generation of the Trimmed Product

Before we define the multi-objective based solution, we show that each of the three problems stated above can be reduced to simpler problems in a trimmed product MDP. We start by building the product MDP Mϕ = M ⊗ Aϕ = ⟨S × Q, sϕ, A, δMϕ , AP, Labϕ⟩, and extending the cost structure c to Mϕ as cϕ((s, q), a) = c(s, a). Mϕ behaves like the original MDP M, but is augmented with information about the satisfaction of ϕ. Once a path of Mϕ reaches an accepting state (i.e., a state of the form (s, qF)), it is a good prefix for ϕ, and we are sure that ϕ is satisfied. The construction of the product MDP is well known and is such that Mϕ preserves the probabilities of paths fromM (see, e.g., [Baier and Katoen, 2008]), thus we can reduce Problem 1 to a reachability problem inMϕ. Furthermore, Problem 2 can be reduced to an expected cumulative reward problem in Mϕ, by encoding pϕ as a reward structure rϕ ∶ (S ×Q) ×A→Q≥0:

However, Problem 3 cannot be reduced to an expected cumulative cost problem in Mϕ, because the value kσ pϕ is not constant, being dependent on the path σ. Thus, we need to remove states fromMϕ for which it is not possible to accumulate more pϕ. To do that, we start by defining the set of states for which we can gather more reward immediately as:

Furthermore, we define the set of states for which it is still possible to gather more reward as:

If (s, q) /∈ Srϕ then, by construction of rϕ, it is guaranteed that we cannot progress further towards the goal from (s, q). Thus, such states are not needed to solve Problems 1 - 3.

We can calculate Srϕ efficiently by using S0 rϕ as above, and finding the fixed-point of the following calculation:

Along with Srϕ , we also need to keep states which are successors of a state in Srϕ , but are not in Srϕ . These are the states for which we are certain that no more can be done towards satisfying ϕ, thus they are the states where we should stop accumulating costs. Thus, let:

We can now define the trimmed product MDP Mrϕ ϕ = ⟨Srϕ ∪ SucSrϕ , sϕ, A, δMrϕ ϕ ,AP,Labϕ⟩ as the restriction of Mϕ to the set of states Srϕ plus their possible successor states. More precisely, we project Labϕ, cϕ, and rϕ to Srϕ ∪ SucSrϕ , and only keep transitions from states in Srϕ , i.e., δMrϕ ϕ is defined as:

We just remove states for which the probability of accumulating progression reward is zero in the construction of Mrϕ ϕ , and we remove all the transitions (along with the corresponding costs) from all such states. This means that the solutions for Problems 1 and 2 for Mrϕ ϕ are the same as the solutions for Mϕ. Furthermore, by removing those states, we guarantee convergence of the calculation of the cumulative cost, by removing all end components in the model with a positive cost. Also, once we reach a state where we cannot progress more towards the goal, we achieved the corresponding value for the cumulative cost, thus we can replace the path-dependent sum upper-bound kσ pϕ on the cumulative cost minimisation by an infinite sum. Thus, letting Sϕ,F = {(s, q) ∈ Srϕ ∪ SucSrϕ ∣ q ∈ QF }, we have:

So, Problem 1 can be reduced to solving a reachability problem, and Problems 2 and 3 can be reduced to expected cumulative reward/cost problems, where convergence is guaranteed. These problems can be solved on the same underlying model Mrϕ ϕ using standard techniques, such as value iteration. This allows us to solve a multi-objective problem with three functions to be optimised, as will be discussed next.

4.4 Multi-objective Model Checking

Finally, we use multi-objective probabilistic model checking to generate a policy that takes into account Problems 1, 2 and 3, in decreasing order of priority. As explained above, each of these can be computed using the trimmed product model Mrϕ ϕ . More precisely, we proceed as follows. We first compute the maximum probability p of completing the task:

Then, we find the maximum expected total progression that can be achieved whilst maintaining a task satisfaction probability of p, denoting this value by r:

Finally, we determine the policy which minimises the total expected cost, whilst ensuring that the task satisfaction probability and total progression remain at their optimal values of p and r, respectively:

By calculating c∗ , we also get a corresponding policy π∗ that optimises the three objectives in decreasing order of priority. Note that, even though in general policies for multi-objective specifications can be randomised, we are guaranteed by construction that there exists a deterministic policy that solves the overall problem, because the values p and r we use to constrain the multi-objective queries are the extreme values obtained from the previous query.

4.5 Calculation of Conditional Expectations

We can now generate a cost-optimal policy π∗ for our problem, however the value we obtain for the expected cumulative cost is the expectation to reach a state for which it is not possible to gather more cumulative progression reward. This value can have a very large variance because the expected costs to reach each of these states can be very different. Thus, we are interested in "splitting" the expected cumulative cost value, into expected cost to success, and expected cost to failure. These conditional expectations are more informative and can be used for execution monitoring, or for a higher level task scheduler. We present a procedure to calculate the conditional expectation Eπ∗Mrϕ ϕ ,sϕ (cumulcϕ ∣ reachSϕ,F ) efficiently. We start by noting that, given that π∗ is a memoryless policy for Mrϕ ϕ , applying π∗ to Mrϕ ϕ induces a (finite) Markov chain C = ⟨Srϕ ∪ SucSrϕ , sϕ, δC⟩, where the transition for each state sϕ ∈ Srϕ ∪ SucSrϕ is given by δC(sϕ, s′ϕ) = δMrϕ ϕ (sϕ,π∗ (sϕ), s′ϕ). Furthermore, during the calculation of π∗ , we calculated Prπ∗Mrϕ ϕ ,sϕ (reachSϕ,F ) for all states of C. Let S/⊧ be the set of all the states where such probability is zero. Our goal is to calculate the expected cumulative cost to success, i.e., only for runs of C that reach Sϕ,F , thus we trim C and build C⊧ = ⟨S⊧, sϕ, δC⊧ ⟩, where S⊧ = (Srϕ ∪ SucSrϕ ) ∖ S/⊧, and for all s, s′ ∈ S⊧:

So, to build C⊧ we simply remove all states for which the probability of satisfying the specification is zero, and normalise the transition function accordingly. Then:

This value can be calculated very efficiently, as it is a simple expectation over the Markov chain. We can also easily calculate the expected cost to failure Eπ∗Mrϕ ϕ ,sϕ (cumulcϕ ∣ ¬reachSϕ,F ) given that we know Prπ∗Mrϕ ϕ ,sϕ (reachSϕ,F ), Eπ∗Mrϕ ϕ ,sϕ (cumulcϕ ), and Eπ∗Mrϕ ϕ ,sϕ (cumulcϕ ∣ reachSϕ,F ).

This method can be generalised over the trimmed product, in order to calculate Emin Mrϕ ϕ ,sϕ (cumulcϕ ∣ reachSϕ,F ), and the corresponding policy. However, such an approach does not provide guarantees on probability of task satisfaction, hence it might have a large probability of failure (in spite of providing an optimal expectation for the satisfying runs). See [Baier et al., 2014] for a more general discussion on the calculation of conditional expectations for MDPs.

5 Implementation and Evaluation

We implemented our approach in the widely used PRISM model checker [Kwiatkowska et al., 2011], which already has support for solving MDPs against properties in LTL and, in particular, for multi-objective policy generation [Forejt et al., 2011b]. The tool also includes multiple efficient solution engines, based on symbolic data structures (e.g., binary decision diagrams) designed to improve scalability.

Consider the topological map of an office environment in Fig. 2. We assume that v0 should always be avoided (e.g. to prevent the robot blocking a fire exit), and that our task is to visit nodes v1, v6 and v18 (i.e., visit three rooms). This specification can be written in co-safe LTL as ((¬v0) U v1) ∧ ((¬v0) U v6) ∧ ((¬v0) U v18).

The policy obtained for this specification simply tries to visit v1, v6 and v18 in the order which minimises expected cost (i.e., time), which is the numerical order in this case. However, since there is a chance the robot will end up in v0 when navigating directly between v3 and v4, the policy takes a "detour" through v10. This is because our approach prioritises robustness - in the form of maximisation of the probability of success - over optimality of expected time.

If a closed door is encountered during execution, the policy simply tries to go to the next unvisited closest node. This allows it to satisfy as much of the specification as possible. Based on the values in Fig. 2 the probability of the policy satisfying the specification is 0.729, with an expected time of 11.8 minutes. The values for the expected time of success and failure are 13.8 and 6.42, respectively. The lower time for failure is explained by the fact that the more of the specification the robot fails to satisfy (due to closed doors), the less it has to move. The MDP model used for the scenario on Fig. 2 has 10,206 states and 49,572 transitions. This number is due to the state space of the MDP having one additional dimension per door, each with value "unknown", "open", or "closed". The trimmed product has 21,222 states, and 100,926 transitions, and was generated in 0.354 seconds. Calculating p = P rmax Mrϕ ϕ ,sϕ (reachSϕ,F ) took approximately 1 second, r = Emax Mrϕ ϕ ,sϕ (cumulrϕ ◃ reachSϕ,F ≥ p) 305 seconds, and Emin Mrϕ ϕ ,sϕ (cumulcϕ ◃ reachSϕ,F ≥ p, cumulrϕ ≥ r) 227 seconds, yielding a total of approximately 9 minutes to generate the policy (on an Intel ® Core™i7 @ 1.70GHz x 4 processor, 8GB of RAM). While the specification we tested is computationally challenging, featuring the combinatorial explosion of choosing the best order to visit a set of locations, the time taken to generate the policy is higher than desirable, given that the model is relatively small. This motivates the need to find more efficient approaches for objective prioritisation, and better modelling approaches for this type of environment, and will be the subject of future work. However, with this example we showcase the ability to generate optimal policies for our problem by using multi-objective modelchecking techniques. Moreover, the policies can be calculated offline, and executing them requires negligible computational effort. Since these policies map all reachable states of the trimmed product to an action, this provides a robust plan that can handle every probabilistic environmental outcome without the need for replanning.

6 Conclusions

This paper presented a methodology for the generation of policies that maximise the probability of satisfying a co-safe LTL specification, whilst trying to satisfy it as much as possible when it becomes unsatisfiable, and minimising the expected cumulative cost while doing so. This approach is one of the first cost-optimal policy generation approach for LTL specifications over MDP models able to optimise an undiscounted expected cost over states where the probability of satisfying the specification is not one. Furthermore, the fact that we base our approach on probabilistic model checking techniques allows us to provide meaningful formal guarantees, which can be used to analyse the overall quality of service of the system. In particular, we show how to provide guarantees on the probability of task satisfaction, along with expected cumulative costs for success and failure. We also illustrated the approach on an example that motivates the need to investigate more efficient solutions to our objective prioritisation problem and to model certain environments as MDPs. This will be subject of future work, e.g., modelling of office-like environments, as we are interested in the deployment of service robots using these techniques, and investigating how the approaches in [Teichteil-K¨onigsbuch, 2012b; Kolobov et al., 2012] can be adapted to increase computational efficiency of our solution, as the problem solved there is very similar to our reduced problem in the product MDP.

Acknowledgements

The research leading to these results has received funding from the EU Seventh Framework Programme (FP7/20072013) under grant agreement No 600623, STRANDS.