Probabilistic Temporal Logic for Reasoning about Bounded Policies

1 Introduction

To design and develop intelligent and autonomous agents, it is essential to build a framework describing when and how they act. Such a framework should allow agents to commit to certain actions and to revise their commitments later on. Creating such a framework, therefore, requires the study of intention revision, a topic receiving increased interest in recent decades [Cohen and Levesque, 1990; Rao and Georgeff, 1991; van der Hoek et al., 2007; Shoham, 2009; Icard et al., 2010; van Ditmarsch et al., 2011; van Zee et al., 2020].

As observed by [Shoham, 2009], a primitive yet important kind of intention is that of commitment to perform an action at a specific time. This already comes with nontrivial complications, involving temporal reasoning about the pre- and postconditions of actions. To build a formal framework capable of dealing with this notion of intention, a natural approach is to start with an appropriate underlying temporal logic, as done by [Icard et al., 2010; van Zee et al., 2020]. In their work, actions are deterministic, with a single outcome.

For many practical applications, agents are expected to operate using behavioral policies in stochastic environments where actions have uncertain, nondeterministic outcomes. So in order to study intention revision using methods similar to those of [Icard et al., 2010; van Zee et al., 2020], we require an appropriate probabilistic temporal logic on which to build the model. Such a logic should allow us to reason about the execution, precondition, and (possibly many) postconditions of actions and policies. And in order to be useful in practice, the logic should possess strong computational properties such as efficient (or at least, decidable) model checking and satisfiability, so that we can e.g. algorithmically verify properties of policies and compute whether certain logical inferences are valid.

Probabilistic temporal logics in wide use include PCTL [Hansson and Jonsson, 1994], pCTL* [Aziz et al., 1995], PATL/PATL* [Chen and Lu, 2007], and Probabilistic Strategy Logic [Aminof et al., 2019]. None of these logics fit our desiderata. First, they do not allow us to reason about pre- and postconditions of specific actions. Second, they generally have either high complexity or even undecidable model checking. Note that the decidability of the satisfiability problem for any of these logics would imply that of PCTL, which is a known open problem, and so we cannot get decidable satisfiability for these logics without severe restrictions. Third, from a more practical point of view, all of these logics are interpreted over infinite traces, while finite traces are both sufficient and more natural for most applications in AI (see e.g. [Artale et al., 2019]).

The contribution of this paper is the introduction of the Probabilistic Logic of Bounded Policies (PLBP), a novel probabilistic temporal logic fitting our desiderata, interpreted over finite traces and bounded-time policies in Markov Decision Processes. The logic allows for both reasoning about specific actions/policies, as well as the existence of policies satisfying certain properties. We prove that the model checking problem for PLBP is PSPACE-complete, that it possesses the small model property, and that the satisfiability problem is decidable with a 2EXPSPACE algorithm. The novelty of the logic lies in the fact that it enables us to express a host of properties important for both general applications in AI, as well as for our intended applications, while simultaneously maintaining strong computational properties, which is uncommon amongst probabilistic temporal logics.

2 Syntax and Semantics of PLBP

PLBP is defined relative to a countably infinite set Prop of propositional variables and a finite set A of actions. To each action a ∈ A we associate a precondition prea, which is a conjunction of literals over Prop, and a finite nonempty list Posta of possible postconditions, which are also conjunctions of literals. Intuitively, the precondition of an action is precisely what must be satisfied so that the action can be executed, and a postcondition of an action is one of its possible outcomes, i.e. which is made true after executing the action. We refer to the ith postcondition of a as posta,i. We require postconditions of an action a to be mutually inconsistent, i.e. posta,i and posta,j cannot be simultaneously true for all i ̸= j, meaning that there is a literal in posta,i for which its negation is in posta,j. We refer to actions with a single postcondition as deterministic.

Example 1 (Running example). Mary is a final-year student in Artificial Intelligence. In order to graduate, she needs to pass her exam on methods in AI research. She's not completely sure yet what she wants to do: she can try to graduate and then apply for a Ph.D. position or for a position in industry, but part of her is also considering the possibility of going straight for a position in industry.

There are several things she can do. She can try to study hard for the exam, but she can also take it easy and try the exam unprepared. If she fails the exam, she can try again next year. If she passes, she can then apply for a Ph.D. position or a position in industry, She can also just apply straight for a position in industry.

We formalize Mary's story through propositional variables pass, inPhD and inIndustry. The actions are study, takeEasy, applyIndustry and applyPhD. The preconditions are

• prestudy = ¬pass ∧¬inIndustry ∧¬inPhD,
• pretakeEasy = ¬pass ∧¬inIndustry ∧¬inPhD,
• preapplyIndustry = ¬inIndustry ∧ ¬inPhD, and
• preapplyPhD = pass ∧¬inIndustry ∧¬inPhD.

The postconditions are

• Poststudy = ⟨pass, ¬pass⟩,
• PosttakeEasy = ⟨pass, ¬pass⟩,
• PostapplyIndustry = ⟨inIndustry, ¬inIndustry⟩, and
• PostapplyPhD = ⟨inPhD, ¬inPhD⟩.

We will write f : X ⇀ Y to denote that f is a partial function from X to Y , and write f(x)↓ to denote that f is defined on input x ∈ X. Given a set X, some x ∈ X and n ⩾ 1, we write Xn x for the set of all sequences in X of length n starting with x, and we write X⩽n x = ⋃nk=1 Xk x . Finally, we write ∆(X) for the set of all finitely supported (discrete) probability distributions on X, i.e. those probability distributions D : X → [0, 1] such that D(x) > 0 for only finitely many x.

Definition 1 (MDP). A Markov decision process (MDP) over A is a tuple M = ⟨S, P, V ⟩, where S is the set of states, P : S×A ⇀∆(S) is the partial probabilistic transition function, and V : S → 2Prop is the valuation. We often abbreviate P(s, a) by Ps,a. These are required to satisfy the following conditions.

• (i) For all s ∈ S, there is some a ∈ A such that s |= prea 1 (or by the following condition, equivalently Ps,a↓).

1 Here, |= is a standard classical satisfaction relation, that is, s |= x iff x ∈ V (s) for x ∈ Prop, s |= ¬φ iff s ̸|= φ, and finally, s |= φ ∧ ψ iff both s |= φ and s |= ψ.

• (ii) Ps,a↓ iff s |= prea. (iii) Given Ps,a↓, (iii.i) for all t ∈ S such that Ps,a(t) > 0, there is a unique posta,i in Posta such that t |= posta,i, and (iii.ii) for all posta,i in Posta there is a unique t such that Ps,a(t) > 0 and t |= posta,i.

Condition (i) states that MDPs have no deadlocks, which we include as it allows us to present the following definitions in a cleaner way. In our examples we will consider MDPs that technically do not satisfy this condition: this is not a problem, since we can add in a special deterministic 'do nothing' action which can be executed at any deadlocking state. Conditions (ii) and (iii) ensure that pre- and postconditions are meaningful: an action is executable precisely when the precondition holds, and the possible outcomes of an action are precisely the postconditions.

Example 2 (Running example, continued). An example MDP describing Mary's story using the actions given in Example 1 is M = ⟨S, P, V ⟩, where S = {sstudent, spass, sindustry, sPhD}, respectively denoting the states in which Mary is still a student, in which she passed the exam (and therefore graduated), in which she got a position in industry, and finally, in which she got a Ph.D. position. The valuation V is given by V (sstudent) = ∅, V (spass) = {pass}, V (sindustry) = {inIndustry}, and V (sPhD) = {inPhD}. The partial probabilistic transition function P is defined (for all executable actions according to the preconditions) as

• P(sstudent, study)(sstudent) = 0.2, and P(sstudent, study)(spass) = 0.8 (Mary is likely to pass when studying),
• P(sstudent, takeEasy)(sstudent) = 0.7, and P(sstudent, takeEasy)(spass) = 0.3 (Mary is likely to fail when taking it easy),
• P(sstudent, applyIndustry)(sstudent) = 0.8, P(sstudent, applyIndustry)(sindustry) = 0.2 (Mary is unlikely to just get into industry),
• P(spass, applyIndustry)(spass) = 0.4, P(spass, applyIndustry)(sindustry) = 0.6 (with a degree Mary has reasonable odds of getting into industry),
• P(spass, applyPhD)(spass) = 0.1, P(spass, applyPhD)(sPhD) = 0.9 (Mary will almost surely get into a Ph.D. if she applies).

Our logic will be built around the notion of a bounded policy, telling the agent how to act for a specified number of timesteps in a memoryful manner. These allow us to reason about the probabilities of sequences of states up to a certain length. While such policies might seem restrictive compared to more standard notions of policy considered in the literature, it suffices for our intended applications, as we will comment on at the end of this section. And importantly, while bounded policies are still memoryful (in a bounded sense), the amount of n-step bounded policies from a certain state in a finite MDP will always be finite, in contrast to general memoryful policies. This is an important property that we will use in proving the decidability of the satisfiability problem in Section 4.

On a similar note, we also restrict ourselves to deterministic policies, as they are simple and sufficient for most applications (note e.g. the result by [Puterman, 1994] showing the guaranteed existence of optimal deterministic policies).

Definition 2 (Bounded policies). Given an MDP M and n ⩾ 1, an n-step M-policy is a pair ⟨s, π⟩ where s ∈ S is referred to as its initial state (and we say the policy is from s), and π: S⩽n s → A is a function such that sk |= preπ(s1···sk) (or equivalently P(sk, π(s1 · · · sk))↓) for all s1 · · · sk ∈ S⩽n s . A bounded M-policy is an n-step M-policy for some n.

We drop the M when the MDP is clear from the context. We will also often identify the bounded policy ⟨s, π⟩ with the function π. Whenever we wish to make the initial state explicit, by slight abuse of notation, we write πs instead of the function π.

For an n-step policy πs , we define Paths(πs ) as the set

Given an n-step policy πs , its path distribution is the probability distribution µM,s π over Paths(πs ) defined as

This extends to sets of paths in the standard way, i.e. µM,s π (X) = ∑s∈X µM,s π (s). Whenever it is clear from the context, we drop the M from the superscript.

Our policies are defined with respect to finite state histories. For practical purposes, it can be useful to consider policies that consider state-action histories as well, so that the agent can base the choice of the next action depending on which action it executed in the past. Although we do not expand upon this for simplicity of presentation, we note that all of our work extends to such policies as well.

Example 3 (Running example, continued). Suppose Mary realizes that she has enough time and funds to stay in university for an extra year, and therefore wants to take it easy this year, only starting to seriously study next year. If she manages to graduate this year, she will try to get into a Ph.D. (surprised by the ease of obtaining a degree).

This can be seen as Mary adopting the 2-step policy π from sstudent, defined as

• π(sstudent) = takeEasy,
• π(sstudentsstudent) = study, and
• π(sstudentspass) = applyPhD.

Note that we need not consider other state sequences than the ones specified, as it is impossible to actually encounter those with this policy.

The path distribution on Paths(πsstudent ) can then be verified to take the following values in its support:

• µsstudent
• π (sstudent takeEasy sstudent study sstudent) = Psstudent,takeEasy(sstudent) · Psstudent,study(sstudent) = 0.7 · 0.2 = 0.14,
• µsstudent π (sstudent takeEasy sstudent study spass) = Psstudent,takeEasy(sstudent) · Psstudent,study(spass) = 0.7 · 0.8 = 0.56,
• µsstudent π (sstudent takeEasy spass applyPhDspass) = Psstudent,takeEasy(spass) · Pspass,applyPhD(spass) = 0.3 · 0.1 = 0.03, and
• µsstudent π (sstudent takeEasy spass applyPhDsPhD) m = Psstudent,takeEasy(spass) · Pspass,applyPhD(sPhD) = 0.3 · 0.9 = 0.27.

Using this path distribution, we can now determine the probability that Mary is not in a Ph.D. in two timesteps when applying π by summing up the probabilities of paths ending in a state other than sPhD, resulting in a probability of 0.73.

Definition 3 (Syntax). The language of PLBP is inductively defined by the grammar

where x ∈ Prop, a ∈ A , n ⩾ 1, r ∈ Q ∩ [0, 1], and ▷◁ ∈ {< , =, >}. Formulas φ are referred to as state formulas (or just PLBP formulas), and formulas Φn are referred to as n-step path formulas (or more generally, path formulas).

In the definition of state formulas, ⊥ stands for falsity. The modal formula ♢n▷◁rΦ involves existential quantification over policies and states that "the agent can act in the next n steps in such a way that Φ will hold with probability ▷◁ r."

Boolean connectives ∨, → are defined as abbreviations in a standard way. We also define the following abbreviations:

• ♢n⩾rΦ := ♢n>r Φ∨♢n=rΦ
• ♢n⩽rΦ := ♢n<r Φ∨♢n=rΦ

We can also define a modal operator □n▷◁rΦ that replaces the existential quantification with universal quantification, through the following abbreviations:

• □n<r Φ := ¬♢n>r Φ∧¬♢n=rΦ
• □n⩽rΦ := ¬♢n>r Φ
• □n=rΦ := ¬♢n<r Φ∧¬♢n>r Φ
• □n⩾rΦ := ¬♢n<r Φ
• □n>r Φ := ¬♢n<r Φ∧¬♢n=rΦ

Path formulas are built from state formulas together with doa-propositions, combined using the X-operator and Boolean connectives. The doa-proposition, where a ∈ A , should be read as "the agent will now execute a", i.e. the next action on the path is a. The operator X stands for the next-time operator, with Xφ being true on a path meaning that φ is true on the next state in the path.

Note that in the way we set up our syntax, Φn -formulas have at most n nested X-operators. Therefore, in the state formula ♢n▷◁rΦ, the path formula Φ is not allowed to have a nesting depth of X-operators greater than n. Intuitively, this is because the policies quantified over in ♢n▷◁rΦ only look n steps ahead. 2

If the limitation on the length of paths and nesting depth is dropped, problems arise in the semantics: we somehow

2 The definition of path formulas could have been stated in a standard way, as

but then in the definition of state formulas, we would need a side condition that in ♢n▷◁rΦ, the path formula Φ has at most n nested X-operators.

need to evaluate XΦ in a state that does not exist on the path. In LTL on finite traces [De Giacomo and Vardi, 2015], all formulas XΦ are false in the last state of a path, even if Φ is a tautology. So, paradoxically, the probability of a set of 1-step paths where a tautology holds after two steps would have to be 0 if we adopt a similar approach.

Note that although the temporal part of the logic only contains X, we can define abbreviations for bounded versions of other standard temporal operators like U (something holds until something else does) and G (something always holds).

E.g. GnΦ, meaning Φ always holds in the next n steps, can be considered as an abbreviation of Φ ∧ XΦ ∧ · · · ∧ XnΦ, where Xn is X repeated n times.

Example 4 (Running example, continued). Below are some examples of formulas of PLBP for the example of Mary:

• inPhD is a state formula and therefore also an n-step path formula for any n,
• XinPhD is an n-step path formula for n ⩾ 1, meaning that Mary is in a Ph.D. position at the next timestep,
• ♢2=0.96XXinPhD is a state formula, meaning that Mary can act now and in the next timestep in such a way that afterwards she will be in a Ph.D. position with probability 0.96, and
• ♢2>0.4XXXinPhD is not a syntactically correct formula because XXXinPhD has three nested X-operators, which cannot occur in the scope of a ♢2 modality. Intuitively, it is not meaningful to say that Mary can act now and in the next timestep in such a way that in three steps she will be in a Ph.D. position with a probability greater than 0.4 since this would depend on what action Mary would take in two steps.

Definition 4 (Semantics). Given an MDPM, the semantics of PLBP is defined via simultaneous induction over state and path formulas: for state formulas, it is defined with respect to states as

• M, s |= ⊥ never,
• M, s |= x iff x ∈ V (s),
• M, s |= φ ∧ ψ iff M, s |= φ and M, s |= ψ,
• M, s |= ¬φ iff M, s ̸|= φ, and
• M, s |= ♢n▷◁rΦ iff there exists an n-step policy πs such that µsπ ({s ∈ Paths(πs ) | M, s |= Φ}) ▷◁ r,

while for n-step path formulas, it is defined with respect to length n paths, i.e. nonempty finite sequences s = s1a1 · · · snansn+1 of states and actions, as

• M, s |= φ iff M, s1 |= φ,
• M, s |= doa iff a1 = a,
• M, s |= Φ ∧ Ψ iff M, s |= Φ and M, s |= Ψ,
• M, s |= ¬Φ iff M, s ̸|= Φ, and
• M, s |= XΦ iff M, sX |= Φ where sX = s2a2 · · · sn.

Whenever it is clear from the context, we drop the M and just write s |= φ and s |= Φ.

Example 5 (Running example, continued). Revisiting the MDP we specified for Mary's situation, we see that the following formulas are satisfied.

• sstudent |= ♢2>0.5XXinIndustry: Mary can act now and in the next step in such a way that with probability greater than 0.5, she will be in industry in two steps. Namely, with
• the policy saying to study now, and then (no matter the outcome) apply to industry afterwards.
• sstudent |= prestudy ∧□1⩾0.6 (dostudy → Xpass): Mary can execute study, and doing so will cause pass to hold afterwards with a probability at least 0.6.
• sstudent |= ♢1=1X□1=1X¬inPhD: Mary can act now in such a way that it becomes guaranteed that no matter how she acts afterwards, she will not be in a Ph.D. position. Namely, by choosing to apply to industry now.

Since we have explicit postconditions in the logic, we can even formulate properties of specific policies Mary can choose. For example, consider the 2-step policy that says to take it easy now, apply to industry afterwards if she passes, and otherwise study. We can state in our logic that under this policy, Mary will be in industry in two steps with a probability less than 0.2. This can be done by way of the formula

remembering that posttakeEasy,1 = pass and posttakeEasy,2 = ¬pass. And indeed, this formula holds at sstudent. Generalizing beyond the example of Mary, we can similarly state that policies in other MDPs satisfy properties with some probability, e.g. safety and liveness properties.

Example 6 (Coherence of intentions). Let us now revisit the theory of intention. Given a finite set I of "commitment towards time" intentions (which we take to be pairs ⟨a, t⟩ of actions a and time steps t, meaning that the agent intends to perform a at t), it is important to be able to determine whether adopting these intentions is coherent, in the sense laid out by [Shoham, 2009; van Zee et al., 2020]. In particular, this means that intentions need to be internally consistent (e.g. at most one action can be executed at a time, and subsequent actions need to have compatible pre- and postconditions). Furthermore, with respect to the agent's beliefs, coherence means that for all of the agent's intentions, the agent does not believe that the preconditions of the intended action do not hold at the intended time, and the agent does believe that the intended actions' postconditions hold.

Representing the agent's beliefs as a set Γ of formulas, we can formulate a notion of coherence of I with respect to Γ satisfying the above criteria. Consider the formula

where tmax = max⟨a,t⟩∈I t. This formula encodes the agent's belief (with strength θ ∈ [0, 1]) that it is possible to execute all of their intentions. Using this, we can say that I is coherent with respect to Γ iff Γ and execθ(I) is satisfiable. And indeed, this notion of coherence requires that intentions are internally consistent, as well as that the agent does not believe (too strongly) that the preconditions of the intended actions do not hold at the intended time, and after adding execθ(I) to the agent's beliefs, the agent must also believe that the intended actions' postconditions hold (with a certain probability).

This example shows why it is important that we use a logic in which we can explicitly reason about the execution of actions, as well as their pre- and postconditions. And furthermore, the example shows how restricting to bounded policies and finite paths still allows us to express what we wish, while simultaneously allowing for good computational properties, which we will see in the following sections.

3 Model Checking

In this section, we state the model checking problem for PLBP, show that it is decidable, and analyze its complexity. Note that we restrict our attention to state formulas, as this suffices for our intended applications. The model checking problem for PLBP can be formulated as follows:

Instance An MDP M over A with associated prea and Posta for all a ∈ A , a state s in M, and a PLBP formula φ, where the numbers are written in unary. 3

Question Does it hold that M, s |= φ?

Theorem 1. The model checking problem for PLBP is decidable.

Proof. We give an algorithm for solving the model checking problem. Consider the set of all state subformulas of φ, Subf(φ) (including those occurring inside its path subformulas). Order Subf(φ) in the order of increasing complexity, starting with propositions. Then label the states in M with formulas in Subf(φ) that they satisfy, in order. The cases of propositions and Boolean connectives are trivial. Let us consider the case of ♢n▷◁rΦ. In order to determine whether to label some state s with ♢n▷◁rΦ, we need to check whether there is some policy πs such that property µsπ ({s ∈ Paths(πs ) | s |= Φ}) ▷◁ r. A straightforward approach is to iterate over all possible n-step policies πs . There are O(|A ||Sn | ) of those, and each policy is of size O(|A | × |Sn |). We can generate them one by one and represent them using space polynomial in the MDP and exponential in the formula. For each policy πs , generate Paths(πs ). That set is of size O((|S| × |A |)n ). Given that states on each path are already labeled with the state subformulas of Φ, it is easy (i.e. linear time) to evaluate Φ on all of them. If for a given policy π it holds that µsπ ({s ∈ Paths(πs ) | s |= Φ}) ▷◁ r, then label s with ♢n▷◁rΦ. Otherwise, if no policy satisfies this, s does not satisfy ♢n▷◁rΦ.

The algorithm above gives a decision procedure in EXPSPACE. It has the advantage that it can return a policy satisfying ♢n▷◁rΦ if it exists (and since policy size is exponential in the formula, we cannot do better). However, if a witness policy is not required, it is possible to do better.

Below we give a nondeterministic algorithm which, given a structure M = (S, P, V ) over A and a formula φ0, returns the set of states [φ0]M satisfying φ0: [φ0]M = {s | M, s |= φ0} (see Algorithm 1). This algorithm uses only polynomial space.

Given φ0, we produce a set of subformulas Subf (φ0) of φ0 in the usual way. We then proceed by cases. For all formulas in Subf (φ0) apart from ♢n▷◁rΦ the cases are standard. Labeling states with ♢n▷◁rΦ makes use of a function MEASURE

3 If n is written in binary, then e.g. a linear pass over a sequence of n states takes time exponential in the size of the formula, which we find counterintuitive.

Algorithm 1 Labelling φ0

function PLBP-LABEL(M, φ0) for φ′ ∈ Subf (φ0) do case φ′ = p [φ′ ]M ← V (p) case φ′ = ¬φ [φ′ ]M ← S \ [φ]M case φ′ = φ ∧ ψ [φ′ ]M ← [φ]M ∩ [ψ]M case φ′ = ♢n▷◁rΦ [φ′ ]M ← { s | MEASURE(node0(s), Φ, n, 0) ▷◁ r} return [φ0]M

Algorithm 2 Computing the measure of paths

function MEASURE(q, Φ, n, PΦ) if d(q) > n then if p(q) |= Φ then PΦ ← PΦ + µ(p(q)) return PΦ elseguess a ∈ actions(s(q)) for o ∈ outcomes(s(q), a) do PΦ ← MEASURE(node(q, a, o), Φ, n, PΦ) return P ′Φ

which returns the measure of paths generated by a policy (see Algorithm 2).

The function MEASURE takes four arguments: the current node q, the formula Φ, the depth of the policy n, and the measure of the paths generated by the policy so far which satisfy Φ. The algorithm proceeds by recursive depth-first search. Each branch in the search tree is represented by a sequence of nodes. A node is a structure that consists of a state of M and a finite path of nodes leading to this node from the root node. For each node q, we have a function s(q) which returns its state, a(q) which returns the action taken to reach s(q), p(q) which returns the nodes on the path to q and d(q) which returns the length of the path to q. The function node0(s) returns the root node, i.e., a node q0 such that s(q0) = s a(q) = nil, p(q0) = [ ] and d(q0) = 0. The function node(q, a, s′ ) returns a node q′ where s(q′ ) = s′ , a(q′ ) = a, p(q′ ) = [p(q) · q′ ] and d(q′ ) = d(q) + 1.

The base case is when the length of the branch, d(q) is greater than n. If Φ is true on the path represented by this branch, we update PΦ, the measure of the paths generated so far, by adding the probability of the current path to it, before returning; otherwise, we return the value of PΦ passed as an argument. The recursive case is when the length of the branch is less than or equal to n. We extend the policy by guessing an action possible in s(q) (this is the only non-deterministic step in the algorithm). For each possible outcome state o of executing action a in state s(q), we call MEASURE to update PΦ with the measure of paths through state o. When all the outcome states of a have been considered, we return PΦ as the measure of the paths with prefix p(n) where action a is chosen in s(n). Note that execution of MEASURE requires only polynomial space. The recursion is bounded by n, and for each recursive call, we need to remember only the remaining outcomes of the chosen action yet to be considered, which is bounded by |S|. Keeping track of the measure of the paths generated by the policy so far which satisfy Φ requires constant space. MEASURE is a nondeterministic algorithm, so the complete model checking algorithm runs in nondeterministic polynomial space. Since NPSPACE = PSPACE by Savitch's theorem [Savitch, 1970], there is a PSPACE algorithm for solving the model checking problem for PLBP. This gives us inclusion in PSPACE. Below we also prove PSPACE-hardness.

Theorem 2. The model checking problem for PLBP is PSPACE-complete.

Proof. The hardness proof is by reduction of the QSAT (Satisfiability of Quantified Boolean Formulas) problem (which is a PSPACE-complete problem) to the model checking problem for PLBP. We use a reduction from QSAT inspired by [Bulling and Jamroga, 2010]. However, instead of the strategic setting of [Bulling and Jamroga, 2010], where a verifier has a strategy to evaluate the formula to true (enforce the 'yes' state) if and only if the formula is satisfiable, we work in the probabilistic setting, where an agent has a policy to reach the 'yes' state with probability 1 if and only if the QBF formula is satisfiable.

The details of the proof are given in the supplementary material.

4 Satisfiabilty

The satisfiability problem for PLBP is as follows:

Instance A PLBP formula φ over A with associated prea and Posta for all a ∈ A . We assume that the numbers are written in unary.

Question Is there an MDP M over A , prea, and Posta, such that there exists a state s in M with M, s |= φ?

We will now begin proving that the satisfiability problem is also decidable.

Denote by pd(φ) the policy depth of a formula φ, defined as pd(φ) = 1 if φ is atomic, pd(φ ∧ ψ) = max{pd(φ), pd(ψ)}, pd(¬φ) = pd(φ), and pd(♢n▷◁rΦ) = n + max{pd(φ) | φ appears in Φ}. We then have the following.

Theorem 3 (Small model property). If a formula φ is satisfiable, then it is also satisfiable in an MDP with at most as many states as a tree with depth pd(φ) and branching factor ∑a∈A |Posta|.

Proof sketch. As the proof is a conceptually clear but technically involved extension of the method of unraveling, wellknown in modal logic, we give details only in the supplementary material. The intuition is that we can unfold the MDP into a tree-shaped structure, branching for every executable action and possible outcome (i.e. each executable a ∈ A and posta,i ∈ Posta). This tree satisfies exactly the same formulas as the original MDP. Evaluating φ only requires us to search through the tree up to depth pd(φ).

Theorem 4 (Satisfiability). The satisfiability problem for PLBP is decidable in 2EXPSPACE.

Proof sketch. We first describe a decision procedure and comment on its complexity afterwards. Using the bound y on the state count from Theorem 3, we iterate over sets S = {s1, . . . , sl} of size at most y, and over valuations V on S considering only the variables appearing in φ (plus all pre- and postconditions). We require that for all s ∈ S there is some a such that s |= prea. We now show that we can define some P such that ⟨S, P, V ⟩, s1 |= φ, iff some first-order logic (FOL) sentence αφ holds in the theory of real closed fields (RCF). We refer to [Chang and Keisler, 2012] for those unfamiliar with RCF. Using the well-known decidability of RCF, we then get a decision procedure.

We will encode P through variables ps,t,a for s, t ∈ S and a ∈ A , denoting Ps,a(t) (if that is defined). Writing p for the sequence of all these variables, we consider a first-order formula β(p) that is true in RCF iff the P encoded by p is well-defined (following the conditions of Definition 1).

Next, we consider for every 1 ⩽ n ⩽ pd(φ), state s, n-step policy πs , X ⊆ Paths(πs ), ▷◁ and r ∈ Q ∩ [0, 1], a FOL formula γs,X,π,▷◁,r(p) such that if β(p) holds in RCF, then γs,X,π,▷◁,r(p) holds iff µsπ (X) ▷◁ r in the MDP encoded by p. Note that µsπ (X) ▷◁ r is an inequality with a sum of products, expressible in RCF.

We now simultaneously define FOL formulas δψ,s, κΦ,h, and λΦ,s,n,π,X, respectively expressing "s |= ψ", "h |= Φ", and "X is the set of all h ∈ Paths(πs ) such that h |= Φ".

The definitions of these are simple, and almost directly follow the semantics of our logic, with e.g. (i) δ♢n▷◁r Φ,s = ∨n-step πs ∨X⊆Paths(πs ) λΦ,s,n,π,X → γs,X,π,▷◁,r, (ii) κXΦ,h = κΦ,hX , and (iii) λΦ,i,n,π,X = ∧h∈X κΦ,h ∧ ∧h∈Paths(πs )\X ¬κΦ,h.

Finally, we put αφ = ∃p(β(p) ∧ δφ,s1 (p)), finishing our description of the decision procedure.

Iterating over S and V proceeds for a double exponential number of iterations w.r.t. the input, by the bound given in Theorem 3. The FOL formula we construct in each iteration is also of double exponential size, as the δ♢n▷◁r Φ,s formula contains a disjunct for every policy and set of paths. Noting that αφ is an existential formula, it follows from existential RCF being in PSPACE [Canny, 1988] that the overall procedure runs using double exponential space.

5 RelatedWork

There are many logics designed to reason about time and probability. Most of these consider infinite traces/histories, in contrast to PLBP. Though we will state for each logic how the expressive power of that logic differs from that of PLBP, we also refer the interested reader to [Artale et al., 2019] for a more general comparison of finite- and infinite-trace logics.

The logics PCTL [Hansson and Jonsson, 1989; Hansson and Jonsson, 1994] and pCTL∗ [Aziz et al., 1995] extend the branching-time temporal logics CTL and CTL∗ , respectively, with operators P▷◁r such that P▷◁rφ is true at a state iff infinite paths starting from that state satisfy φ with probability ▷◁ r. The logics have decidable model checking, polynomial-time for PCTL and polynomial-space for pCTL∗ , but the matter of whether satisfiability is decidable has been a long-standing open problem, as is the case for all the other logics we mention here. Formulas of PCTL and pCTL∗ are interpreted over discrete-time Markov chains, which are our MDPs without actions. PLBP is not a fragment or a restriction of pCTL∗ to finite traces. One obvious reason for this is the presence of actions; formulas with do expressions in Example 5 cannot be expressed in pCTL∗ .

Closer in spirit are extensions introduced in [Bianco and de Alfaro, 1995]. Their models are Markov chains, in which at each state a next-state probability distribution is nondeterministically selected, according to which the structure transitions to a next state. This is in effect working with a less structured notion of actions (without pre- and postconditions), in which the nondeterministic choice corresponds to a choice of action. The logic has operators P⩾r and P⩽r, which respectively consider minimal and maximal probabilities of paths with respect to the nondeterministic choices. Considering the mentioned correspondence between nondeterminism and actions, these operators are effectively doing existential and universal quantification (respectively) over policies, similar to the ♢ and □ modalities of PLBP. The PCTL extension still has polynomialtime model checking, but the pCTL∗ extension now has a lower bound of 2EXPTIME. Though these extensions have some notion of action hiding behind the scenes as we pointed out, they cannot express everything we need for our applications (which we can express with PLBP). Specifically, we cannot reason in these extensions about the executability and consequences of certain actions, which is required to determine the coherence of an agent's intentions (as discussed in Example 6). Besides that, these extensions are quite limited in what kind of inequalities they support: for example, we cannot reason about the existence of a policy for which Φ holds with a probability less than 0.2.

The logics PATL and PATL∗ , introduced by [Chen and Lu, 2007], are extensions of PCTL and pCTL∗ respectively, in which there is a set of multiple agents, and in which actions are explicitly part of the semantics (but not the language). These logics are interpreted over probabilistic concurrent game structures, which are generalizations of MDPs in which the probability of transitioning from one state to another is determined by which actions all of the agents choose. The main modality of these logics is ⟨⟨B⟩⟩▷◁r, where B is a subset of agents, with the interpretation that ⟨⟨B⟩⟩▷◁rΦ iff the agents in B have a (memoryful) strategy/policy together that enforces that the path formula Φ holds with probability ▷◁ r. Model checking PATL is in P NP∩coNP , and [Chen and Lu, 2007] state that pATL∗ also has decidable model checking, and though we did not manage to find the proof of this statement and (the complexity of) the corresponding algorithm, it must have a lower bound of 2EXPTIME since model checking for the pCTL∗ extension of [Bianco and de Alfaro, 1995] reduces to it. Again, PLBP is not a fragment or a restriction of these formalisms.

Probabilistic Strategy Logic (PSL) [Aminof et al., 2019] has first-order quantification over memoryful strategies/policies, allowing one to express statements like 'there exists a policy such that p will hold with probability at least 0.2 and q will hold with probability precisely 0.9', which is not possible in PATL∗ (or any of the other logics mentioned here, including PLBP). We note that PSL does not allow us to reason about the execution of specific actions. This increase in expressive power comes with a high price: model checking is already undecidable for a highly restricted fragment of PSL, even when considering deterministic finite-memory strategies and a single agent. Limiting to memoryless strategies gives decidable model-checking with an upper bound of 3EXPSPACE. So even if we were to add reasoning about explicit pre- and postconditions into PSL, the resulting logic would not be practical for our purposes from a computational perspective, having too high complexity model checking and unknown decidability of satisfiability. And we truly need memoryful (bounded) policies for statements like "the agent can act in the next n steps in such a way that . . . " which we use for checking the coherence of intentions.

6 FutureWork

As explained in Section 1, the intended application of PLBP is to build a theory of intention revision under uncertainty, following [Shoham, 2009] in considering intentions as commitments towards time. In particular, we aim to follow [van Zee et al., 2020] in putting intention revision on top of the wellknown AGM-style belief revision [Alchourr´on et al., 1985]. The computational properties of PLBP are important for this goal; especially decidable satisfiability, as it allows us to compute whether beliefs and intentions after an update are still consistent. And as discussed in Example 6, we can define coherence as satisfiability in the logic. Furthermore, the logic working with finite/bounded traces and policies also facilitates AGM-style revision in the absence of compactness, following [van Zee et al., 2020].

Besides intention revision, we plan to consider reasoning about policies in reinforcement learning. For this application, we will consider extensions of PLBP with reward signals and imperfect information. Natural starting points are [Jamroga, 2008], who introduces a quantitative logic for MDPs that reasons about rewards, and [Huang et al., 2012], who introduce an extension of PATL∗ with imperfect information.

We will also investigate the expressive power of the logic, by following common practice in modal logic and defining an appropriate notion of bisimulation for MDPs that satisfies a Hennessy-Milner theorem with respect to PLBP. A sound and complete axiomatization of PLBP is of interest since it would allow us to formalize how pre- and postconditions behave in PLBP and verify whether principles of coherence like those listed by [Shoham, 2009] hold in the logic.

7 Conclusion

We have introduced PLBP, a novel probabilistic temporal logic for reasoning about the interactions between actions, time, and probability. It can describe time-bounded policies in MDPs, the probability that some property can be achieved by such a policy, and can also reason about specific properties of actions and policies. We have analyzed the typical reasoning problems for PLBP, namely model checking and satisfiability, and have shown that both are decidable. We plan to use PLBP in the future for formalizing intention revision under uncertainty and to apply it to settings like Reinforcement Learning.