Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Traditionally, strategies are represented by Mealy machines, i.e., finite automata with outputs (see, e.g., [12, 33]). Strategies that admit such a representation are called finite-memory strategies. A special subclass is that of memoryless strategies, i.e., strategies whose decisions depend only on the current state.

In finite MDPs, pure memoryless strategies often suffice to play optimally with a single payoff or objective, e.g., for reachability [4] and parity objectives [22], and mean [8] and discounted-sum payoffs [40]. In countable MDPs, for reachability objectives, pure memoryless strategies are also as powerful as general ones, though optimal strategies need not exist in general [35, 31]. In the multi-objective setting, memory and randomisation are necessary in general (e.g., [39, 21]). Nonetheless, finite memory often suffices in finite MDPs, e.g., when considering several $\omega$-regular objectives [25].

The picture is more complicated in infinite-state MDPs, where even pure memoryless strategies need not admit finite representations. Our contribution focuses on small (and particularly, finite) counter-based representations of memoryless strategies in a fundamental class of infinite-state MDPs: one-counter MDPs.

One-counter MDPs (OC-MDPs, [16]) are finite MDPs augmented with a counter that can be incremented (by one), decremented (by one) or left unchanged on each transition.¹¹1 Considering such counter updates is not restrictive for modelling: any integer counter update can be obtained with several transitions. However, this impacts the complexity of decision problems. Such a finite OC-MDP induces an infinite MDP over a set of configurations given by states of the underlying MDP and counter values. In this induced MDP, any play that reaches counter value zero is interrupted; this event is called termination. We consider two variants of the model: unbounded OC-MDPs, where counter values can grow arbitrarily large, and bounded OC-MDPs, in which plays are interrupted when a fixed counter upper bound is reached.

The counter in OC-MDPs can, e.g., model resource consumption along plays [16], or serve as an abstraction of unbounded data types and structures [20]. It can also model the passage of time: indeed, OC-MDPs generalise finite-horizon MDPs, in which a bound is imposed on the number of steps (see, e.g., [5]). OC-MDPs can be also seen as an extension of one-counter Markov chains with non-determinism. One-counter Markov chains are equivalent to (discrete-time) quasi-birth-death processes [26], a model studied in queuing theory.

Termination is the canonical objective in OC-MDPs [16]. Also relevant is the more general selective termination objective, which requires terminating in a target set of states. In this work, we study both the selective termination objective and the state-reachability objective, which requires visiting a target set of states regardless of the counter value.

Optimal strategies need not exist in unbounded OC-MDPs for these objectives [15]. The general synthesis problem in unbounded OC-MDPs for selective termination is not known to be decidable, and it is at least as hard as the positivity problem for linear recurrence sequences [37], whose decidability would yield a major breakthrough in number theory [36]. Optimal strategies exist in bounded OC-MDPs: the induced MDP is finite and we consider reachability objectives. However, constructing optimal strategies is already EXPTIME-hard for reachability in finite-horizon MDPs [5].

In this work, we propose to tame the inherent complexity of analysing OC-MDPs by restricting our analysis to a class of succinctly representable (yet natural and expressive) strategies called interval strategies.

The monotonic structure of OC-MDPs makes them amenable to analysis through strategies of special structure. For instance, in their study of solvency games (stateless variant of OC-MDPs with binary counter updates), Berger et al. [7] identify a natural class of rich man’s strategies, which, whenever the counter value is above some threshold, always select the same action in the same state. They argue that the question of existence of rich man’s optimal strategies “gets at a real phenomenon which …should be reflected in any good model of risk-averse investing.” While [7] shows that optimal rich man’s strategies do not always exist, if they do, their existence substantially simplifies the model analysis.

In this work, we make such finitely-represented strategies the primary object of study. We consider so-called interval strategies: each such strategy is based on some (finite or infinite but finitely-representable) partitioning of $\mathbb{N}$ into intervals, and the strategy’s decision depends on the current state and on the partition containing the current counter value.

More precisely, we focus on two classes of these strategies: On the one hand, in bounded and unbounded OC-MDPs, we consider open-ended interval strategies (OEISs): here, the underlying partitioning is finite, and thus contains an open-ended interval $[n,\mathrm{\infty })$ on which the strategy behaves memorylessly, akin to rich man’s strategies.

On the other hand, in unbounded OC-MDPs, we also consider cyclic interval strategies (CISs): strategies for which there exists a (positive integer) period such that, for any two counter values that differ by the period, we take the same decisions. A CIS can be represented similarly to an OEIS using a partition of the set of counter values up to the period.

We collectively refer to OEISs and CISs as interval strategies. While interval strategies are not sufficient to play optimally in unbounded OC-MDPs [7], they can be used to approximate the supremum probability for the objectives we consider [15].

We formally introduce the class of interval strategies. We show that OEISs in bounded OC-MDPs and CISs in unbounded OC-MDPs can be exponentially more concise than equivalent Mealy machines (Sect. 3), and unbounded OEISs can even represent infinite-memory strategies.

For selective termination and state reachability, we consider the interval strategy verification problem and two realisability problems for structure-constrained interval strategies. On the one hand, the fixed-interval realisability problem asks, given an interval partition, whether there is an interval strategy built on this partition that ensures the objective with a probability greater than a given threshold. Intuitively, in this case, the system designer specifies the desired structure of the controller. On the other hand, the parameterised realisability problem (for interval strategies), asks whether there exists a well-performing strategy built on a partition of size no more than a parameter $d$ such that no finite interval is larger than a second parameter $n$. We consider two variants of the realisability problem: one for checking the existence of a suitable pure strategy and another for randomised strategies. Randomisation allows for better performance when imposing structural constraints on strategies (Ex. 3), but pure strategies are however often preferred for synthesis [24].

Our complexity results are summarised in Table 1. Analysing the performance of a memoryless strategy amounts to studying the Markov chain it induces on the MDP. The Markov chain induced by an interval strategy is infinite in unbounded OC-MDPs and of exponential size in bounded OC-MDPs, and thus cannot be analysed in polynomial space with classical approaches. Our results rely on the analysis of a compressed Markov chain derived from this large induced Markov chain. We remove certain configurations and aggregate several transitions into one (Sect. 4). This compressed Markov chain preserves the probability of selective termination and of hitting counter upper bounds (Thm. 6). However, its transition probabilities may require exponential-size representations or even be irrational. To represent these probabilities, we characterise them as the least solutions of quadratic systems of equations (Thm. 8), similarly to the result of [32] for termination probabilities in probabilistic pushdown automata. Compressed Markov chains are finite for OEISs and are induced by a one-counter Markov chain for CISs (Lem. 10).

The crux of our algorithmic results is the aforementioned compression. For verification, we reduce the problem to checking the validity of a universal formula in the theory of the reals, by exploiting our characterisation of transition probabilities in compressed Markov chains. This induces a PSPACE upper bound. For bounded OC-MDPs, we can do better: verification can be solved in polynomial time in the unit-cost arithmetic RAM model of computation of Blum, Shub and Smale [11], by computing transition and reachability probabilities of the compressed Markov chain. This yields a ${\text{P}}^{\text{PosSLP}}$ complexity in the Turing model (see [2]).

Both realisability variants exploit the verification approach through the theory of the reals. For fixed-interval realisability for pure strategies, we exploit non-determinism to select good strategies and then verify them with the above. In the randomised case, in essence, we build on the verification formulae and existentially quantify over the probabilities of actions under the sought strategy. Finally, for parameterised realisability, we build on our algorithms for the fixed-interval case by first non-deterministically building an appropriate partition.

We also provide complexity lower bounds. We show that all of our considered problems are hard for the square-root-sum problem, a problem that is not known to be solvable in polynomial time but that is solvable in polynomial time in the Blum-Shub-Smale model [42]. We also prove NP-hardness for our realisability problems for selective termination, already when checking the existence of good single-interval strategies.

Our results provide a natural class of strategies for which realisability is decidable (whereas the general case remains open and known to be difficult [37]), and with arguably low complexity (for synthesis). Furthermore, the class of interval strategies is of practical interest thanks to their concise representation and their inherently understandable structure (in contrast to the corresponding Mealy machine representation).

In addition to the main references cited previously, we mention some (non-exhaustive) related work. The closest is [9]: interval strategies are similar to counter selector strategies, studied in consumption MDPs. These differ from OC-MDPs in key aspects: all transitions consume resources (i.e., bear negative weights), and recharge can only be done in special reload states, where it is considered as an atomic action up to a given capacity. Consumption and counter-based (or energy) models have different behaviors (e.g., [19]). The authors of [9] also study incomparable objectives: almost-sure (i.e., probability one) Büchi objectives.

Restricting oneself to subclasses of strategies that prove to be of practical interest is a common endeavor in synthesis: e.g., strategies represented by decision trees [17, 18, 3, 30], pure strategies [29, 24, 13], finite-memory strategies [23, 14, 13], or strategies using limited forms of randomness [33, 34].

Due to space constraints, we only present an overview of our results. Technical details and proofs can be found in the full version of this paper [1]. In Sect. 2, we introduce all prerequisite notions. We define interval strategies and formalise our decision problems in Sect. 3. The compressed Markov chain construction, which is central in our verification and realisability algorithms, is presented in Sect. 4. Complexity results are overviewed in Sect. 5.

We write $\mathbb{N}$, $\mathbb{Q}$ and $ℝ$ for the sets of non-negative integers, rational numbers and real numbers respectively. We let ${\mathbb{N}}_{>0}$ denote the set of positive integers. We let $\overline{\mathbb{N}}=\mathbb{N}\cup \{\mathrm{\infty }\}$ and ${\overline{\mathbb{N}}}_{>0}={\mathbb{N}}_{>0}\cup \{\mathrm{\infty }\}$. Given $n,n^{\prime }\in \overline{\mathbb{N}}$, we let $⟦n,n^{\prime }⟧$ denote the set $\{k\in \mathbb{N}\mid n\le k\le n^{\prime }\}$, and if $n=0$, we shorten the notation to $⟦n^{\prime }⟧$.

Let $A$ be a finite or countable set. We write $𝒟(A)$ for the set of distributions over $A$, i.e., of functions $\mu :A\to [0,1]$ such that ${\sum }_{a\in A}\mu (a)=1$. Given a distribution $\mu \in 𝒟(A)$, we let $\mathrm{𝗌𝗎𝗉𝗉}(\mu )=\{a\in A\mid \mu (a)>0\}$ denote the support of $\mu$.

Formally, a Markov decision process (MDP) is a tuple $ℳ=(S,A,\delta )$ where $S$ is a countable set of states, $A$ is a finite set of actions and $\delta :S\times A\to 𝒟(S)$ is a (partial) probabilistic transition function. Given $s\in S$, we write $A(s)$ for the set of actions $a\in A$ such that $\delta (s,a)$ is defined. We say that an action $a$ is enabled in $s$ if $a\in A(s)$. We require, without loss of generality, that there are no deadlocks in MDPs, i.e., that for all states $s$, $A(s)$ is non-empty. We say that $ℳ$ is finite if its state space is finite.

A Markov chain can be seen as an MDP with a single enabled action per state. We omit actions in Markov chains and denote them as tuples $𝒞=(S,\delta )$ with $\delta :S\to 𝒟(S)$.

Let $ℳ=(S,A,\delta )$. A play of $ℳ$ is an infinite sequence $\pi =s_0{a}_0{s}_1{a}_1\mathrm{\dots }\in {(SA)}^{\omega }$ such that for all $\mathrm{\ell }\in \mathbb{N}$, $s_{\mathrm{\ell }+1}\in \mathrm{𝗌𝗎𝗉𝗉}(\delta (s_{\mathrm{\ell }},a_{\mathrm{\ell }}))$. A history is a finite prefix of a play ending in a state. We let $\mathrm{𝖯𝗅𝖺𝗒𝗌}(ℳ)$ and $\mathrm{𝖧𝗂𝗌𝗍}(ℳ)$ respectively denote the set of plays and of histories of $ℳ$. Given a play $\pi =s_0{a}_0{s}_1{a}_1\mathrm{\dots }$ and $n\in \mathbb{N}$, we let ${\pi }_{|n}=s_0{a}_0\mathrm{\dots }{a}_{n-1}{s}_n$ and extend this notation to histories. For any given history $h=s_0{a}_0\mathrm{\dots }{a}_{n-1}{s}_n$, we let $\mathrm{𝖿𝗂𝗋𝗌𝗍}(h)=s_0$ and $\mathrm{𝗅𝖺𝗌𝗍}(h)=s_n$. The cylinder of a history $h=s_0{a}_0\mathrm{\dots }{a}_{n-1}{s}_n$ is the set $\mathrm{𝖢𝗒𝗅}(h)=\{\pi \in \mathrm{𝖯𝗅𝖺𝗒𝗌}(ℳ)\mid {\pi }_{|n}=h\}$ of plays extending $h$. For any set of histories $\mathscr{H}$, we let $\mathrm{𝖢𝗒𝗅}(\mathscr{H})={\bigcup }_{h\in \mathscr{H}}\mathrm{𝖢𝗒𝗅}(h)$.

In a Markov chain, due to the lack of actions, plays and histories are simply sequences of states coherent with transitions. We extend the notation introduced above for plays and histories of MDPs to plays and histories of Markov chains.

A strategy describes the action choices made throughout a play of an MDP. In general, strategies can use randomisation and all previous knowledge to make decisions. Formally, a strategy is a function $\sigma :\mathrm{𝖧𝗂𝗌𝗍}(ℳ)\to 𝒟(A)$ such that for any history $h\in \mathrm{𝖧𝗂𝗌𝗍}(ℳ)$, $\mathrm{𝗌𝗎𝗉𝗉}(\sigma (h))\subseteq A(\mathrm{𝗅𝖺𝗌𝗍}(h))$, i.e., a strategy can only prescribe actions that are available in the last state of a history. A play $\pi =s_0{a}_0{s}_1\mathrm{\dots }$ is consistent with a strategy $\sigma$ if for all $\mathrm{\ell }\in \mathbb{N}$, $\sigma ({\pi }_{|\mathrm{\ell }})(a_{\mathrm{\ell }})>0$. Consistency of a history with respect to a strategy is defined similarly.

A strategy is pure if it does not use any randomisation, i.e., if it maps histories to Dirac distributions. We view pure strategies as functions $\sigma :\mathrm{𝖧𝗂𝗌𝗍}(ℳ)\to A$. A strategy $\sigma$ is memoryless if the distribution it suggests depends only on the last state of a history, i.e., if for all histories $h$ and $h^{\prime }$, $\mathrm{𝗅𝖺𝗌𝗍}(h)=\mathrm{𝗅𝖺𝗌𝗍}(h^{\prime })$ implies $\sigma (h)=\sigma (h^{\prime })$. We view memoryless strategies and pure memoryless strategies as functions $S\to 𝒟(A)$ and $S\to A$ respectively.

Given a strategy $\sigma$ and an initial state $s_{\mathrm{𝗂𝗇𝗂𝗍}}\in S$, we define a distribution ${\mathbb{P}}_{ℳ,s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }$ over measurable sets of plays in the usual way (e.g., [4]). For a Markov chain $𝒞$, due to the absence of non-determinism, we drop the strategy from this notation. If the relevant MDP or Markov chain is clear from the context, we also omit them.

In the following, we focus on memoryless strategies. If $\sigma$ is a memoryless strategy of $ℳ$, we consider the Markov chain induced by $\sigma$ on $ℳ$ as a Markov chain over $S$. Formally, it is defined as the Markov chain $(S,{\delta }^{\prime })$ such that for all $s$, $s^{\prime }\in S$, ${\delta }^{\prime }(s)(s^{\prime })={\sum }_{a\in A(s)}\sigma (s)(a)\cdot \delta (s,a)(s^{\prime })$.

One-counter MDPs (OC-MDPs) extend MDPs with a counter that can be incremented, decremented or left unchanged on each transition. Formally, a one-counter MDP is a tuple $𝒬=(Q,A,\delta ,w)$ where $(Q,A,\delta )$ is a finite MDP and $w:S\times A\to \{-1,0,1\}$ is a (partial) weight function that assigns an integer weight from $\{-1,0,1\}$ to state-action pairs. For all $q\in Q$ and $a\in A$, we require that $w(q,a)$ be defined whenever $a\in A(q)$. A configuration of $𝒬$ is a pair $(q,k)$ where $q\in Q$ and $k\in \mathbb{N}$. In the sequel, by plays, histories, strategies etc. of $𝒬$, we refer to the corresponding notion with respect to the MDP $(Q,A,\delta )$ underlying $𝒬$.

We remark that the weight function is not subject to randomisation, i.e., the weight of any transition is determined by the outgoing state and chosen action. In particular, counter values can be inferred from histories and be taken in account to make decisions in $𝒬$.

Let $𝒬=(Q,A,\delta ,w)$ be an OC-MDP. The OC-MDP $𝒬$ induces an MDP over the infinite countable space of configurations. Transitions in this induced MDP are defined using $\delta$ for the probability of updating the state and $w$ for the deterministic change of counter value. We interrupt any play whenever a configuration with counter value $0$ is reached. Intuitively, such configurations can be seen as situations in which we have run out of an energy resource. We may also impose an upper bound on the counter value, and interrupt any plays that reach this counter upper bound. We refer to OC-MDPs with a finite upper bound on counter values as bounded OC-MDPs and OC-MDPs with no upper bounds as unbounded OC-MDP.

We provide a unified definition for both semantics. Let $𝒬=(Q,A,\delta ,w)$ be an OC-MDP and let $r\in {\overline{\mathbb{N}}}_{>0}$ be an upper bound on the counter value. We define the MDP ${ℳ}^{\le r}(𝒬)=(Q\times ⟦r⟧,A,{\delta }^{\le r})$ where ${\delta }^{\le r}$ is defined, for all configurations $s=(q,k)\in Q\times ⟦r⟧$, actions $a\in A(q)$ and states $p\in Q$, by ${\delta }^{\le r}(s,a)(p,k+w(q,a))=\delta (q,a)(p)$ if $k\notin \{0,r\}$, and ${\delta }^{\le r}(s,a)(s)=1$ otherwise. The state space of ${ℳ}^{\le r}(𝒬)$ is finite if and only if $r\ne \mathrm{\infty }$.

For technical reasons, we also introduce one-counter Markov chains. In one-counter Markov chains, we authorise stochastic counter updates, i.e., counter updates are integrated in the transition function. This contrasts with OC-MDPs where deterministic counter updates are used to allow strategies to observe counter updates. We only require the unbounded semantics in this case. Formally, a one-counter Markov chain is a tuple $𝒫=(Q,\delta )$ where $Q$ is a finite set of states and $\delta :Q\to 𝒟(Q\times \{-1,0,1\})$ is a probabilistic transition and counter update function. The one-counter Markov chain $𝒫$ induces a Markov chain ${𝒞}^{\le \mathrm{\infty }}(𝒫)=(Q\times \mathbb{N},{\delta }^{\le \mathrm{\infty }})$ such that for any configuration $s=(q,k)\in Q\times \mathbb{N}$, any $p\in Q$ and any $u\in \{-1,0,1\}$, we have ${\delta }^{\le \mathrm{\infty }}(s)((p,k+u))=\delta (q)(p,u)$ if $k\ne 0$ and ${\delta }^{\le \mathrm{\infty }}(s)(s)=1$ otherwise.

Let $ℳ=(S,A,\delta )$ be an MDP. An objective is a measurable set of plays that represents a specification. We focus on variants of reachability. Given a set of target states $T\subseteq S$, the reachability objective for $T$ is defined as $\mathrm{𝖱𝖾𝖺𝖼𝗁}(T)=\{s_0{a}_0{s}_1{a}_1\mathrm{\dots }\in \mathrm{𝖯𝗅𝖺𝗒𝗌}(ℳ)\mid \exists \mathrm{\ell }\in \mathbb{N},s_{\mathrm{\ell }}\in T\}$. If $T=\{s\}$, we write $\mathrm{𝖱𝖾𝖺𝖼𝗁}(s)$ for $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\{s\})$. We assume familiarity with linear systems for reachability probabilities in finite Markov chains (see, e.g., [4]).

Let $𝒬=(Q,A,\delta ,w)$ be an OC-MDP, let $r\in {\overline{\mathbb{N}}}_{>0}$ be a counter upper bound and let $T\subseteq Q$. We consider two variants of reachability on ${ℳ}^{\le r}(𝒬)$. The first goal we consider requires visiting $T$ regardless of the counter value and the second requires visiting $T$ with a counter value of zero. The first objective is called state-reachability and we denote it by $\mathrm{𝖱𝖾𝖺𝖼𝗁}(T)$ instead of $\mathrm{𝖱𝖾𝖺𝖼𝗁}(T\times ⟦r⟧)$. The second objective is called selective termination, which is formalised as $\mathrm{𝖳𝖾𝗋𝗆}(T)=\mathrm{𝖱𝖾𝖺𝖼𝗁}(T\times \{0\})$. Like above, if $T=\{q\}$, we write $\mathrm{𝖱𝖾𝖺𝖼𝗁}(q)$ and $\mathrm{𝖳𝖾𝗋𝗆}(q)$ instead of $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\{q\})$ and $\mathrm{𝖳𝖾𝗋𝗆}(\{q\})$.

Some of our complexity bounds rely on a model of computation introduced by Blum, Shub and Smale [11]. A Blum-Shub-Smale (BSS) machine, intuitively, is a random-access memory machine with registers storing real numbers. Arithmetic computations on the content of registers are in constant time in this model.

The class of decision problem that can be solved in polynomial time in the BSS model coincides with the class of decision problems that can be solved, in the Turing model, in polynomial time with a PosSLP oracle [2]. The PosSLP problem asks, given a division-free straight-line program (intuitively, an arithmetic circuit), whether its output is positive. The PosSLP problem lies in the counting hierarchy and can be solved in polynomial space [2].

The theory of the reals refers to the set of sentences (i.e., fully quantified first-order logical formulae) in the signature of ordered fields that hold in $ℝ$. The problem of deciding whether a sentence is in the theory of the reals is decidable; if the number of quantifier blocks is fixed, this can be done in PSPACE [6, Rmk. 13.10]. Furthermore, the problem of deciding the validity of an existential (resp. universal) formula is NP-hard (resp. co-NP-hard) [6, Rmk. 13.9]. Our complexity bounds refer to the complexity classes ETR (existential theory of the reals) and co-ETR, which contain the problems that can be reduced in polynomial time to checking the membership of an existential sentence and universal sentence in the theory of the reals respectively.

Interval strategies are a subclass of memoryless strategies of ${ℳ}^{\le r}(𝒬)$ that admit finite compact representations based on families of intervals. Intuitively, a strategy is an interval strategy if there exists an interval partition (i.e., a partition containing only intervals) of the set of counter values such that decisions taken in a state for two counter values in the same interval coincide. We require that this partition has a finite representation to formulate verification and synthesis problems for interval strategies.

The set $⟦1,r-1⟧$ contains all counter values for which decisions are relevant. Let $ℐ$ be an interval partition of $⟦1,r-1⟧$. A memoryless strategy $\sigma$ of ${ℳ}^{\le r}(𝒬)$ is based on the partition $ℐ$ if for all $q\in Q$, all $I\in ℐ$ and all $k,k^{\prime }\in I$, we have $\sigma (q,k)=\sigma (q,k^{\prime })$. All memoryless strategies are based on the trivial partition of $⟦1,r-1⟧$ into singleton sets. In practice, we are interested in strategies based on partitions with a small number of large intervals.

We define two classes of interval strategies: strategies that are based on finite partitions and, in unbounded OC-MDPs, strategies that are based on periodic partitions. An interval partition $ℐ$ of ${\mathbb{N}}_{>0}$ is periodic if there exists a period $\rho \in {\mathbb{N}}_{>0}$ such that for all $I\in ℐ$, $I+\rho =\{k+\rho \mid k\in I\}\in ℐ$. A periodic interval partition $ℐ$ with period $\rho$ induces the interval partition $𝒥=\{I\in ℐ\mid I\subseteq ⟦1,\rho ⟧\}$ of $⟦1,\rho ⟧$. Conversely, for any $\rho \in {\mathbb{N}}_{>0}$, an interval partition $𝒥$ of $⟦1,\rho ⟧$ generates the periodic partition $ℐ=\{I+k\cdot \rho \mid I\in 𝒥,k\in \mathbb{N}\}$.

Let $\sigma$ be a memoryless strategy of ${ℳ}^{\le r}(𝒬)$. The strategy $\sigma$ is an open-ended interval strategy (OEIS) if it is based on a finite interval partition of $⟦1,r-1⟧$. The qualifier open-ended follows from there being an unbounded interval in any finite interval partition of ${\mathbb{N}}_{>0}$ (for the unbounded case). When $r=\mathrm{\infty }$, $\sigma$ is a cyclic interval strategy (CIS) if there exists a period $\rho \in {\mathbb{N}}_{>0}$ such that for all $q\in Q$ and all $k\in {\mathbb{N}}_{>0}$, we have $\sigma (q,k)=\sigma (q,k+\rho )$. A strategy is a CIS with period $\rho$ if and only if it is based on a periodic interval partition of ${\mathbb{N}}_{>0}$ with period $\rho$.²²2We do not consider strategies based on ultimately periodic interval partitions. However, our techniques can be adapted to analyse such strategies. Furthermore, we can show that our complexity bounds for the decision problems we study extend to this case.

We represent interval strategies as follows. First, assume that $\sigma$ is an OEIS and let $ℐ$ be the coarsest finite interval partition of $⟦1,r-1⟧$ on which $\sigma$ is based. We can represent $\sigma$ by a table that lists, for each $I\in ℐ$, the bounds of $I$ and a memoryless strategy of $𝒬$ dictating the choices to be made when the current counter value lies in $I$. Next, assume that $r=\mathrm{\infty }$ and that $\sigma$ is a CIS with period $\rho$. Let $𝒥$ be an interval partition of $⟦1,\rho ⟧$ such that $\sigma$ is based on the partition $ℐ$ generated by $𝒥$. We represent $\sigma$ by $\rho$ and an OEIS of ${ℳ}^{\le \rho +1}(𝒬)$ based on $𝒥$ that specifies the behaviour of $\sigma$ for counter values up to $\rho$.

Interval strategies subsume counter-oblivious strategies, i.e., memoryless strategies that make choices based only on the state and disregard the current counter value. Counter-oblivious strategies can be viewed as memoryless strategies $\sigma :Q\to 𝒟(A)$ of $𝒬$.

Memoryless strategies of ${ℳ}^{\le r}(𝒬)$ can be seen as strategies of $𝒬$ when an initial counter value is fixed. The idea is to use memory to keep track of the counter instead of observing it. We can thus compare our representation of interval strategies to the classical Mealy machine representation of the corresponding strategies of $𝒬$. The following discussion is formalised in the full version of this paper [1].

If $r\in \mathbb{N}$, the counterpart in $𝒬$ of any OEIS has finite memory: there are only finitely many counter values. However, a Mealy machine for this strategy can require a size exponential in the binary encoding of $r$ (which occurs in the OEIS representation). Below, we illustrate this claim and that, if $r=\mathrm{\infty }$, then counterparts in $𝒬$ of OEIS may require infinite memory.

We now assume that $r=\mathrm{\infty }$ and that $\sigma$ is a CIS. Its counterpart in $𝒬$ is a finite-memory strategy: by periodicity of $\sigma$, it suffices to keep track of the remainder of division of the counter value by the period. By adapting Ex. 1, we can show that a CIS representation may be exponentially more succinct than any Mealy machine for its counterpart in $𝒬$.

We formulate the decision problems studied in following sections. The common inputs of these problems are an OC-MDP $𝒬$ with rational transition probabilities, a counter bound $r\in {\overline{\mathbb{N}}}_{>0}$ (encoded in binary if it is finite), a target $T\subseteq Q$, an objective $\mathrm{\Omega }\in \{\mathrm{𝖱𝖾𝖺𝖼𝗁}(T),\mathrm{𝖳𝖾𝗋𝗆}(T)\}$, an initial configuration $s_{\mathrm{𝗂𝗇𝗂𝗍}}=(q_{\mathrm{𝗂𝗇𝗂𝗍}},k_{\mathrm{𝗂𝗇𝗂𝗍}})$ and a threshold $\theta \in [0,1]\cap \mathbb{Q}$ against which we compare the probability of $\mathrm{\Omega }$. Problems that are related to CISs assume that $r=\mathrm{\infty }$ as all strategies in the bounded case are OEISs. We lighten the probability notation below by omitting ${ℳ}^{\le r}(𝒬)$ from it.

First, we are concerned with the verification of interval strategies. The interval strategy verification problem asks to decide, given an interval strategy $\sigma$, whether ${\mathbb{P}}_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })\ge \theta$. We assume that the encoding of the input interval strategy matches the description above.

The other two problems relate to interval strategy synthesis. The corresponding decision problem is called realisability. We provide algorithms checking the existence of well-performing structurally-constrained interval strategies. We formulate two variants of this problem.

For the first variant, we fix an interval partition $ℐ$ of $⟦1,r-1⟧$ beforehand and ask to check if there is a good strategy based on $ℐ$. Formally, the fixed-interval OEIS realisability problem asks whether, given a finite interval partition $ℐ$ of $⟦1,r-1⟧$, there exists an OEIS $\sigma$ based on $ℐ$ such that ${\mathbb{P}}_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })\ge \theta$. The variant for CISs is defined similarly: the fixed-interval CIS realisability problem asks whether, given a period $\rho \in {\mathbb{N}}_{>0}$ and an interval partition $𝒥$ of $⟦1,\rho ⟧$, there exists a CIS $\sigma$ based on the partition generated by $𝒥$ such that ${\mathbb{P}}_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })\ge \theta$.

For the second variant, we parameterise the number of intervals in the partition and the size of bounded intervals. The parameterised OEISs realisability problem asks, given a bound $d\in {\mathbb{N}}_{>0}$ on the number of intervals and a bound $n\in {\mathbb{N}}_{>0}$ on the size of bounded intervals, whether there exists an OEIS $\sigma$ such that ${\mathbb{P}}_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })\ge \theta$ and $\sigma$ is based on an interval partition $ℐ$ of $⟦1,r-1⟧$ with $|ℐ|\le d$ and, for all bounded $I\in ℐ$, $|I|\in ⟦1,n⟧$ (in particular, the parameter $n$ does not constrain the required infinite interval in the unbounded setting $r=\mathrm{\infty }$). The parameterised CIS realisability problem asks, given a bound $d\in {\mathbb{N}}_{>0}$ on the number of intervals and a bound $n\in {\mathbb{N}}_{>0}$ on the size of intervals, whether there exists a CIS $\sigma$ such that ${\mathbb{P}}_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })\ge \theta$ and $\sigma$ is based on an interval partition $ℐ$ of ${\mathbb{N}}_{>0}$ with period $\rho$ such that $|I|\le n$ for all $I\in ℐ$ and $ℐ$ induces a partition of $⟦1,\rho ⟧$ with at most $d$ intervals. In both cases, we assume that the number $d$ is given in unary. This ensures that witness strategies, when they exist, are based on interval partitions that have a representation of size polynomial in the size of the inputs.

For both realisability problems, we consider two variants, depending on whether we want the answer with respect to the set of pure or randomised interval strategies. For many objectives in MDPs (e.g., reachability, parity objectives [4, 13]), the maximum probability of satisfying the objective is the same for pure and randomised strategies. As highlighted by the following example, when we restrict the structure of the sought interval strategy, there may exist randomised strategies that perform better than all pure ones. Intuitively, randomisation can somewhat alleviate the loss in flexibility caused by structural restrictions [23].

Let $\sigma$ be an interval strategy. First, assume that $\sigma$ is an OEIS. We comment on the CIS case below. Let $ℐ$ be a refinement of the interval partition from the encoding of $\sigma$ such that ${𝒞}_{ℐ}^{\sigma }$ is well-defined and $k_{\mathrm{𝗂𝗇𝗂𝗍}}$ is an interval bound in $ℐ$ (thus $s_{\mathrm{𝗂𝗇𝗂𝗍}}\in S_{ℐ}$). We can construct this partition in polynomial time with respect to the input size.

By Thm. 6 and Rmk. 7, ${\mathbb{P}}_{{ℳ}^{\le r}(𝒬),s_{\mathrm{𝗂𝗇𝗂𝗍}}}^{\sigma }(\mathrm{\Omega })$ is equal to a reachability probability from $s_{\mathrm{𝗂𝗇𝗂𝗍}}$ in ${𝒞}_{ℐ}^{\sigma }$. To analyse ${𝒞}_{ℐ}^{\sigma }$, we use different approaches for bounded and unbounded OC-MDPs.

In the bounded case, we can decide the problem in polynomial time in the BSS model. By Thm. 9, we can explicitly compute the transition probabilities of ${𝒞}_{ℐ}^{\sigma }$. These can be used to compute the relevant reachability probabilities (by solving a linear system) and conclude.

In general, we can show that the verification problem is in co-ETR. From the characterisation of transition probabilities of ${𝒞}_{ℐ}^{\sigma }$ in Thm. 8, we can derive a formula ${\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳(\sigma ))$ where $𝐱$ are variables representing transition probabilities of ${𝒞}_{ℐ}^{\sigma }$, $𝐳(\sigma )$ are strategy probabilities of $\sigma$, and the least satisfying assignment of $𝐱$-variables in ${\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳(\sigma ))$ contains the transition probabilities of ${𝒞}_{ℐ}^{\sigma }$. Similarly, we can build a formula ${\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲)$ from the linear system for reachability probabilities in ${𝒞}_{ℐ}^{\sigma }$, where $𝐲$ are the variables for the relevant reachability probabilities with respect to $\mathrm{\Omega }$. By construction, any vectors ${𝐱}^{\star }$ and ${𝐲}^{\star }$ such that $ℝ\vDash {\mathrm{\Phi }}_{\delta }^{ℐ}({𝐱}^{\star },𝐳(\sigma ))\wedge {\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}({𝐱}^{\star },{𝐲}^{\star })$ are over-estimations of the probabilities of interest. Thus, the verification problem amounts to checking if $ℝ\vDash \forall 𝐱\forall 𝐲(({\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳(\sigma ))\wedge {\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲))⟹y_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}\ge \theta )$, where $y_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}$ is the variable for the reachability probability from $s_{\mathrm{𝗂𝗇𝗂𝗍}}$ in ${𝒞}_{ℐ}^{\sigma }$.

We now informally comment on how to adapt the technique for OEIS to obtain a co-ETR upper bound when $\sigma$ is a CIS. The main technical difference is that we apply the compression technique twice. We apply the compression first to obtain the infinite Markov chain ${𝒞}_{ℐ}^{\sigma }$. We then consider the one-counter Markov chain ${𝒫}_{𝒥}^{\sigma }$ that generates it (Lem. 10) and use a compression to analyse it (Rmk. 5). In the end, we construct a formula similarly to above, with an additional sub-formula for the transition probabilities of the additional compression.

We consider the fixed-interval realisability problem. We first discuss the variant for pure strategies. It suffices to non-deterministically guess a pure interval strategy based on the input interval partition of $⟦1,r-1⟧$ and verify this strategy. In our complexity analysis, we treat verification as a part of the procedure and not as an oracle. We obtain that the fixed-interval realisability problem for pure strategies is in ${\text{NP}}^{\text{PosSLP}}$ for OEIS in bounded OC-MDPs and in ${\text{NP}}^{\text{co-ETR}}={\text{NP}}^{\text{ETR}}$ for OEIS and CIS in unbounded OC-MDPs. In particular, we have a PSPACE upper bound.

For randomised strategies, we quantify existentially over strategy variables in the verification formulae. We illustrate the case of OEISs with an interval partition $ℐ$. We introduce a new sub-formula ${\mathrm{\Phi }}_{\sigma }^{ℐ}(𝐳)$ that holds if and only if the interpretation of the variables $𝐳$ are strategy probabilities. Solving the fixed-interval realisability problem can be reduced to checking if $ℝ\vDash \exists 𝐳\forall 𝐱\forall 𝐲({\mathrm{\Phi }}_{\sigma }^{ℐ}(𝐳)\wedge ({\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳)\wedge {\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲))⟹y_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}\ge \theta )$. For CISs, we can follow the same reasoning. We obtain a PSPACE algorithm (see Sect. 2).

We refine this approach for bounded OC-MDPs. Assume that the supports of the distributions of the strategy to be synthesised, i.e., which of the variables of $𝐳$ have a positive assignment, are fixed. With this assumption, we can modify the conjunction ${\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳)\wedge {\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲)$ of the verification formula by using Thm. 9 so that for any valuation of $𝐳$ compatible with the supports, the only valuation of $𝐱$ and $𝐲$ satisfying this conjunction is made of the probabilities represented by these variables. We can refine the system underlying ${\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲)$ because Thm. 9 indicates the transitions of the compressed chain that have a positive probability. We obtain an ${\text{NP}}^{\text{ETR}}$ complexity as follows: we non-deterministically guess some strategy distribution supports and then check if $ℝ\vDash \exists 𝐳\exists 𝐱\exists 𝐲({\mathrm{\Phi }}_{\sigma }^{ℐ}(𝐳)\wedge {\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳)\wedge {\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲)\wedge y_{s_{\mathrm{𝗂𝗇𝗂𝗍}}}\ge \theta )$ where ${\mathrm{\Phi }}_{\sigma }^{ℐ}(𝐳)$ only allows strategies with the guessed support and ${\mathrm{\Phi }}_{\delta }^{ℐ}(𝐱,𝐳)$ and ${\mathrm{\Phi }}_{\mathrm{\Omega }}^{ℐ}(𝐱,𝐲)$ have been adapted by applying the result of Thm. 9.

We consider the input parameters $d$ for the number of intervals and $n$ for the bound on the size of finite intervals. Intuitively, we non-deterministically construct an interval partition compatible with $d$ and $n$ and then use algorithms for the fixed case. Due to the assumption that $d$ is given in unary, the guessed partition can be represented in polynomial space. To obtain the same complexity upper bounds for parameterised realisability as for fixed-interval realisability, we consider the algorithms for fixed-interval realisability as a part of the overall procedure and not as oracles in our complexity analyses.

All of the problems discussed above are square-root-sum-hard. The square-root-sum problem asks, given integers $x_1,\mathrm{\dots },x_n\in \mathbb{N}$ and $y\in \mathbb{N}$, whether ${\sum }_{i=1}^n\sqrt{x_i}\ge y$. The square-root-sum problem can be solved in polynomial time in the BSS model [42] but is not known to lie in NP. In the unbounded case, the hardness can be obtained by relying on an existing reduction for one-counter Markov chains [26]. For the bounded setting, we build on the same construction. The main hurdle is to establish that we can, in polynomial time, compute a large enough counter bound so the bounded one-counter Markov chain approximates the one used in the unbounded reduction well enough for the reduction to still be valid. We also provide a reduction from the Hamiltonian cycle problem to the counter-oblivious realisability problem for selective termination, implying its NP-hardness [28]. This implies the NP-hardness of our two realisability problems.