arXiv CSopen access

Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes

Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes Konstantin Kueffner1 , Tobias Meggendorfer2 , Maximilian Weininger3 , and Patrick Wienhöft4

arXiv:2606.25797v1 [cs.AI] 24 Jun 2026

1

Institute of Science and Technology Austria, Klosterneuburg, Austria 2 Lancaster University Leipzig, Leipzig, Germany 3 Ruhr-University Bochum, Bochum, Germany 4 TUD Dresden University of Technology, Dresden, Germany

Abstract. Markov decision processes (MDPs) are a classic model of decision making under uncertainty, exhibiting both non-deterministic choice as well as probabilistic uncertainty. Traditionally, exact knowledge of the underlying probabilities is assumed. However, this often is unrealistic, e.g. when modelling cyber-physical systems or biological processes. Here, statistical methods provide a way towards obtaining meaningful guarantees. The classical approach is to gather samples in the MDP, use these to draw statistical conclusions about the transition probabilities, and from there obtain bounds on the true value; then, if these bounds are too broad, repeat. However, existing implementations of this approach are either subtly incorrect or sub-optimal, and quite often both. We present several confidence sequences, which are specifically designed for such “online” settings, implement all of them in an efficient tool, and show their practical applicability. In particular, we show that they outperform classical “union-bound” style approaches, and overall our implementation requires 50x less samples on average than previous state of the art. Keywords: Probabilistic verification · Statistical model checking · Markov decision processes · Confidence intervals

1

Introduction

Markov decision processes (MDPs) [55] are the classic modelling formalism for dynamic systems with probabilistic and nondeterministic behaviour. Taking one of the available actions in each state moves the system to a successor state, which is chosen from a probability distribution associated with the state-action pair. This is aleatory uncertainty, i.e. the inherent randomness of the process, e.g. a coin toss. However, there may also be epistemic uncertainty (lack of knowledge), e.g. not knowing the bias of the coin, see [8]. While verification procedures traditionally assume full knowledge of the MDP (also called “white box”, with no epistemic uncertainty), over the past decade there has been an increasing interest in reliable analysis of MDPs where the exact transition probabilities are unknown (grey box) or even the presence of the transitions (positivity of the transition probability) is unknown (black box). For example, consider the task of finding the optimal probability of getting heads from a coin toss when choosing among multiple coins. Given knowledge of the coins’ biases (white box),

2

K. Kueffner et al.

we clearly choose the coin with the highest biases towards heads. This does not guarantee winning (there still is aleatoric uncertainty), but we know which coin to pick and the resulting value (the chances we get). With unknown biases (grey box), we cannot with certainty determine the value nor choose the best coin. Statistical model checking (SMC) [70] tackles this problem by gathering simulations of the system (e.g. tossing each coin several times) and drawing statistical conclusions from the obtained data. One of the strongest guarantees possible are probably approximately correct (PAC) results, where the reported value is ε-close to the true result with confidence at least γ. When considering discounted or finite-horizon objectives, the distance between estimation and true value can be upper-bounded for paths of a certain length. Thus, PAC-guarantees and even bounds on sample-complexity can be derived in a straightforward manner, see e.g. [1,39,32,58,61,66]. In contrast, for infinite-horizon objectives, more involved methods are required. There, the prevalent approach to obtain PAC guarantees (in the grey box setting) [4,65,2,59,9,7,54] is to repeat the following three steps: (i) Sample the unknown MDP, counting occurrences of every transition, (ii) Infer an interval MDP (IMDP) [27] by obtaining confidence intervals of the transition probabilities, and finally (iii) Solve the IMDP, obtaining lower and upper bounds a, b, that, with probability γ, bound the true value of the unknown MDP, i.e. v ∈ [a, b]. If additionally |b − a| < ε, the algorithm terminates; otherwise, it repeats the steps, i.e. gathers more data, increasing the precision of the confidence intervals in the IMDP, until a and b are ε-close. However, existing variants rely on flawed correctness arguments or are too conservative, and quite often both. Firstly, naively repeating the three steps compromises the PAC-guarantee, as the entire confidence γ is “reused” across multiple Infers. Intuitively, this is akin to repeating a statistical experiment until the result “looks right”. (In App. B we provide a general counterexample based on the law of iterated logarithm [40,28].) Secondly, the used statistical methods are overly conservative: On the one hand, the statistical methods used in Infer are suboptimal, providing wide confidence intervals, in turn requiring more samples, see [53]. However, even the “optimal” methods of [53] are sub-optimal when we can repeatedly interact with the system. Intuitively, estimates for the same distribution in different Infer steps do not exploit the fact that the samples they are working with actually stem from the same distribution. So, on the other hand, strictly dividing the process into these three phases is fundamentally problematic. Contributions. We improve SMC with PAC guarantees for MDPs by employing confidence sequences [23]. For a stream of samples, these yield a stream of estimates with a statistical guarantee for the entire (arbitrarily long) stream. Using such sequentially correct estimates, we address the flawed correctness proof of previous works. Moreover, confidence sequences exploit the fact that estimates at different times are not independent, also replacing previous overly conservative estimates and significantly reducing the required number of samples. Technically, we analyse gridded variants of classical confidence intervals such as Hoeffding [35], (empirical) Bernstein [49], and Clopper-Pearson [21]. Moreover, we adapt several confidence sequences, based on stitching [37], betting [64], and test-martingales [64], to our setting. Finally, we introduce a novel value-based

Confidence Sequences for Online MDP-SMC

3

hypothesis test for SMC, which entirely circumvents estimating probabilities. For all these methods, we discuss correctness, convergence, and computability. Practically, we provide an efficient, extensible Java tool embedding the confidence sequences not only in the state-of-the-art Sample-Infer-Solve pipeline, but also a new interwoven approach. Our new variant exploits the continuous guarantees of confidence sequences to avoid constructing an IMDP for the whole model and instead locally applies the robust value iteration of [52]. This enables soundly incorporating guidance heuristics for sampling [16] and utilizing the novel valuebased hypothesis test. Our evaluation shows a significant reduction in the number of samples required, on average 50x less than state-of-the-art, and that all of our contributions (confidence sequences, in particular the value test, and our interwoven approach) are instrumental to this improvement. Additionally, our evaluation provides, to our knowledge for the first time, an empirical comparison of all presented statistical methods, both on single distributions and on SMC of MDPs. This additionally demonstrates the benefits of confidence sequences and their individual strengths and weaknesses, also beyond our focus of SMC for MDPs. Related Work Sec. 2.3 discusses other works on SMC of MDPs. App. A details common SMC assumptions and how they reduce to the grey box setting we consider. Other Formalisms for System and Specification. Continuous time systems can be tackled by estimating transitions rates from samples [2,5]. Continuous space systems can be approached by abstraction to finite-state MDPs [7]; the incurred abstraction error can be transparently incorporated in the underlying robust value iteration [52] by expanding the uncertainty set. For objectives, we focus on reachability specifications for simplicity but again can directly extend others as long as robust value iteration supports them: Technically, our work provides statistically sound bounds on the Bellman backup used in robust value iteration. SMC for Markov Chains. In Markov chains, the motivation for SMC is fundamentally different: The system usually is assumed to be known, but too large to handle, see e.g. [70,19]. Since there is no non-determinism in Markov chains, one can, intuitively, just repeatedly sample entire paths from the system to gain a statistical estimate on the probability of reaching the goal. In many cases, this is significantly faster than explicit computation, yielding a precision-performance trade-off (faster results but only with PAC guarantees), in particular since the exact model description is known, and successor states can be sampled very efficiently. In contrast, for MDPs the main motivation is an inherent lack of knowledge of transition dynamics, and the underlying systems are usually very costly to simulate, shifting the focus from speed to reducing sample count. Other Forms of Guarantees. When obtaining samples according to a behavioural policy, one can guarantee an improvement over this policy [68]. In our setting, we explicitly explore unsafe states, while in a “safe online” setting, safety has to be guaranteed already while exploring the system. In this direction, we refer to works on shielding [3], PAC online learning [43,42] and regret minimization [61].

4

K. Kueffner et al.

2

Preliminaries

In this section, we summarize all relevant theory necessary to explain our contributions. Since our work touches upon many different topics, we keep this section brief and refer the reader to cited literature for further information. We assume familiarity with the basics of probability theory (see e.g. [13]) and statistics (see e.g. [62]). A probability P distribution over a countable set X is a mapping d : X → [0, 1], such that x∈X d(x) = 1. The set of all probability distributions over X is D(X). For a set S, we denote by S ∗ (S ω ) the set of all (in)finite sequences over S. 2.1

Markov Decision Processes

A Markov decision process (MDP), e.g. [55], is a tuple M = (S, A, P), where S is a finite set of states; A is a finite set of actions, overloaded to yield for each state s ∈ S a non-empty set of available actions A(s) ⊆ A; and P : S × A ⇀ D(S) is the (partial) transition function, that yields for each state s ∈ S and a ∈ A(s) the associated distribution over successor states P(s, a). For simplicity, we write P(s, a, r) instead of P(s, a)(r). The semantics of MDPs are defined as usual by means of paths, strategies, and the probability measure in the induced Markov chain, see [11, Chp. 10] for an extensive introduction. An infinite path is a sequence of state-action pairs ρ = s1 a1 s2 a2 · · · ∈ (S × A)ω with P(si , ai , si+1 ) > 0. We denote by ρ(i) the i-th state si in a path ρ and by PathsM the set of all infinite paths. A (memoryless deterministic, MD) strategy is a mapping π : S → A, choosing one enabled action in each state, i.e. π(s) ∈ A(s). (For our purposes, MD strategies are sufficient.) MD We write ΠM to refer to all MD strategies. Complementing an MDP M with such a strategy yields a Markov chain, which together with an initial state ŝ ∈ S induces a unique probability measure PrπM,ŝ over infinite paths [11, Chp. 10.1]. An objective formalises the goal of the MDP. For simplicity, we focus on reachability, but our methods easily generalize to other relevant objectives such as total reward, too. A reachability objective concerns the probability to reach a given set of goal states G ⊆ S. Formally, denote the set of paths that eventually reach G as ♢G := {ρ ∈ PathsM | ∃i. ρ(i) ∈ G}. The value of a state is the maximum probability to achieve the objective, i.e. reach the goal states, under any strategy, π formally VM,♢G (s) := maxπ∈ΠM MD PrM,s [♢G]. We omit the subscripts of V where clear from the context. MD strategies are sufficient for optimal reachability [11, Lem. 10.102]. We are interested in approximating the value in a given initial state ŝ, i.e. compute v such that |VM (ŝ) − v| ≤ ε for a given ε > 0. A classical approach to solve this problem is value iteration (VI), the method of choice in most modern tools due to empirical scalability [30]. Starting from an initial value vector LP 0 (s) = 1 if s ∈ G and 0 otherwise, VI iterates the Bellman backup B(s, a, V ) = r∈S P(s, a, r)·V (r), setting Li+1 (s) = maxa∈A(s) B(s, a, Li ). Intuitively, Li (s) describes the maximal probability to reach G from s in i steps. Li converges monotonically to the correct value, i.e. Li (s) ≤ Li+1 (s) ≤ V(s) for all i and limi→∞ Li (s) = V(s) [20]. Through a similar, but technically more involved process, we also obtain converging upper bounds Ui (see e.g. [29,41]), allowing to stop once Ui (ŝ) − Li (ŝ) ≤ ε.

Confidence Sequences for Online MDP-SMC

2.2

5

Statistical Model Checking

In the classical setting, the entire MDP is provided as input. In this work, we deal with MDPs where the exact transition probabilities are unknown. Instead, we have sampling access to the system: Starting in the initial state, we can choose an available action a ∈ A(s), take a step according to the probability distribution P(s, a) associated with a, observe the successor state r we end up in, and repeat the process. Moreover, we can reset the system into its initial state, i.e. we can sample (finite) paths in the MDP. Repeatedly interacting with the system in this way allows us to draw statistical conclusions. For example, consider an MDP modelling a simple coin toss with unknown bias. By tossing several times, we can get a statistical estimate on its bias: Tossing a coin 1000 times and seeing 400 heads, we can conclude that the actual bias of the coin likely lies in the uncertainty set [0.3, 0.5]. (We discuss the details on obtaining such estimates later.) However, the true bias might actually be different and we just observed an unlikely outcome, hence we can never be certain. Thus, we can only aim for a probably approximately correct (PAC) result, i.e. given a confidence requirement γ and precision requirement ε, we want a value v such that |V(ŝ) − v| ≤ ε with confidence γ. For readability, we write δ = 1 − γ for the allowed error probability. By applying statistical methods to each action of the MDP separately (e.g. using the union bound), we can obtain estimates of their behaviour (e.g. bounds on the transition probabilities) [53], and in turn compute bounds on the value using robust value iteration [27,52]. The key ingredient this method requires is obtaining lower bounds on the Bellman backup, i.e. an operator L which for any value function V : S → R P and state-action pair s ∈ S, a ∈ A(s) yields a value L(s, a, V ) ≤ B(s, a, V ) = r∈S P(s, a, r) · V (r). Intuitively, when using L instead of B, the Li we obtain still are lower bounds on the true value. If the values returned by L additionally “tighten” over the execution of an algorithm, we converge to the true value. As further details of this approach are beyond our scope (e.g. how to obtain matching upper bounds), we refer to [41,52]. Finally, observe that we assume an online setting, meaning that we can gather further samples on demand and actively drive the interaction with the system by choosing which actions to take during sampling. In contrast, e.g. [53] assumes to be given a fixed set of samples, with no option of gathering additional ones. As we see later, this significantly changes which solution approaches are adequate. For simplicity, we assume to know the support of P, i.e. whether P(s, a, s′ ) > 0, often called “grey box” [4,12,2]. We distinguish two independent modelling choices. First, sampling access specifies how observations are obtained. In the strongest setting, one may sample any state-action pair directly. In the simulation setting, one may only start in the initial state and then sample finite paths by choosing actions online. In the batch setting, one is given a fixed data set of past transitions and cannot actively collect further samples. We work in the simulation setting: samples are obtained along finite paths, but the algorithm may reset to the initial state and may choose actions adaptively. Second, knowledge of the transition structure specifies what is known about the unknown transition function. In the whitebox setting, the full transition probabilities are known. In the grey-box setting,

6

K. Kueffner et al.

the support of every transition distribution is known, but the probabilities are unknown. In the black-box setting, the support is unknown, but one may assume a positive lower bound pmin on all non-zero transition probabilities. Without either support information or such a lower bound, finite samples cannot rule out an unseen transition of arbitrarily small probability; hence PAC guarantees for infinite-horizon reachability are impossible in general. For the rest of the paper, we focus on the online grey-box setting. Black-box models can be handled by first using part of the confidence budget to learn the support, thereby reducing to the grey-box case; details and minor variants are deferred to App. A. We can formulate our problem as follows. Problem: Online Grey Box MDP-SMC Input: An MDP M with unknown transition probabilities P (but known support) and sampling access, a set of goal states G, a precision requirement ε > 0, and a confidence requirement γ > 0. Output: A value v such that |v − V(ŝ)| ≤ ε with confidence at least γ. As motivated before, we additionally are interested in keeping the number of required interactions with the system as low as possible. We deliberately leave “as low as possible” vague: It is surprisingly challenging to formally define this notion already for a single distribution. As observed in e.g. [53, Sec. 3.3], how many samples different methods require to achieve a given precision heavily depends on the shape of the distribution (e.g. the true probability), and focusing only on worst cases is not necessarily meaningful in practice. 2.3

Existing Methods and the SOTA MDP-SMC Framework

We survey existing methods and categorize them using an informal, unifying framework. Most approaches work in the grey box setting, i.e. for each state-action pair we do not know the precise probabilities but the set of successors. Relatedly, most approaches are model-based (an informal notion, intuitively meaning that the underlying graph is constructed, i.e. the space requirement is O(|P|)). This includes [4,65,2,59,9,7,54], which all exhibit a common structure: They Sample the MDP some finite number of times, from these samples Infer confidence intervals on the transition probabilities, and finally Solve the induced IMDP, yielding bounds on the true value. If the bounds are not tight enough, too little data has been gathered, and they go back to the first step. However, as mentioned, these methods all suffer from severe drawbacks. Firstly, most works “reuse” the entire confidence budget in every Infer step, which in general is statistically incorrect, as demonstrated in Ex. 1 and further discussed in App. B. This issue is present in most works on SMC [65,2,59,9,7,54], invalidating their proofs of correctness. (see App. B for details). Only in [4], this is (naively) addressed by exponentially distributing confidence over all Infer steps, ensuring soundness of all Infers by union bound. Example 1. Consider an MDP with states s1 , s2 , s+ , s− , initial state s1 , target state s+ , and sink state s− . There is one action a in s1 , with P (s1 , a, s2 ) = p,

P (s1 , a, s− ) = 1 − p,

Confidence Sequences for Online MDP-SMC

7

and one action b in s2 , with P (s2 , b, s+ ) = 1. Thus the reachability value from s1 is exactly p. Suppose an SMC procedure repeatedly constructs fixed-time confidence intervals and stops once the resulting value interval has width below ε. Even if each individual interval is valid at its pre-specified sample size, the stopping time is data-dependent: the procedure continues precisely until the interval looks sufficiently favourable. Thus the final interval is not covered by the fixed-time guarantee. In particular, for rate-optimal fixed-time intervals containing the empirical mean, the law of the iterated logarithm implies that the empirical p estimate will almost surely cross any fixed 1/t-width boundary infinitely often. Hence there are data-dependent stopping times at which the returned interval excludes the true value with probability one. This is the core reason why fixed-time confidence intervals cannot simply be reused across repeated Infer calls. Secondly, existing methods use sub-optimal or incorrect statistical methods (usually the general and overly conservative Hoeffding / Okomato bound). While [19,53] tackle this for Markov chain SMC and the “offline” MDP-SMC setting, none discuss how to adapt to an online setting, where we need to repeatedly draw statistical conclusions. The case where the topology is unknown, i.e. black box, intuitively corresponds to not knowing how many sides the coin we are tossing has. The crux of this setting is to reason about the infinite time behaviour (e.g. “can the goal still be reached?”) based on finite samples. Notably, without any assumptions, it is impossible to give any guarantees on infinite-horizon behaviour. Suppose we want the probability of eventually getting heads from repeatedly tossing a coin. This is 1 if the chance for heads is non-zero, and 0 otherwise. However, from seeing finitely many tails we cannot conclude that the chance of heads is 0. Two approaches tackle this case directly. DQL [16] only relies on a lower bound on transition probabilities and upper bound on state and action count. This however comes at the cost of requiring an astronomical amount of samples already on toy examples [4, Tbl. 1]. In contrast, [26] requires (among others) knowledge of the mixing time of the MDP, which allows to extrapolate from (large) finite samples to their infinite time behaviour. An a-priori bound for the mixing time is exponential in the size of the MDP and leads to similarly large sample requirements. As such, the standard approach is to separately learn the topology (using mild assumptions, see e.g. [53, Rem. 2]) to “recover” the grey box case (see App. A for details). As this “reduction” is based on estimating probabilities, it directly profits from our improvements, too.

3

Improving Online MDP-SMC

In this section, we introduce several approaches to statistical estimations in the online MDP-SMC setting. Recall that we aim to obtain a safe and converging under-approximation L of the Bellman backup in every state-action pair. We introduce several statistical methods that allow us to obtain such approximations which (i) are correct with high confidence and (ii) get more precise the more samples we gather. Together, this then gives us converging bounds on the true value which are correct with high confidence.

8

K. Kueffner et al.

As mentioned, we distribute our confidence over all state-action pairs using the union bound, allowing us to focus on the problem localized to a single state-action pair s ∈ S and a ∈ A(s). We model the observations at this state-action pair as an i.i.d. process of successor-state samples Z = (Zt )t∈N+ with Zt ∼ P(s, a) for all t ∈ N+ , where each realisation zt lies in S. In other words, we focus on samples obtained from a finite-support distribution and fix as underlying probability space infinite sequences drawn i.i.d. from this distribution. Due to space constraints, formal definitions of known notions are provided in App. C and proofs in App. D. The algorithm for MDP-SMC is outlined in Sec. 3.4. Notation. Throughout the section, we write P = P(s, a) for the underlying distribution, r ∈ S for a successor state, R = {r ∈ S | P (r) > 0} for all successors, and t ∈ N+ for a point in time. Given a sequence z = (zt )t∈N+ we write z1:t = (z1 , . . . , zt ) for every t ∈ N+ . For every r ∈ S we denote the Pt transition count and empirical transition probability as ξr (z1:t ) := i=1 1zi =r and µr (z1:t ) := 1t ξr (z1:t ). Value estimation. In the most general form, we aim to find a functor V that, given an error threshold and a sequence of observations, maps value functions V : S → R over successors to a subset of the real numbers (typically an interval), containing the Bellman backup of V . Formally, we want for every δ ∈ (0, 1) that h i X Pr ∀t ∈ N+ .∀V : S → R. P (r) · V (r) ∈ V(δ; Z1:t )(V ) ≥ 1 − δ. (1) r∈S

Intuitively, this guarantees that with high confidence all Bellman backups performed using V contain the true value, allowing to use L(s, a, V ) = inf V(δ; Z1:t )(V ). Observe that the ∀t is inside the Pr operator. This is essential in our online setting, as it permits adaptively gathering samples until sufficient precision is achieved. (We show in App. D.2 that this requirement is equivalent to requiring correctness at termination.) Such a value estimation can be obtained by estimating the distribution P , as follows. Distribution estimation. Formally, we want a function C : (0, 1) × S ∗ → 2D(S) that maps a sequence of observations to a confidence set of distributions, i.e. satisfying Pr [∀t ∈ N+ . P ∈ C(δ; P Z1:t )] ≥ 1 − δ. From this, we obtain a value estimate by V(δ; Z1:t )(V ) = { r∈S Q(r) · V (r) | Q ∈ C(δ; Z1:t )}. Probability estimation. The common approach to obtain such a set is to estimate each transition probability individually and combine the results. Formally, for every r we seek a function Cr : (0, 1) × S ∗ → 2[0,1] that maps observations to an uncertainty set over the single transition probability, satisfying Pr [∀t ∈ N+ . P (r) ∈ Cr (δ; Z1:t )] ≥ 1 − δ.

(2)

×

This gives a distribution estimate by C(δ; Z1:t ) = r∈R Cr (δ/|R|; Z1:t ) through the union bound. Thus, we first focus on estimating a single transition probability. 3.1

Grid Constructions

To estimate individual transition probabilities, one might be tempted to use standard statistical estimates (e.g. the Hoeffding inequality) to repeatedly infer

Confidence Sequences for Online MDP-SMC

9

bounds. However, as we outline in Lem. 1 and App. B, such naive use of fixed-time confidence intervals in an online context (i.e. “reusing” the confidence multiple times) is unsound. Instead, we suggest to spread the available confidence over an (a-priori fixed) grid using the union bound, yielding correctness (Thm. 1). Interestingly, the shape of the grid has significant influence on the convergence rate (Thm. 2), potentially even leading to divergence (Cor. 1). Confidence intervals. A (fixed-time) confidence interval Ir : (0, 1) × S ∗ → 2[0,1] guarantees for all t ∈ N+ that Pr [P (r) ∈ Ir (δ; Z1:t )] ≥ 1 − δ. Crucially, although this guarantee holds for any a-priori fixed t, it does not imply Eq. (2) (observe that the “for all” is outside Pr). For example, if we infer at both t1 = 100 and t2 = 200, the probability getting at least one estimate wrong may be larger than δ. We show that this occurs for all rate-optimal confidence intervals containing the empirical average (see App. C.1), including the commonly used Hoeffding [35], (empirical) Bernstein [49], and Clopper-Pearson intervals [21] (see App. C.2). Rate-optimal fixed-time intervals. Let Ir : (0, 1) × S ∗ → 2[0,1] be a fixed-time confidence interval for the transition probability P (r). We call Ir empirically anchored if, for all t ∈ N+ , all δ ∈ (0, 1), and all z1:t ∈ S t , µr (z1:t ) ∈ Ir (δ; z1:t ). Its maximal width at time t is
WIr (δ, t) := sup sup Ir (δ; z1:t ) − inf Ir (δ; z1:t ) . z1:t ∈S t

We say that Ir has rate-optimal maximal width if there exist constants 0 < c ≤ C < ∞, t0 ∈ N+ , and δ0 ∈ (0, 1) such that, for all t ≥ t0 and all δ ∈ (0, δ0 ], ( r ) ( r ) log(1/δ) log(1/δ) c min 1, ≤ WIr (δ, t) ≤ C min 1, . t t p This captures the usual fixed-time log(1/δ)/t concentration rate of standard Bernoulli intervals such as Hoeffding, empirical Bernstein, and Clopper–Pearson. Lemma 1. For any fixed-time confidence interval Ir with rate-optimal maximal width containing the empirical average, there exists an error probability δ0 > 0 and a transition probability P (r) ∈ [0, 1] s.t. for every δ ∈ (0, δ0 ] we have Pr [∀t ∈ N+ . P (r) ∈ Ir (δ; Z1:t )] = 0. In particular, Eq. (2) is violated. Gridding. To extend fixed-time guarantees to our setting, one can distribute confidence over time using the union bound. Essentially, we specify a grid of sample counts at which the confidence interval must be valid and distribute confidence across this grid. Formally, a grid N = (ni )i∈N+ is an increasing sequence of sample counts ni ∈P N+ and a confidence spending function h : N+ → (0, ∞) is a ∞ function satisfying i=1 1/h(i) ≤ 1. Together, we get valid sequential inference. Theorem 1. Let δ ∈ (0, 1), r ∈ S, N a grid, h a confidence spending function, and Ir a confidence interval. Then, Pr [∀i ∈ N+ . P (r) ∈ Ir (δ/h(i); Z1:ni )] ≥ 1−δ. More specifically,Tfor any time t we can use the intersection of all previously inferred sets, i.e. i,ni ≤t Ir (δ/h(i); Z1:ni ). Thm. 1 generalizes the approach of [4] for Infer, which distributes confidence over times at which Infer takes place.

10

K. Kueffner et al.

The usefulness of this method depends mainly on the choice of grid and spending function. In Thm. 2 we summarise the asymptotic maximal widths b,c b,c for polynomial and exponential gridding, i.e. Npoly = (⌊b · ic ⌋)i∈N+ and Nexp = i (⌊b · c ⌋)i∈N+ for b, c ≥ 1; and for polynomial and exponential spending, i.e. for step i ∈ N+ set hapoly (i) = ηp · ia and haexp (i) = ηe · ai for a > 1, with spending P normalization ηp = 1/ i i−a = 1/ζ(a) (the Riemann zeta function) P constants P and ηe = 1/ i a−i , s.t. i 1/h(i) = 1. Theorem 2. Let δ ∈ (0, 1), r ∈ S, Ir a confidence interval with rate-optimal maximal width, and a, b, c ∈ R with a > 1 and b, c ≥ 1. Applying polynomial and exponential grids under polynomial and exponential spending impacts the rate-optimal maximal widths (and its constants) as follows: hapoly

haexp

b,1 Npoly

p p (a log(ni /b) + log(ηp /δ))/ni ((ni /b) log a + log(ηe /δ))/ni q p p b,c Npoly ((a/c) log(ni /b) + log(ηp /δ))/ni ( c ni /b log a + log(ηe /δ))/ni q p i /b) b,c Nexp (a log logc (ni /b) + log(ηp /δ))/ni ( log(n log(c) log a + log(ηe /δ))/ni .

We note two disadvantages of the exponential spending (as e.g. used in [4]): Firstly, the interval width is (asymptotically) at least as large as for polynomial spending (Lem. 2). Secondly, while the intervals converge for every grid size under polynomial spending, a constant grid size for exponential spending leads to non-convergence (Cor. 1). Lemma 2. Let δ ∈ (0, 1), r ∈ S, Ir a confidence interval with rate-optimal maximal width, and N a grid. Then, for every a, b ∈ R such that a, b > 1, we get for large i ∈ N+ that WIr (δ/hapoly (i), ni ) ≤ WIr (δ/hbexp (i), ni ). Corollary 1. For every error probability, every confidence interval with rateoptimal maximal width, every grid with constant spacing, and every exponential spending function, the resulting maximal widths fail to converge to 0. In general, Thm. 2 shows that slower spending and sparser grids yield a better asymptotic convergence rate. However, sparse grids in turn increase the gaps between time points where estimates can be refined. This trade-off between asymptotic convergence rate and large gaps arises because the naive union bound treats each grid point as an independent experiment. Fortunately, there are methods leveraging the connection between adjacent points to provide guarantees for every time point. 3.2

Confidence Sequences

A confidence sequence [23] is a stream of probably correct estimates from a stream of samples, as defined in Eq. (2). Notably, a gap-free grid (ni = i) with polynomial spending already gives p a confidence sequence, however with a (sub-optimal) convergence rate of (log t + log(1/δ))/t (Thm. 2), whereas p (log log t + log(1/δ))/t is optimal [37]. Interestingly, this in turn matches the

Confidence Sequences for Online MDP-SMC

11

rate obtained by exponentially spaced grids with polynomial spending, while providing validity at all times. Many confidence sequences with optimal rates are fundamentally connected to martingale theory and Ville’s inequality [36] (with some exceptions [38]). As with confidence intervals, there are worst-case, varianceaware, and parametric confidence sequences, mirroring the fixed-time Hoeffding, (empirical) Bernstein, and Clopper-Pearson constructions. Similar in spirit to Sec. 3.1, stitching [37] first applies a union bound on an exponentially spaced grid and then uses Ville’s inequality to obtain validity at intermediate times. In [64], the authors construct betting confidence sequences from test supermartingales by mirroring the classical Chernoff method for constructing confidence bounds. App. C provides formal definitions of the known Stitched Hoeffding SrSH , Stitched Bernstein SrSB , Betting Hoeffding SrBH , and Betting Bernstein SrBB sequences. Theorem 3. SrSH , SrSB , SrBH , and SrBB are confidence sequences (Eq. (2)). Therefore, we can directly use these to tackle the probability estimation problem. We note that the betting confidence sequences are built from test super martingales, introducing additional slack compared to test martingales. Test martingale-based betting confidence sequences, such as those of [64], typically lack closed forms and are costly to update, scaling linearly with the sample history. Fortunately, our setting admits efficiently computable likelihood-ratio-based test martingales. 3.3

Test Confidence Sequences

A test-based confidence sequence is obtained by inverting a family of sequential hypothesis tests. We use the general approach outlined [56,64] to construct two test-based confidence sequences: One for a single transition probability P(s, a, r), as natural analogue to the Clopper-Pearson interval, and one for the entire distribution P(s, a), avoiding the additional slack introduced by the union bound. Although both test-based confidence sequences lack a closed form, we show that they can be utilised efficiently during value iteration by solving a one dimensional optimisation problem via bisection. Single-transition test confidence sequence. For an intuition, fix a sequential hypothesis test ψr : [0, 1] × S ∗ → {0, 1} that, for a given parameter q ∈ [0, 1], tests the null H0 : P (r) = q against the alternative H1 : P (r) ̸= q with a false positive rate of at most δ ∈ (0, 1). In other words, conditioned on P (r) = q we have Pr[∃t ∈ N+ . ψr (q; Z1:t ) = 1] ≤ δ. Hence, if ψr (q; z1:t ) is 1 at some point in time t, the decision to remove q out of the set of possible parameter for P (r) is the correct decision with probability greater than γ = 1 − δ. This yields a confidence sequence by considering exactly those parameters that have not yet been rejected, i.e. Cr (γ; Z1:t ) = {q ∈ [0, 1] | ψr (q; Z1:t ) = 0}. A natural choice of ψ for a single transition is based on the likelihood ratio [63,64]. Specifically, for the observations z1:t ∈ S t let xi := 1zi =r indicate a transition to r ∈ R, then we define for q ∈ (0, 1) MrMLE (q; z1:t ) :=

µr (z1:i−1 )xi (1 − µr (z1:i−1 ))1−xi , i=1 q xi (1 − q)1−xi

Yt

(3)

12

K. Kueffner et al.

The function MrMLE computes the product of likelihood ratios, where the alternative parameter p at time i is replaced by the predictable empirical average up to time i − 1, i.e. the maximum likelihood estimate before observing the new data at time i. Using the predictable average, as suggested by [64,56], is the crucial difference to the classical Wald Sequential Probability Ratio Test [63], as it ensures that the process MrMLE (P (r); ·) is a test-martingale, i.e. a non-negative martingale with expectation 1. By Ville’s inequality we know that this process never exceeds 1/δ with a probability greater than γ, i.e. Pr[∃t ∈ N+ . MrMLE (P (r); Z1:t ) ≥ 1δ ] ≤ δ. Conversely, if the threshold is exceeded, the assumption that P (r) = q is rejected with probability γ. Hence, MrMLE (q; z1:t ) > 1/δ is an appropriate hypothesis test. Interestingly, this method is not restricted to the predictable empirical average. In fact, any (history-dependent) prediction of P (r) is sufficient: Let νr : S ∗ → D([0, 1]) map observations to a parameter distribution, define for q ∈ (0, 1)  Yt Z 1 uxi (1 − u)1−xi ν (z )(du) . (4) Mrνr (q; z1:t ) := xi 1−xi r 1:i−1 i=1 0 q (1 − q) and Mrνr (0; z1:t ) = 1 if ξr (z1:t ) = 0, Mrνr = 1 if ξr (z1:t ) = t, and Mrνr (q; z1:t ) = +∞ for q ∈ {0, 1} otherwise. Intuitively, Mrνr is the product of likelihood ratios, averaged over alternatives u with respect to a history-dependent distribution representing a best-effort prediction of P (r). An easily computable example of νr is the Beta distribution, i.e. for a0 , b0 ∈ R>0 , at := a0 +ξr (z1:t ), bt := b0 +(t−ξr (z1:t )) MrBeta (q; z1:t ) :=

Yt i=1

Beta(ai−1 + xi , bi−1 + (1 − xi )) 1 · xi . Beta(ai−1 , bi−1 ) q (1 − q)1−xi M νr

Theorem 4. Let δ ∈ (0, 1), r ∈ R, and Mrνr as in Eq. (4). Then Cr r is a valid confidence sequence (satisfying Eq. (2)) and if νr (Z1:t ) converges to P (r) a.s. M νr then Cr r converges to P (r). Computability. Since these test-based confidence sets are not represented as a closed form expression, computability is not obvious. To this end, we exploit the convexity of the log-likelihood ratio in the parameter q. Lemma 3. Let δ ∈ (0, 1), r ∈ R, and Mrνr as in Eq. (4). Then log Mrνr (q, z1:t ) is convex in q ∈ (0, 1) with minimum at µr (z1:t ) when µr (z1:t ) ∈ (0, 1). With this, the confidence sequence {q ∈ [0, 1] | Mrνr (q; z1:t ) ≤ 1/δ} is an interval and its endpoints can be found by bisection. Probability-distribution test confidence sequence. The likelihood-ratio approach can be extended to sequentially valid confidence sets for the full successor distribution P , by replacing the multinomial likelihood ratio instead of binomial one. This method avoids the union bound required to reconstruct the successor distribution and therefore can be statistically more efficient, especially for states with large successor count. In other words, instead of using a hypothesis test for a single probability, we consider a hypothesis test for the entire distribution. As above, we provide a general definition using a (history-dependent) prediction for it. Let ν : S ∗ →

Confidence Sequences for Online MDP-SMC

13

D(D(R)) map state observations to a distribution over successor distributions. For t ∈ N+ , Q in the interior of D(R), U ∈ D(R) and z1:t ∈ S t , define Yt Z U (zi ) M ν (Q; z1:t ) := ν(z1:i−1 )(dU ). (5) i=1 D(R) Q(zi ) and for Q on the boundary of D(R) analogously to Eq. (4). For example, in M MLE (Q; z1:t ), ν maps to the empirical distribution P̂ (z1:t ) := (µr (z1:t ))r∈R . ν

Theorem 5. Let δ ∈ (0, 1) and M ν as in Eq. (5). Then C M is a valid confidence ν sequence, i.e. Pr ∀t ∈ N+ . P ∈ C M (δ; Z1:t ) ≥ 1 − δ and if ν(Z1:t ) converges to ν the successor distribution P a.s. then C M converges to P . Computability. Before, we could explicitly represent the one-dimensional uncertainty set for P (r). This is no longer clear for the |R|-dimensional confidence set ν C M (δ; z1:t ) = {Q ∈ D(R) | M ν (Q; z1:t ) ≤ 1/δ}. However, recall that ultimately we only need to compute bounds on P the Bellman backup, i.e. for a value function V : S → R compute inf Q∈C M ν (δ;z1:t ) r∈R Q(r) · V (r). To solve this optimisation ν problem, we show that C M (δ; z1:t ) is the intersection of the simplex with a convex sublevel set of α(Q; z1:t ). Therefore, the minimiser is the solution of a convex optimisation problem. Moreover, we show that the KKT conditions [14, p. 243] apply and the optimisation problem admits a one-dimensional reduction. Theorem 6. Let t ∈ N+ , δ ∈ (0, 1), z1:t ∈ S t , and V : R → R. Assume ξr (z1:t ) > 0 for all r ∈ R (otherwise restrict to {r | ξr (z1:t ) > 0} and assign all remaining mass to an extremiser of V among {r | ξr (z1:t ) = 0}). If V is ν not constant and C M (δ; z1:t ) ̸= ∅, then ( X P̂ (z1:t ) if M ν (P̂ (z1:t ); z1:t ) = 1/δ ⋆ , Qη ∈ arg min Q(r) · V (r) = ξr (z1:t ) P ξu (z1:t ) otherwise Q∈C M ν (δ;z1:t ) r∈R u∈R η+V (u) η+V (r) / where η > − minr∈R V (r) is the unique solution of M ν (Q⋆η ; z1:t ) = 1/δ and M ν (Q⋆η ; z1:t ) is strictly decreasing in η. Consequently, Q⋆η can be found efficiently using standard bisection. 3.4

Confidence Sequence MDP-SMC

We now summarize our new approach towards online MDP-SMC. Recall that the Sample-Infer-Solve pipeline first distributes confidence over inference steps, and then in each inference step distributes the available confidence over state-action pairs to apply point-wise estimates (such as the Hoeffding bound), i.e. spreading confidence first over time, then over (state) space. Instead, we propose to invert this order by first distributing confidence over all state-action pairs and then constructing confidence sequences for each of them, i.e. spreading confidence first over space and then time. Instead of breaking the process into discrete steps, this allows us to interleave sampling and solving, akin to partial exploration approaches [16,50,51], as we obtain reliable and improving estimates after every sample. In particular, we can refine value estimates after every step.

14

K. Kueffner et al.

Formally, we distribute the entire error budget δtotal over all state-action pairs, obtaining a separate error budget for each individual pair. For example, δtotal using the union bound, we get δ = |{(s,a)|s∈S,a∈A(s)}| . Even though we sample paths through the MDP, by the Markov property we can apply our methods independently in each pair using the per-pair budget and the successor state observations gathered there. Concretely, whenever we visit a state s and choose action a in it, we sample a successor and “advance” the inference process for this specific state-action pair, and use the information in the next Bellman backup of the robust value iteration. See also [67, Chp. 5.4.3] for further details.

4

Implementation and Experimental Evaluation

We present our implementation and evaluation, focusing on two main questions: RQ1 How do the presented inference methods perform on individual distributions, and how does the shape of distributions influence their performance? RQ2 How do our methods perform in online MDP-SMC tasks, i.e. how many samples do we require until we obtain the required precision? We expect correlation between the answers to these two questions, i.e. inference methods which perform well on individual distributions should also do so in MDPSMC, but not necessarily a 1:1 correspondence. Firstly, some inference methods are more suitable for certain shapes of distributions (empirically observed in RQ1 below), and so similarly they are better for MDPs where a particular distributionshape is prevalent. Secondly, the random nature of SMC, further emphasized by our guided sampling approach (explained below), introduces significant variance to the overall process. We deliberately do not emphasize runtime, as gathering samples in real-world scenarios typically is more expensive than their analysis. 4.1

Implementation Details

We implemented all presented methods in a Java tool. For handling MDP, we build on the library of the partial exploration tool (PET) [51] and support models given in PRISM language [44] with reachability properties. Inference methods. We list all implemented inference methods with a short name for referring to them. We consider the Hoeffding (Hoeff), Bernstein (Bern), and Clopper-Pearson (CP) inequalities. From Sec. 3.1, we get “sequentialized” versions using exponential (h2exp ) and squared spending (h2poly ) of confidence (indicated by the suffix -Exp or -Sq, e.g. CP-Sq). To ensure convergence for -Exp (see Cor. 1), we use an exponential grid size (i.e. ni −ni−1 = 2i ); for squared we choose a gap-less grid (ni = i) to compare to confidence sequences. From Sec. 3.2, we use the stitched and betting variants of Hoeffding- and Bernstein-based sequences (Hoeff-Stitch, Hoeff-Bet, Bern-Stitch, and Bern-Bet). From Sec. 3.3, we use the maximum likelihood (MLETest) and Beta hypothesis test methods (BetaTest). For BetaTest, we deliberately used uniform priors (a0 = b0 = 1) to avoid fitting to our dataset. Finally, we have ValueTest using Thm. 6. For validation, we compared results with an independent Python implementation on randomly generated inference tasks, and used parametrized hypothesis

Confidence Sequences for Online MDP-SMC

15

tests on the correctness of each inference method (e.g. statistically testing the hypothesis that the inferred probabilities are correct with probability at least γ). MDP-SMC approaches. We implement our proposed confidence sequence approach as described in Sec. 3.4 as well as the state of the art approach. For the former, for every confidence sequence X, we get an instance CS-X of our approach. For the latter, recall that it is parametrized by (i) how far apart the Infer steps are (i.e. grid size), (ii) how the confidence is spent, and (iii) which point-wise estimate is used. We refer to our implementation of this approach by SOTA-X-Y, where X describes grid and spending and Y the applied (point-wise) inference method. For X, we use exponential (Exp), i.e. δ · h2exp (i) = 2δi confidence and 100 · 2i sampled paths in iteration i, and squared (Sq), i.e. δ · h2poly (i) = δ · i26π2 confidence and 100 · i2 sampled paths in iteration i. Both variants additionally rely on a sampling strategy, i.e. which actions to choose while sampling a path. We employ guided sampling as in [16]: We choose actions which currently achieve the highest value in the corresponding state until a goal or sink state is reached. For updating value estimates, we employ robust value iteration [52], continuing until a value estimate is ε-precise. We pre-process MDPs by collapsing end components, as suggested in [53]. Finally, we consider CAV19 [4], the only other sound approach we know of. From a statistical perspective, it is similar to SOTA-Exp-Hoeff, however with technical differences, such as the grid spacing (105 · 2i instead of 100 · 2i ) and sampling strategy. As the original code contained a bug (not properly distributing confidence), we reimplemented the method, mimicking the implementation as closely as possible. The changes were bug fixes and adding the improvements of [53] to ensure a fair comparison of the statistical methods. 4.2

RQ1: Performance of Individual Inference

In this section, we investigate our first research question, i.e. how the different sequential inference methods perform on various distributions. Setup. We consider several classes of distributions, parametrized by the number of successors and their “shape”. Fig. 1 shows results for (nearly) uniform distributions with 2 and 50 successors; further data can be found in App. E.1. For each class, we generate 20 random distributions and 40 random value vectors. Then, for each distribution, we generate 100 000 samples, feed these to the inference methods with an overall confidence of γ = 0.9, and compute the difference between the smallest and largest value estimate each inference method can provide for each of the given vectors at several time steps. For each method, we then report the average of this error. Note that we cannot give an error estimate on probabilities directly, since, for example, the ValueTest approach does not estimate probabilities. To establish a lower bound, we also compare with the pointwise Clopper-Pearson estimate (PointCP), i.e. what we could infer if we used all given confidence at a single point in time instead of spreading it over infinite time. Results. Fig. 1 summarizes our results, omitting some inference methods for readability. We see that the number of successors (and shape, as visible in App. E.1) of

16

K. Kueffner et al.

0.05

Hoeff-Exp CP-Exp Bern-Sq CP-Sq Hoeff-Stitch Bern-Stitch Bern-Bet BetaTest ValueTest PointCP

0.5

0.01 0.1

104 2 successors

105

104 50 successors

105

Fig. 1: Comparison of our presented methods on (nearly) uniform distributions with 2 and 50 successors, respectively. We show how the inference error (averaged over 40 random value vectors, y-axis) decreases with increasing number of samples (x-axis). Observe that both axes are logarithmic. We only consider a selection of methods for readability, further data can be found in App. E.1 Table 1: Comparison scores of all our methods (lower is better), sorted from best to worst. The scores describe how much more samples (relatively) a method needs on average compared to the best method. For example, a score of 10 means a method required 10 times more samples than the best on average. CAV19 SOTA-Exp-Bern SOTA-Exp-Hoeff SOTA-Exp-CP CS-Hoeff-Bet SOTA-Sq-Bern

SOTA-Sq-Hoeff

SOTA-Sq-CP

CS-Bern-Sq

CS-Bern-Exp

CS-Hoeff-Sq

CS-Hoeff-Exp

CS-Hoeff-Stitch

CS-CP-Exp

CS-Bern-Stitch CS-CP-Sq CS-Bern-Bet

CS-MLETest

CS-BetaTest

CS-ValueTest

Method

Score 1.3 1.5 1.5 1.6 1.8 2 2.1 2.2 2.7 3.3 4.1 5.0 5.9 6.8 8.6 11 19 22 23 50

the distribution has a profound impact on the rate of convergence. Moreover, confidence sequences, in particular Bern-Stitch and ValueTest, perform favourably. Notably, our novel ValueTest is always among the best and sometimes even more precise than PointCP, as it does not need to infer individual probabilities but directly infers a single value. In other words, we lose surprisingly little precision for gaining guarantees across arbitrarily many samples instead of just a single point in time. 4.3

RQ2: Performance of Online MDP-SMC

In this section, we investigate our second research question, i.e. the impact of using our inference methods in the context of online MDP-SMC. Setup. We evaluate all methods on several MDP benchmarks, using our implementation of [4] as baseline. We consider MDPs from the PRISM benchmark suite [45] and the (revised) practitioner’s guide’s community set [30,31] with a

Confidence Sequences for Online MDP-SMC

17

non-trivial reachability query (including all models in [53] and more). For models with multiple parametrizations or multiple non-trivial queries, we (arbitrarily) selected one of them to avoid over-representing one particular model’s structure. All in all, we obtain 320 model-method combinations. As metric, we focus on the total number of samples. To smooth randomness, we repeat each experiment ten times and report the average. We focus on moderately sized models to allow for a reasonably quick reproduction, and set a timeout of 120s per run. Results. We summarize our findings in Tab. 1. For brevity, we present an average score of each method, obtained as follows. For each model, we compute the relative difference between the method and the best one and then take the (geometric) average of this ratio over all models. For example, a score of 4 intuitively means that, on average, this method required four times more samples than the respective best method. Timeouts are counted as twice the worst method’s performance. We treat all sample counts below 100 as equally good, to reduce the impact of minor fluctuations. Individual results are provided in App. E.2. Our new methods clearly outperform both (our improved implementation of) the previous approach of [4] and all other state-of-the-art variants. We conjecture that this is due to confidence sequences being able to consistently give meaningful information to the interwoven solving and guidance, allowing the approach to focus on regions of interest more effectively. Of our methods, the hypothesis test methods are the clear winners. Notably, if we exclude the one model where ValueTest times out, it achieves a near-perfect score of 1.1. Moreover, the dedicated confidence sequences (mostly) outperform the “sequentialized” approaches. The only exception are the sequentialized Clopper-Pearson methods, which beat some of the confidence sequences. We conjecture that this is due to Clopper-Pearson being specifically tailored towards binomial distributions. For runtime, we found that as soon as gathering samples becomes non-trivial, their cost vastly dominates any computational effort required for the statistical estimates. Already in our unoptimized implementation, each method is able to handle thousands of updates per second. Overall Verdict. In summary, in most cases our novel ValueTest is the best choice, as typically gathering samples is much more expensive than a slight increase in runtime. Given appropriate domain knowledge, methods using priors (such as BetaTest) may perform even better. Finally, in cases where gathering samples is extremely cheap and overall runtime is of importance, easily computable approaches such as Bern-Bet may be the best choice.

5

Conclusion

We have presented confidence sequences for online MDP-SMC, improving upon the previous, mostly flawed and/or inefficient state of the art. These sequences obtain statistical estimates that improve with every arriving sample while maintaining global guarantees. Thus, they are an ideal match for online inference tasks, where gathering samples and extracting knowledge from them is interwoven. The efficiency of these methods is underlined by our experimental evaluation.

18

K. Kueffner et al.

For future work, we are interested in further improving on the performance and numerical stability of the ValueTest. Additionally, we want to investigate using “pre-sampling”, i.e. gathering some samples without directly using them for inference, to influence some parameters such as confidence distribution, the prior of the BetaTest, or identifying which inference method could be most suitable. Finally, we want to extend those techniques to a dynamic setting, where transition probabilities are subject to change [34]. Data availability: Our implementation, all benchmarks, and scripts to reproduce our results are included in our artifact, which will be publicly available.

Confidence Sequences for Online MDP-SMC

19

References 1. Agarwal, A., Kakade, S.M., Yang, L.F.: Model-based reinforcement learning with a generative model is minimax optimal. In: COLT. Proceedings of Machine Learning Research, vol. 125, pp. 67–83. PMLR (2020) 2. Agarwal, C., Guha, S., Křetínskỳ, J., Muruganandham, P.: PAC statistical model checking of mean payoff in discrete-and continuous-time MDP. In: CAV. pp. 3–25. Springer (2022) 3. Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI. pp. 2669–2678. AAAI Press (2018) 4. Ashok, P., Kretínský, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. In: CAV, Part I. LNCS, vol. 11561, pp. 497–519. Springer (2019) 5. Bacci, G., Ingólfsdóttir, A., Larsen, K.G., Reynouard, R.: An mm algorithm to estimate parameters in continuous-time markov chains. In: International Conference on Quantitative Evaluation of Systems. pp. 82–100. Springer (2023) 6. Badings, T.S., Romao, L., Abate, A., Jansen, N.: Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty. In: AAAI. pp. 14701–14710. AAAI Press (2023) 7. Badings, T.S., Romao, L., Abate, A., Parker, D., Poonawala, H.A., Stoelinga, M., Jansen, N.: Robust control for dynamical systems with non-gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341–391 (2023) 8. Badings, T.S., Simão, T.D., Suilen, M., Jansen, N.: Decision-making under uncertainty: beyond probabilities. Int. J. Softw. Tools Technol. Transf. 25(3), 375–391 (2023) 9. Baier, C., Dubslaff, C., Wienhöft, P., Kiebel, S.J.: Strategy synthesis in Markov decision processes under limited sampling access. In: NFM, Lecture Notes in Computer Science, vol. 13903, pp. 86–103. Springer (2023) 10. Baier, C., Dubslaff, C., Wienhöft, P., Kiebel, S.J.: Strategy synthesis in markov decision processes under limited sampling access. In: NASA Formal Methods Symposium. pp. 86–103. Springer (2023) 11. Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008), https: //mitpress.mit.edu/books/principles-model-checking 12. Bazille, H., Genest, B., Jégourel, C., Sun, J.: Global PAC bounds for learning discrete time Markov chains. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 304–326. Springer (2020). https://doi.org/10.1007/978-3-030-53291-8_17 13. Billingsley, P.: Probability and measure. John Wiley & Sons (2017) 14. Boyd, S., Vandenberghe, L.: Convex optimization. Cambridge university press (2004) 15. Brafman, R.I., Tennenholtz, M.: A near-optimal polynomial time algorithm for learning in certain classes of stochastic games. Artificial Intelligence 121(1-2), 31–47 (2000) 16. Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretínský, J., Kwiatkowska, M., Meggendorfer, T., Parker, D., Ujma, M.: Learning algorithms for verification of markov decision processes. TheoretiCS 4 (2025) 17. Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Křetínský, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA. pp. 98–114. Springer (2014). https://doi.org/10.1007/ 978-3-319-11936-6_8 18. Brown, L.D., Cai, T.T., DasGupta, A.: Interval Estimation for a Binomial Proportion. Statistical Science 16(2), 101 – 133 (2001). https://doi.org/10.1214/ss/ 1009213286

20

K. Kueffner et al.

19. Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienhöft, P.: Sound statistical model checking for probabilities and expected rewards. In: TACAS (to appear, preprint available at https://arxiv.org/pdf/2411.00559). Lecture Notes in Computer Science, Springer (2025) 20. Chatterjee, K., Henzinger, T.A.: Value iteration. In: 25 Years of Model Checking. Lecture Notes in Computer Science, vol. 5000, pp. 107–138. Springer (2008). https://doi.org/10.1007/978-3-540-69850-0_7, https://doi.org/10. 1007/978-3-540-69850-0_7 21. Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404–413 (1934) 22. Daca, P., Henzinger, T.A., Křetínskỳ, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 112–129. Springer (2016) 23. Darling, D.A., Robbins, H.: Confidence sequences for mean, variance, and median. Proceedings of the National Academy of Sciences 58(1), 66–68 (1967) 24. El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: International Symposium on Automated Technology for Verification and Analysis. pp. 120–134. Springer (2009) 25. Frey, J.: Fixed-width sequential confidence intervals for a proportion. The American Statistician 64(3), 242–249 (2010). https://doi.org/10.1198/tast.2010.09140 26. Fu, J., Topcu, U.: Probably approximately correct MDP learning and control with temporal logic constraints. In: Robotics: Science and Systems (2014). https: //doi.org/10.15607/RSS.2014.X.039 27. Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artificial Intelligence 122(1-2), 71–109 (2000) 28. Grimmett, G., Stirzaker, D.: Probability and random processes. Oxford university press (2020) 29. Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111–131 (2018). https://doi.org/10.1016/j.tcs.2016. 12.003 30. Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: TACAS (1). LNCS, vol. 13993, pp. 469–488. Springer (2023). https://doi.org/10.1007/978-3-031-30823-9_24 31. Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: The revised practitioner’s guide to MDP model checking algorithms. STTT (to appear), Preprint: https://sjunges.github.io/files/revised_practitioners_guide.pdf (2026) 32. HasanzadeZonuzy, A., Bura, A., Kalathil, D.M., Shakkottai, S.: Learning with safety constraints: Sample complexity of reinforcement learning for constrained MDPs. In: AAAI. pp. 7667–7674. AAAI Press (2021) 33. He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H.: A bounded statistical approach for model checking of unbounded until properties. In: ASE. pp. 225–234. ACM (2010) 34. Henzinger, T.A., Kueffner, K., Singh, V., Sun, I.: Alignment monitoring. In: International Conference on Runtime Verification. pp. 140–159. Springer (2025) 35. Hoeffding, W.: Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association 58(301), 13–30 (1963) 36. Howard, S.R., Ramdas, A., McAuliffe, J., Sekhon, J.: Time-uniform chernoff bounds via nonnegative supermartingales. Probability Surveys 17, 257–317 (2020) 37. Howard, S.R., Ramdas, A., McAuliffe, J., Sekhon, J.: Time-uniform, nonparametric, nonasymptotic confidence sequences. The Annals of Statistics 49(2), 1055–1080 (2021)

Confidence Sequences for Online MDP-SMC

21

38. Jamieson, K., Malloy, M., Nowak, R., Bubeck, S.: lil’ucb: An optimal exploration algorithm for multi-armed bandits. In: Conference on Learning Theory. pp. 423–439. PMLR (2014) 39. Jin, C., Krishnamurthy, A., Simchowitz, M., Yu, T.: Reward-free exploration for reinforcement learning. In: ICML. Proceedings of Machine Learning Research, vol. 119, pp. 4870–4879. PMLR (2020) 40. Khintchine, A.: über einen satz der wahrscheinlichkeitsrechnung. Fundamenta Mathematicae 6(1), 9–20 (1924) 41. Kretínský, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: LICS. pp. 1–14. IEEE (2023). https://doi.org/10.1109/LICS56636.2023.10175771, https://doi.org/ 10.1109/LICS56636.2023.10175771 42. Kretínský, J., Michel, F., Michel, L., Pérez, G.A.: Finite-memory near-optimal learning for Markov decision processes with long-run average reward. In: UAI. Proceedings of Machine Learning Research, vol. 124, pp. 1149–1158. AUAI Press (2020) 43. Křetínský, J., Pérez, G.A., Raskin, J.F.: Learning-based mean-payoff optimization in an unknown MDP under omega-regular constraints. In: CONCUR. pp. 8:1–8:18. Dagstuhl (2018) 44. Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: Verification of probabilistic real-time systems. In: International conference on computer aided verification. pp. 585–591. Springer (2011) 45. Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST. pp. 203–204. IEEE Computer Society (2012). https://doi.org/10.1109/ QEST.2012.14 46. Lange, S., Gabel, T., Riedmiller, M.A.: Batch reinforcement learning. In: Reinforcement Learning, Adaptation, Learning, and Optimization, vol. 12, pp. 45–73. Springer (2012) 47. Lattimore, T., Szepesvári, C.: Bandit algorithms. Cambridge University Press (2020) 48. Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. pp. 541–548. AAAI Press (1999) 49. Maurer, A., Pontil, M.: Empirical bernstein bounds and sample-variance penalization. In: COLT (2009), http://www.cs.mcgill.ca/%7Ecolt2009/papers/012. pdf#page=1 50. Meggendorfer, T.: PET - A partial exploration tool for probabilistic verification. In: ATVA. Lecture Notes in Computer Science, vol. 13505, pp. 320–326. Springer (2022) 51. Meggendorfer, T., Weininger, M.: Playing games with your PET: extending the partial exploration tool to stochastic games. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 359–372. Springer (2024) 52. Meggendorfer, T., Weininger, M., Wienhöft, P.: Solving robust markov decision processes: Generic, reliable, efficient. In: AAAI. pp. 26631–26641. AAAI Press (2025). https://doi.org/10.1609/AAAI.V39I25.34865, https://doi.org/ 10.1609/aaai.v39i25.34865 53. Meggendorfer, T., Weininger, M., Wienhöft, P.: What are the odds? improving statistical model checking of markov decision processes. In: QEST+FORMATS. Lecture Notes in Computer Science, vol. 16143, pp. 195–218. Springer (2025). https://doi.org/10.1007/978-3-032-05792-1_11, https://doi.org/10.1007/ 978-3-032-05792-1_11

22

K. Kueffner et al.

54. Perez, M., Somenzi, F., Trivedi, A.: A PAC learning algorithm for LTL and omegaregular objectives in mdps. In: AAAI. pp. 21510–21517. AAAI Press (2024). https: //doi.org/10.1609/AAAI.V38I19.30148 55. Puterman, M.L.: Markov decision processes: Discrete stochastic dynamic programming. John Wiley and Sons (1994) 56. Ramdas, A., Wang, R.: Hypothesis testing with e-values. Foundations and Trends® in Statistics 1(1-2), 1–390 (2025) 57. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: International Conference on Computer Aided Verification. pp. 202–215. Springer (2004) 58. Shi, L., Li, G., Wei, Y., Chen, Y., Chi, Y.: Pessimistic q-learning for offline reinforcement learning: Towards optimal sample complexity. In: ICML. Proceedings of Machine Learning Research, vol. 162, pp. 19967–20025. PMLR (2022) 59. Suilen, M., Simão, T.D., Parker, D., Jansen, N.: Robust anytime learning of Markov decision processes. In: NeurIPS (2022) 60. Tsybakov, A.B.: Introduction to Nonparametric Estimation. Springer Series in Statistics, Springer, New York, NY (2009). https://doi.org/10.1007/b13794 61. Wagenmaker, A.J., Simchowitz, M., Jamieson, K.: Beyond no regret: Instancedependent PAC reinforcement learning. In: COLT. Proceedings of Machine Learning Research, vol. 178, pp. 358–418. PMLR (2022) 62. Wainwright, M.J.: High-dimensional statistics: A non-asymptotic viewpoint, vol. 48. Cambridge university press (2019) 63. Wald, A.: Sequential tests of statistical hypotheses. In: Breakthroughs in statistics: Foundations and basic theory, pp. 256–298. Springer (1992) 64. Waudby-Smith, I., Ramdas, A.: Estimating means of bounded random variables by betting. Journal of the Royal Statistical Society Series B: Statistical Methodology 86(1), 1–27 (2024) 65. Weininger, M., Grover, K., Misra, S., Kretínský, J.: Guaranteed trade-offs in dynamic information flow tracking games. In: CDC. pp. 3786–3793. IEEE (2021). https://doi.org/10.1109/CDC45484.2021.9683447 66. Wen, M., Topcu, U.: Probably approximately correct learning in adversarial environments with temporal logic specifications. IEEE Trans. Autom. Control. 67(10), 5055–5070 (2022) 67. Wienhöft, P.: Statistical model checking with robust markov decision processes (2025), https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-1000969 68. Wienhöft, P., Suilen, M., Simão, T.D., Dubslaff, C., Baier, C., Jansen, N.: More for less: Safe policy improvement with stronger performance guarantees. In: 32nd International Joint Conference on Artificial Intelligence, IJCAI 2023. pp. 4406–4415. International Joint Conferences on Artificial Intelligence (IJCAI) (2023) 69. Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: SBMF. Lecture Notes in Computer Science, vol. 6527, pp. 144–160. Springer (2010) 70. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV. pp. 223–235. Springer (2002)

Confidence Sequences for Online MDP-SMC

A

23

Assumptions on Sampling Access and Knowledge

In this appendix, we describe the different settings for the MDP-SMC problem that have appeared in the literature. The focus is on how exactly we can access an unknown MDP. There are two independent choices to make: firstly, how we can sample transitions from the MDP (related to Sample) and secondly what kind of knowledge we have about the transition function (related to Infer). For both choices, we first classify settings appearing in the literature, ordering them from strongest to weakest assumption, and then discuss them. A.1

Obtaining Samples of Transitions

– Every state, e.g. [70,26,1]: In this setting, we can start a simulation in every state. This is equivalent to freely choosing a state-action pair to sample in every step. – Simulations, e.g. [57,17,4,12,2,59]: In this setting, we can only start a simulation in the initial state. It then continues by choosing an available action, sampling a successor state and then repeating the choosing and sampling from this state. Thus, it is harder to get samples of regions that are only visited with small probability, but the setting is arguably more realistic. – Batch learning, e.g. [46,58,68,53]: In this setting, we have no control over which states are sampled but only get a fixed data set of past interactions. Note that in the first two settings, we can use guidance heuristics to improve the practical performance. In the batch learning setting, PAC guarantees require that we can get further batches, and that the unknown policy performing the sampling is fair, so that every transition is sampled infinitely often. Even if we know nothing about the origins of the batch data set, we can get a probabilistic guarantee that the bounds computed by Solve are correct; however, they may be far apart, i.e. not give us the precision we aim for. Finally, we mention that in addition to having the samples, we require knowledge of the initial state ŝ and the set of available actions A(s) for every state s that has been sampled. For the latter, observe that a single unseen action can completely change the value of the MDP, which would make even PAC-guarantees impossible. A.2

Knowledge of the Transition Function

– White box, e.g. [55]: In this fully-informed setting, we know the whole tuple M = (S, A, P). Our whole goal in this work is to avoid assuming this precise knowledge, in particular knowledge of the exact transition probabilities P. – Grey box, e.g. [33,69,4,12,2,59,10,6]: In this setting, we do not know the exact transition probabilities P(s, a, r) for any state-action-successor triple. However, we know the topology of the underlying graph, i.e. for every stateaction pair (s, a), we know its successors {r | P(s, a, r) > 0}. We discuss variants of this setting below. – Black box, e.g. [16,22,4,2]: In this setting, we know neither the exact transition probabilities nor the topology of the underlying graph. However, we have a lower bound on the smallest transition probability occurring in the MDP pmin ≤ min({P(s, a, r) | s, r ∈ S, a ∈ A(s)}).

24

K. Kueffner et al.

– No-knowledge: In this setting, we know nothing about the transition function. For completeness, we mention other assumptions appearing in the literature: We can restrict attention to systems that are ergodic under any pair of strategies [15,24], essentially requiring that we are in a single strongly connected component; or we can assume knowledge of the mixing time of the MDP [26], which however is as hard to compute as the value. Thus, we consider both of these assumptions not fitting for our framework. Alternative grey box formulations. There exist three variants of the greybox setting in the literature. The first version [33,69,26] requires immediate knowledge of the full graph. Equivalently [12,59,10,6], we can assume that we have an oracle that for every state gives us the available actions and for every state-action pair (s, a) returns the set of its successors {r | P(s, a, r) > 0}. By exploring the whole graph, we arrive in the same situation as knowing the whole topology. A weaker variant of the grey box setting is used in [4,2]. Instead of knowing the the exact set of successors for every state-action pair, we only assume to know the number of successors, formally |{r | P(s, a, r) > 0}|. This allows us to know that all successors have been sampled as soon as the number of sampled successors is equal the known number of successors. The assumption is only eventually equivalent to knowing the full topology because we need to wait until we have samples seen every successor. In particular, we can be unlucky and not sample some successor arbitrarily long, albeit with probability 0. As long as we have not seen all successors of a state-action pair, applying qualitative graph algorithms (e.g. to detect that a state has no path to the target) is not possible. Thus the qualitative graph algorithms can be applied immediately for the stronger setting, but only after sampling every transition at least once in the weaker one. Finally, we mention that [59] requires a combination of both black box and grey box, because in addition to the topology it knows for each transition a lower bound strictly greater than 0. Reducing Black Box to Grey Box. Given that we know pmin , we can reduce black box to grey box with enough samples, since then we can be sufficiently certain that we have not overlooked a transition, see [53, Remark 2]. Intuitively, the idea is to commit, for example, half the confidence towards inferring the topology. Assuming we have some confidence dedicated to a state-action pair (s, a), we can estimate lower bounds on the transition probabilities p(r) for each seen successor r by using e.g. our presented confidence sequence on probabilities. Once the P inferred lower bounds are large enough, i.e. r p ≥ 1 − pmin , we know that we have seen all successors of this state-action pair with high confidence. After this happened for every state-action pair we encountered, we can conclude that we have “seen” the entire system, can apply graph-based analysis, and switch to the grey box approach, using the remaining “unspent” confidence. Note that since in some cases we might not know the number of states in advance, we would need to apply a similar “confidence spending” approach (e.g. dedicate δ/2 error budget to the first 1000 states, δ/4 to the next 1000, and so on). While this process may seem excessive, observe that we need to perform graph-based

Confidence Sequences for Online MDP-SMC

25

analysis to even identify sink states, i.e. those states which can never reach the goal. In particular, knowing neither the graph nor pmin , we cannot provide PAC guarantees: Intuitively, just missing a single transition (with arbitrarily small probability) can change the value from 0 to 1, and without any further information we cannot prove that we have seen “everything” just from finitely many finite samples. Discussion. The black box assumption is a relatively light assumption in many realistic scenarios. For instance, “bounds on the rates for reaction kinetics in chemical reaction systems are typically known; for models in the PRISM language [44], the bounds can be easily inferred without constructing the respective state-space” [22, p. 2-3]. We believe that the grey box setting has slightly stronger assumptions than the black box setting, as grey box has topological information about every state, while black box only has a global lower bound. However, one can also argue that the grey box setting is more realistic because of “systems for which probabilities are governed by uncertain forces (e.g. error rates): in this case, it is not easy to have a lower bound on the minimal transition probability, but we can assume that the set of transitions is known” [12, p. 20]. Observability. One assumption that is common to all approaches mentioned above is observability, i.e. that at any time we can exactly see which state the system is in. In some cases, the system as a whole is a black box and may even just present us with currently available actions and feedback on the state of the objective (e.g. has the goal been reached or not). Here, none of the mentioned approaches (including ours) is applicable. In general, partially observable MDPs are undecidable with infinite-horizon objectives, even when the underlying structure is known [48].

B

Reusing Confidence is Incorrect

As mentioned, most approaches following the Sample-Infer-Solve framework, e.g. [65,2,59,9,7,54], are not designed with a fixed number of samples in mind, but rather sample continuously until the property of interest can be estimated with the given precision ε. They also re-use the entire confidence in each Infer, intuitively assuming that since we terminate only once the precision is achieved, the correctness of all previous Infers is irrelevant, i.e. that Pr[error | termination] = Pr[error], which is not the case in general. Concretely, the (flawed) correctness proofs for these sequential procedures usually relies on the soundness of the statistical method used in each SampleInfer cycle. While sound inference methods such as Clopper-Pearson or Hoeffding indeed ensure that each single Infer step is correct with at least the nominal probability γ, this is not sufficient to show correctness of the sequential algorithm since the termination condition might be biased. As given by Lem. 1, there are stopping times for which the failure condition will happen with probability ≥ δ. A more detailed analysis, weighting the precise probability of a failure for a given stopping time with the probability of observing each stopping time, reveals that the sequential algorithm using Clopper-Pearson is unsound for certain parameters [25]. Note that this can be cast as simple

26

K. Kueffner et al. s1

a

p

s2

1−p

b, 1

s−

s+

Fig. 2: Example MDP to show the problem with re-using confidence budget. MDP, thus already showing that the underlying logic of re-using confidence for multiple Infer steps for a generic fixed-time confidence interval is incorrect. We emphasize that therefore this existing work already provides a counterexample to the correctness proofs, as Clopper-Pearson is a correct fixed-time confidence interval, and the correctness proofs of the cited works only rely on this fact. In practice, we could not find a case where the concrete implementations using the Hoeffding / Okamoto bound fail reliably, as this bound is extremely conservative. (Note that even if these methods would turn out to be sound, they are far less sample-efficient, as they rely on such a conservative bound.) We however provide a generic example that shows that fixed time confidence intervals are ill suited for the statistical model checking problem posed in Sec. 2.2. Example 2. Consider the MDP on S = {s1 , s2 , s+ , s− } with initial state s1 , target state s+ , sink state s− , and transitions P(s1 , a, s2 ) = p, P(s1 , a, s− ) = 1 − p, and P(s2 , b, s+ ) = 1, where p ∈ (0, 1) (see Fig. 2). Then Pr[♢s+ ] = p♢ = p. The SMC algorithm estimates p♢ by combining Hoeffding confidence intervals for P(s1 , a, s2 ) and P(s2 , b, s+ ) via interval arithmetic and a union bound. For i ∈ {1, 2}, let Itii = [Liti , Utii ] be a confidence interval for pi with error probability δ/2. Assume the sampling strategy keeps t1 so small that It11 = [0, 1], while t2 → ∞. Then, the resulting interval for p♢ is It♢1 ,t2 := It11 · It22 = [0, Ut12 ]. If ε = p, then the stopping time τ := inf{t2 ∈ N+ | |It♢1 ,t2 | < ε} coincides with τ = inf{t1 ∈ N+ | Ut11 < p}. By the law of the iterated logarithm [28, p. 377], this event occurs almost surely, implying that the claimed guarantee fails, i.e. Pr[p♢ ∈ It♢1 ,τ ] = Pr[p2 ≤ Uτ2 ] = 0 ̸= 1 − δ. Note that grey box algorithms could infer that P(s2 , b, s+ ) = 1 by graph analysis alone. By, for example, changing from 1 to 1 − β with β ≪ ε we can prevent this, too, however at the cost of simplicity of the example.

C

Additional Definitions

Here, we provide formal definitions of existing confidence intervals and sequences in our notation. In the following, and predictive Pt define the the empirical → − 1 2 empirical variance as σr (z1:t ) := t−1 ( 1 − µ (z )) and σ r (z1:t ) := r 1:t i=1 zi =r P t 1 2 i=1 (1zi =r − µr (z1:i−1 )) , respectively. For t = 0 we define z1:t as the empty t − sequence ϵ, set µr (ϵ) = 1/2, → σ r (ϵ) = 1/4, and set σr (z1:t ) = 1/4 for t ∈ {0, 1}. C.1

Rate Optimality

Bernoulli Confidence Intervals. We define I as the set of all confidence intervals for the Bernoulli mean. Each confidence interval I ∈ I satisfies for each error

Confidence Sequences for Online MDP-SMC

27

inf Pr [p ∈ I(δ; X1:t )] ≥ 1 − δ.

(6)

probability δ ∈ (0, 1) that ∀t ∈ N+ :

p∈[0,1] p

Empirically Anchored. The confidence interval I ∈ I is empirically anchored, if it always contains the empirical average. Formally, I is empirically anchored if for all t ∈ N+ , all δ ∈ (0, 1), and all x1:t ∈ {0, 1}t , t

1X xi ∈ I(δ; x1:t ). t i=1 Interval Width. The width of the confidence interval I ∈ I for a given sequence of samples x1:t ∈ {0, 1}t and error probability δ ∈ (0, 1) is |I(δ; x1:t )| := sup I(δ; x1:t ) − inf I(δ; x1:t ).

(7)

The maximal width after t ∈ N+ of the confidence interval I ∈ I is WI (δ, t) :=

sup

|I(δ; x1:t )|.

(8)

x1:t ∈{0,1}t

Intuitively, this is the worst case width that may occur on a sequence of Bernoulli random variables. The optimal maximal width among I is given by W ⋆ (δ, t) := inf WI ′ (δ, t). ′ I ∈I

(9)

Lemma 4. The optimal maximal width benchmark for Bernoulli confidence intervals is of order ( r )! log(1/δ) ⋆ W (δ, t) = Θ min 1, . (10) t

Since we are interested in the shrinking-width regime, we formulate rate optimality asymptotically, i.e. for sufficiently large sample sizes and sufficiently small error probabilities [36,64]. Related to the discussion of minimax optimal width, where optimality is defined w.r.t. to the confidence intervals expected behaviour [18,60], we define optimality w.r.t. the worst case behaviour. This allows us to address the common fixed time confidence intervals uniformly. Definition 1. A confidence interval I ∈ I has asymptotically rate-optimal maximal width, if there exist constants 0 < c0 ≤ C0 < ∞, t0 ∈ N+ , and δ0 ∈ (0, 1) such that for all t ≥ t0 and all δ ∈ (0, δ0 ] we have ( r ) ( r ) log(1/δ) log(1/δ) ≤ WI (δ, t) ≤ C0 · min 1, . (11) c0 · min 1, t t

28

K. Kueffner et al.

C.2

Confidence Intervals

We provide definitions of the classical Hoeffding [35], (empirical) Bernstein [49], and Clopper-Pearson intervals [21]: h i p IrH (δ; z1:t ) = µr (z1:t ) ± log(2/δ)/(2t) ∩ [0, 1], h i p IrB (δ; z1:t ) = µr (z1:t ) ± 2σr (z1:t ) log(3/δ)/t + 7 log(3/δ)/(3(t − 1)) ∩ [0, 1], h i IrC (δ; z1:t ) = Beta−1 (δ/2; kt , t − kt + 1), Beta−1 (1 − δ/2; kt + 1, t − kt ) , where kt = ξr (z1:t ) and Beta−1 the inverse of the Beta distribution. Whenever an interval is undefined, e.g., IrB for t < 2 and IrC for kt = 0 or kt = t, they are set to the trivial interval [0, 1]. All three p intervals are empirically anchored and their maximal widths are of order Θ( log(1/δ)/t) (see also Lemms. 5 and 6). C.3

Stitching Sequences

1,c Fix c > 1 as the parameter of an exponential grid Nexp , an initial time t0 ∈ N+ , √ 1/4 −1/4 and )/ 2, k2 = √ let h be a confidence-spending function. Define k1 = (c + c ( c + 1)/2, m(v) := ⌈log(v/t0 )/ log(c)⌉, and g(δ; v) := log h (m(v)) + log (2/δ). Then, for every t ∈ N+ , δ ∈ (0, 1), r ∈ R, and z1:t ∈ Rt , the Stitched Hoeffding confidence sequence [37] is q SrSH (δ; z1:t ) = µr (z1:t ) ± 1t k12 g(δ; t) ∩ [0, 1],

and the Stitched Bernstein confidence sequence [37] is q  k12 vt g(δ; vt ) + k22 g(δ; vt )2 + k2 g(δ; vt ) ∩ [0, 1], SrSB (δ; z1:t ) = µr (z1:t ) ± 1t − where vt = max(1, t · → σ r (z1:t )) C.4

Betting Sequences

For t ∈ N+ , δ ∈ (0, 1), r ∈ R, and z1:t ∈ Rt , define the Betting Hoeffding confidence sequence [64] Pt Pt log(2/δ) + i=1 λ2i /8 BH i=1 λi 1zi =r Sr (δ; z1:t ) = ± , Pt Pt i=1 λi i=1 λi p where λi = min(1, ηi ) and ηi = (8 log(2/δ))/(i log(i + 1)). Moreover, the Betting Bernstein confidence sequence [64] is defined as Pt Pt log(2/δ) + i=1 vi (− log(1 − λi ) − λi ) BB i=1 λi 1zi =r Sr (δ; z1:t ) = ± ∩ [0, 1], Pt Pt i=1 λi i=1 λi s ! 1 2 log(2/δ) 2 where vi = (1zi =r − µr (z1:i−1 )) , and λi = min , → . − 2 σ r (z1:i−1 )i log(i + 1)

Confidence Sequences for Online MDP-SMC

D

29

Proofs

Throughout this section, fix a state-action pair s ∈ S, a ∈ A(s) and a successor state r ∈ R. Let P = P(s, a), Z = (Zt )t∈N+ with Zt ∼ P i.i.d., and define Xt := 1Zt =r ∈ {0, 1},

p := P (r) ∈ [0, 1].

Write Ft := σ(Z1:t ) = σ(X1:t ). Lemma 4. The optimal maximal width benchmark for Bernoulli confidence intervals is of order ( r )! log(1/δ) ⋆ . (10) W (δ, t) = Θ min 1, t Proof. We first prove the upper bound. Because the Hoeffding interval is dataagnostic the claim follows immediatly, i.e., for δ < 1/2 ( r ) ( r ) 2 log(2/δ) 2 log(1/δ) ≤ C min 1, . W ⋆ (δ, t) ≤ WI H (δ, t) ≤ min 1, t t for some constant C > 0 because W ⋆ is the infimum over all Bernoulli confidence intervals. We now prove the lower bound. Fix an arbitrary Bernoulli confidence interval I ∈ I and abbreviate w := WI (δ, t). If w > 1/4, then trivially ( r ) 1 log(1/δ) min 1, ≤ w. 4 t It therefore remains to consider the case w ≤ 14 . We show this using a standard argument from information theory, i.e., we derive a Le Cam-style lower bound, which reduces this problem to binary hypothesis testing. Towards that end let p− := 12 − w and p+ := 12 + w. Notice that since p+ − p− = 2w > w, no interval of width at most w can contain both p− and p+ simultaneously. We construct a hypothesis test trying to distinguish between those two parameters. Specifically, we test H0 : p = p −

against

H1 : p = p+

by

ψ(x1:t ) := 1p+ ∈I(δ;x1:t ) .

Because I has maximal width at most w, the event {p+ ∈ I(δ; x1:t )} implies p− ∈ / I(δ; x1:t ). Hence, by fixed-time validity of I we bound the false positive probability (type-I error) and the false negative probability (type-II error) respectively by δ, i.e. Pr(ψ = 1) ≤ Pr (p− ∈ / I(δ; X1:t )) ≤ δ, p−

p−

Pr(ψ = 0) = Pr (p+ ∈ / I(δ; X1:t )) ≤ δ. p+

p+

Thus the type-I and type-II errors satisfy α + β ≤ 2δ. On the other hand, by the Bretagnolle-Huber inequality [47, p. 190] we obtain 1 2 exp (−t KL(p− ∥p+ )) ≤ α + β ≤ 2δ

which is

log (1/(4δ)) ≤ t KL(p− ∥p+ ).

30

K. Kueffner et al.

For w ≤ 14 we compute     1 1 −w +w 1 1 + 2w 1 + = 2w log KL(p− ∥p+ ) = − w log 21 + w log 21 . 2 2 1 − 2w 2 +w 2 −w Using log(1 + x) ≤ x and − log(1 − x) ≤ x/(1 − x) for x ∈ [0, 1), we obtain log

2w 1 + 2w = log(1 + 2w) − log(1 − 2w) ≤ 2w + ≤ 8w, 1 − 2w 1 − 2w

and therefore KL(p− ∥p+ ) ≤ 16w2 . Substituting this into the previous bound gives r 1 log(1/(4δ)) 2 log (1/(4δ)) ≤ tKL(p− ∥p+ ) ≤ 16tw ⇐⇒ ≤w 4 t Notice that for every δ ≤ 81 1 4

r

log(1/(4δ)) 1 = t 4

r

log(1/δ) − log 4 1 ≥ t 4

s

1 3 log(1/δ)

t

1 = √ 4 3

r

log(1/δ) . t

Combining this with the case w > 1/4 results in ) ( r log(1/δ) 1 √ min 1, ≤ w. t 4 3 Since I ∈ I was arbitrary we get ) ( r 1 log(1/δ) √ min 1, ≤ W ⋆ (δ, t). t 4 3 D.1

Union Bound

Lemma 1. For any fixed-time confidence interval Ir with rate-optimal maximal width containing the empirical average, there exists an error probability δ0 > 0 and a transition probability P (r) ∈ [0, 1] s.t. for every δ ∈ (0, δ0 ] we have Pr [∀t ∈ N+ . P (r) ∈ Ir (δ; Z1:t )] = 0. In particular, Eq. (2) is violated. Proof (of Lem. 1). Assume p = 12 and let Ir be an empirically anchored fixedtime confidence interval with asymptotically rate-optimal maximal width. By Definition 1, there exists δ0 ∈ (0, 1) such that for every δ ∈ (0, δ0 ] there exist a constant C < ∞ and a sample count n0 ∈ N+ such that for all n ≥ n0 , r log(1/δ) WIr (δ, n) ≤ C . n Fix δ ∈ (0, δ0 ] and define Aδ := {∀t ∈ N+ : p ∈ Ir (δ; Z1:t )} ⊆ {∀n ≥ n0 : p ∈ Ir (δ; Z1:n )} .

Confidence Sequences for Online MDP-SMC

31

Since it suffices to show that Pr [∀n ≥ n0 : p ∈ Ir (δ; Z1:n )] = 0. Because Ir is empirically anchored, for every n ≥ n0 on the event {p ∈ Ir (δ; Z1:n )} we have r log(1/δ) µr (Z1:n ) − p ≤ Ir (δ; Z1:n ) ≤ WIr (δ, n) ≤ C . n Hence ( {∀n ≥ n0 : p ∈ Ir (δ; Z1:n )} ⊆

r ∀n ≥ n0 : µr (Z1:n ) − p ≤ C

log(1/δ) n

) .

Let Xi := 1Zi =r and Yi := 2(p − Xi ) ∈ {−1, +1}. Under p = 12 , the variables (Yi )i∈N+ are i.i.d. with E[Yi ] = 0 and Var(Yi ) = 1. Moreover, for every n ∈ N+ , n

|np − ξr (Z1:n )| =

1 X Yi 2 i=1

n

and thus

|µr (Z1:n ) − p| =

1 X Yi . 2n i=1

By the law of the iterated logarithm for i.i.d. mean-zero, variance-one variables, Pn | Yi | lim sup √ i=1 =1 almost surely. 2n log log n n→∞ p
√ Since n log(1/δ) = o n log log n , it follows that r Pn | i=1 Yi | log(1/δ) p > C or equivalently µr (Z1:n ) − p > C n 2 n log(1/δ) occurs infinitely often almost surely. In particular, " r Pr ∀n ≥ n0 : µr (Z1:n ) − p ≤ C

# log(1/δ) = 0. n

By the earlier inclusion, this implies that Pr[Aδ ] = 0.

Theorem 1. Let δ ∈ (0, 1), r ∈ S, N a grid, h a confidence spending function, and Ir a confidence interval. Then, Pr [∀i ∈ N+ . P (r) ∈ Ir (δ/h(i); Z1:ni )] ≥ 1−δ.

Proof P∞ (of Thm. 1). Let N = (ni )i∈N+ be an increasing grid and h satisfy i=1 1/h(i) ≤ 1. For each i ∈ N+ , define the “failure event” Ei := {p ∈ / Ir (δ/h(i); Z1:ni )} . By fixed-time validity of Ir with level δ/h(i) at sample size ni , Pr[Ei ] ≤ δ/h(i)

for all i ∈ N+ .

32

K. Kueffner et al.

P We now take a union bound over the grid and because i 1/h(i) ≤ 1 we get "∞ # [ Pr [∃i ∈ N : p ∈ / Ir (δ/h(i); Z1:ni )] = Pr Ei i=1

≤

∞ X i=1

Pr[Ei ] ≤

∞ X

δ/h(i) ≤ δ.

i=1

Theorem 2. Let δ ∈ (0, 1), r ∈ S, Ir a confidence interval with rate-optimal maximal width, and a, b, c ∈ R with a > 1 and b, c ≥ 1. Applying polynomial and exponential grids under polynomial and exponential spending impacts the rate-optimal maximal widths (and its constants) as follows: hapoly

haexp

b,1 Npoly

p p (a log(ni /b) + log(ηp /δ))/ni ((ni /b) log a + log(ηe /δ))/ni q p p b,c Npoly ((a/c) log(ni /b) + log(ηp /δ))/ni ( c ni /b log a + log(ηe /δ))/ni q p i /b) b,c Nexp (a log logc (ni /b) + log(ηp /δ))/ni ( log(n log(c) log a + log(ηe /δ))/ni .

Proof (of Thm. 2). In the following, we write ≍ to denote (asymptotic) equality up to constants. Assume that Ir has rate-optimal maximal width, i.e.   s  log(1/δ)  1 ≥ WIr (δ, ni ) ≍ min 1, ,  ni  uniformly over δ ∈ (0, 1) and i ∈ N+ . Since we clip the interval and are interested in the asymptotic rate we focus on the non-constant term only. On any grid, plugging in δ = δ/h(i) gives s log(h(i)/δ) WIr (δ/h(i), ni ) ≍ . ni b,c Polynomial grid Npoly = (⌊bic ⌋)i . Ignoring floors at the ≍ level, ni ≍ bic , hence i ≍ (ni /b)1/c and log i = 1c log(ni /b) + O(1). Thus  a  h (i) log poly = a log i + log(ηp /δ) = ac log(ni /b) + log(ηp /δ) + O(1), δ

and log

 a

hexp (i) δ



= i log a + log(ηe /δ) = (ni /b)1/c log a + log(ηe /δ) + O(1).

p Substituting into log(h(i)/δ)/ni results in the two claimed expressions up to multiplicative constants. b,c Exponential grid Nexp = (⌊bci ⌋)i . Again ni ≍ bci , hence i = logc (ni /b) + O(1) and log i = log logc (ni /b) + O(1). Therefore  a  h (i) log poly = a log i + log(ηp /δ) = a log logc (ni /b) + log(ηp /δ) + O(1), δ

Confidence Sequences for Online MDP-SMC

33

and log

 a

hexp (i) δ



= i log a + log(ηe /δ) = logc (ni /b) log a + log(ηe /δ) + O(1).

b,1 Substituting finishes the proof (and the Npoly row is the special case c = 1).

Lemma 2. Let δ ∈ (0, 1), r ∈ S, Ir a confidence interval with rate-optimal maximal width, and N a grid. Then, for every a, b ∈ R such that a, b > 1, we get for large i ∈ N+ that WIr (δ/hapoly (i), ni ) ≤ WIr (δ/hbexp (i), ni ). Proof (of Lem. 2). Let Ir have rate-optimal maximal width. Then there exist constants 0 < c0 ≤ C0 < ∞, a sample count n0 ∈ N+ , and an error probability δ0 ∈ (0, 1) such that for all n ≥ n0 and all δ ∈ (0, δ0 ], r r log(1/δ) log(1/δ) c0 ≤ WIr (δ, n) ≤ C0 ≤ 1. n n Fix a grid N = (ni ) and parameters a, b > 1. For polynomial spending hapoly (i) = ηp ia and exponential spending hbexp (i) = ηe bi , we have    a  h (i) hbexp (i) = i log b + log(ηe /δ). log poly = a log i + log(η /δ), log p δ δ Since a log i = o(i), there exists i0 ∈ N+ such that for all i ≥ i0 , C02 (a log i + log(ηp /δ)) ≤ c20 (i log b + log(ηe /δ)) . Therefore, for all sufficiently large i, s WIr (δ/hapoly (i), ni ) ≤ C0 s ≤ c0

a log i + log(ηp /δ) ni

i log b + log(ηe /δ) ni

≤ WIr (δ/hbexp (i), ni ) ≤ 1. Corollary 1. For every error probability, every confidence interval with rateoptimal maximal width, every grid with constant spacing, and every exponential spending function, the resulting maximal widths fail to converge to 0. Proof (of Cor. 1). Let N = (ni )i∈N+ be a grid with constant spacing. Then ni = Θ(i). Hence, by Thm. 2, under exponential spending we obtain WIr (δ/haexp (i), ni ) = Θ(1). In particular, the maximal widths do not converge to 0. Lemma 5. The empirical Bernstein interval IrB (App. C.2) has rate-optimal maximal width. Proof. Since IrB is a Bernoulli confidence interval, we have WIrB (δ, t) ≥ W⋆ (δ, t) for all δ ∈ (0, 1) and t ∈ N+ . By the optimal maximal width convergence rate

34

K. Kueffner et al.

from App. C.1, there exist constants c0 > 0, t0 ∈ N+ , and δ0 ∈ (0, 1) such that for all t ≥ t0 and δ ∈ (0, δ0 ], r log(1/δ) 1 ≥ WIrB (δ, t) ≥ c0 . t It remains to prove the matching upper bound. Fix t ∈ N+ , δ ∈ (0, 1), and a sample sequence z1:t ∈ Rt . By definition of IrB , r 2σr (z1:t ) log(3/δ) 14 log(3/δ) B |Ir (δ; z1:t )| ≤ 2 + . t 3(t − 1) Since σr (z1:t ) ≤ 14 for Bernoulli samples we get r 2 log(3/δ) 14 log(3/δ) B |Ir (δ; z1:t )| ≤ + . t 3(t − 1) p We now distinguish two cases. If log(3/δ) ≥ t and t ≥ 2, then 2 log(3/δ)/t ≥ 1 and the confidence interval is trivial. Otherwise, for t > 1 we have r log(3/δ) log(3/δ) 2 log(3/δ) ≤ ≤2 , t−1 t t and therefore r

2 log(3/δ) 14 log(3/δ) + t 3(t − 1) r r 2 log(3/δ) 14 log(3/δ) ≤ + 2 t 3 t r  √ 28 log(3/δ) ≤ 2+ . 3 t

|IrB (δ; z1:t )| ≤

Taking the supremum over all sample sequences gives  r √ 28 log(3/δ) WIrB (δ, t) ≤ 2+ . 3 t It remains to replace log(3/δ) by log(1/δ). For every δ ∈ (0, 1), log(3/δ) = log(1/δ) + log 3. Hence, for every δ ∈ (0, δ0 ], log(3/δ) log 3 log 3 =1+ ≤1+ . log(1/δ) log(1/δ) log(1/δ0 ) Therefore,  log(3/δ) ≤

log 3 1+ log(1/δ0 )

 log(1/δ)

for all δ ∈ (0, δ0 ].

Confidence Sequences for Online MDP-SMC

35

Substituting this into the previous bound r  s √ 28 log 3 log(1/δ) 2+ 1+ WIrB (δ, t) ≤ . 3 log(1/δ0 ) t Thus, with C0 :=

 √

28 2+ 3

s 1+

log 3 , log(1/δ0 )

we obtain for all t ≥ max{2, t0 } and all δ ∈ (0, δ0 ] that r log(1/δ) . WIrB (δ, t) ≤ C0 t Together with the lower bound, this proves that IrB has rate-optimal maximal width.

Lemma 6. The Clopper–Pearson interval IrC (App. C.2) has rate-optimal maximal width.

Proof. Since IrC is a Bernoulli confidence interval, we have WIrC (δ, t) ≥ W ⋆ (δ, t) for all δ ∈ (0, 1) and t ∈ N+ . By the optimal maximal width convergence rate from App. C.1, there exist constants c0 > 0, t0 ∈ N+ , and δ0 ∈ (0, 1) such that for all t ≥ t0 and δ ∈ (0, δ0 ], r log(1/δ) WIrC (δ, t) ≥ c0 . t It remains to prove the matching upper bound. We fix t ∈ N+ , δ ∈ (0, 1), and z1:t ∈ Rt , and denote kt := ξr (z1:t ) and p̂t := µr (z1:t ) = ktt . We denote the Clopper-Pearson interval by r log(2/δ) C Ir (δ; z1:t ) = [ℓt , ut ] and set εt (δ) := . 2t We demonstrate the claim by proving that the Clopper-Pearson interval is always contained inside the Hoeffding interval, i.e., p̂t − εt (δ) ≤ ℓt ≤ ut ≤ p̂t + εt (δ). We bound the upper endpoint. If kt = t, then ut = 1 = P̂t ≤ P̂t + εt (δ). Now assume kt < t. By definition of the Clopper–Pearson upper endpoint, ut is the unique solution of
δ Pr Bin(t, ut ) ≤ kt = . ut 2

36

K. Kueffner et al.

For p = P̂t + εt (δ), Hoeffding’s inequality gives  
1 Bin(t, p) ≤ P̂t Pr Bin(t, p) ≤ kt = Pr p p t   1 ≤ Pr Bin(t, p) ≤ p − εt (δ) p t
δ ≤ exp −2tεt (δ)2 = . 2 Since p 7→ Prp (Bin(t, p) ≤ kt ) is decreasing, it follows that ut ≤ P̂t + εt (δ). The lower bound can be proven analogously. Both bounds can be combined to obtain r 2 log(2/δ) C |Ir (δ; z1:t )| = ut − ℓt ≤ 2εt (δ) = . t Taking the supremum over all sample sequences gives r 2 log(2/δ) . WIrC (δ, t) ≤ t As in Lem. 5 we can resolve the log(2) to obtain our finial result that there exists C0 < ∞ such that for all t ≥ t0 and all δ ∈ (0, δ0 ], r log(1/δ) ≤ 1. WIrC (δ, t) ≤ C0 t Together with the lower bound, this proves that IrC has rate-optimal maximal width. D.2

Confidence Sequences

We additionally provide a formal proof that requiring correctness at all times (in the sense of Eq. (2)) is equivalent to correctness at a single “data-driven” time, i.e. a time that is adaptively chosen based on the observations, formally called a stopping time. Lemma 7. Let δ ∈ (0, 1) be an error probability, Sr : (0, 1) × R∗ → 2[0,1] for successor r ∈ R, then Pr[∀t ∈ N+ : P (r) ∈ Sr (δ; Z1:t )] ≥ 1 − δ if and only if Pr[P (r) ∈ Sr (δ; Z1:τ )] ≥ 1 − δ for all stopping times τ . Proof (of Lem. 7). A similar, but more condensed proof can be found in [37]. Let Ct be Ft -measurable sets and fix µ. (⇒) Since {µ ∈ / Cτ } ⊆ {∃t ∈ N+ : µ ∈ / Ct }, we have Pr[µ ∈ / Cτ ] ≤ Pr[∃t : µ ∈ / Ct ] ≤ δ, so Pr[µ ∈ Cτ ] ≥ 1 − δ. (⇐) Define τ := inf{t ∈ N+ : µ ∈ / Ct } and τn := min(τ, n). Then τn is a stopping time and {τ ≤ n} ⊆ {µ ∈ / Cτn }, so by the assumed stopping-time guarantee, Pr[τ ≤ n] ≤ Pr[µ ∈ / Cτn ] ≤ δ

for all n.

Confidence Sequences for Online MDP-SMC

37

Letting n → ∞ results in Pr[τ < ∞] ≤ δ, i.e. Pr (∃t ∈ N+ : µ ∈ / Ct ) ≤ δ

⇐⇒

Pr (∀t ∈ N+ : µ ∈ Ct ) ≥ 1 − δ.

Theorem 3. SrSH , SrSB , SrBH , and SrBB are confidence sequences (Eq. (2)). Proof (of Thm. 3). This is a direct consequence of [37, Thm. 1] for the stitched bounds and [64, Prop. 1 and Thm. 2] for the betting bounds. D.3

Test Confidence Sequences

Consistent. Let νr : S ∗ → D([0, 1]) map observations to a parameter distribution, define for q ∈ (0, 1). We call the function νr consistent if νr (Z1:t ) converges almost surely to the true parameter P (r). Similarly, let ν : S ∗ → D(D(R)) map state observations to a distribution over successor distributions. We call the function ν consistent if ν(Z1:t ) converges almost surely to the true successor distribution P . Notation. For r ∈ S and z1:t ∈ S t we can rewrite the condition Mrνr (q; z1:t ) ≤ 1/δ as −ξr (z1:t ) log(q) − (t − ξr (z1:t )) · log(1 − q) | {z } =:αr (q;z1:t ), variable in q

≤ log(1/δ) − |

Z 1

Xt i=1

log 0

u1zi =r (1 − u)1−1zi =r νr (z1:i−1 )(du) . {z }

=:βrνr (z1:t ), constant in q ν

And the condition for C M (δ; z1:t ) as −

X

ξr (z1:t ) log Q(r) ≤ log(1/δ) −

Z log

i=1

r∈R

|

t X

{z

}

=:α(Q;z1:t ), variable in Q

|

U (zi ) ν(z1:i−1 )(dU ) . D(R)

{z

}

=:β ν (z1:t ), constant in Q

We remark that α(Q; z1:t ) ≤ β ν (z1:t ) is simply a rewritten form of the expression M ν (Q; z1:t ) ≤ 1/δ. Since the former separates the parts that depend on Q from the parts that are constant Q, it is more convenient for the proofs. M νr

Theorem 4. Let δ ∈ (0, 1), r ∈ R, and Mrνr as in Eq. (4). Then Cr r is a valid confidence sequence (satisfying Eq. (2)) and if νr (Z1:t ) converges to P (r) a.s. M νr then Cr r converges to P (r). Proof (of Thm. 4). Fix δ ∈ (0, 1). For q ∈ {0, 1}. Then Mt (q) := Mrνr (q; Z1:t ) = 1 almost surely and therefore a test-martingale. Hence, Pr(∃t ∈ N+ . Mrνr (q; Z1:t ) ≥ 1/δ) = 0, which means the true parameter will never be rejected incorrectly. For q ∈ (0, 1) and t ∈ N+ , write Mt (q) :=

Mrνr (q; Z1:t ) =

t Y i=1

Z 1 Ai (q),

Ai (q) := 0

uXi (1 − u)1−Xi νr (Z1:i−1 )(du), q Xi (1 − q)1−Xi

38

K. Kueffner et al.

Clearly M0 (q) = 1 and Mt (q) ≥ 0. Test-martingale property under q. Assume the null hypothesis p = q, i.e., Xi ∼ Bernoulli(q) i.i.d. and Xi is independent of Fi−1 . Since νr (Z1:i−1 ) is Fi−1 measurable, we can condition on Fi−1 and use Fubini and the tower property  Z 1  Xi u (1 − u)1−Xi F Eq [Ai (q) | Fi−1 ] = Eq Xi i−1 νr (Z1:i−1 )(du) q (1 − q)1−Xi 0  Z 1 u 1−u q · + (1 − q) · = νr (Z1:i−1 )(du) q 1−q 0 =∈ t10 1 · νr (Z1:i−1 )(du) = 1. Hence, for all t ≥ 1, Eq [Mt (q) | Ft−1 ] = Eq [Mt−1 (q)At (q) | Ft−1 ] = Mt−1 (q)Eq [At (q) | Ft−1 ] = Mt−1 (q), so (Mt (q))t∈N+ is a test martingale under p = q. M νr

Inversion and Ville. Let Cr r (δ; Z1:t ) := {q ∈ [0, 1] : Mt (q) ≤ 1/δ} which clearly satisfies {q ∈ [0, 1] : Mt (q) < 1/δ} ⊆ {q ∈ [0, 1] : Mt (q) ≤ 1/δ}. By Ville’s inequality under p = q, " Pr sup Mt (q) q

t∈N+

# ≥ 1δ

≤ δ.

For any stopping time τ , M νr {q ∈ / Cr r (δ; Z1:τ )} = {Mτ (q) > 1/δ} ⊆

)

( sup Mt (q) ≥ 1/δ

,

t∈N+

h i M νr hence Prq q ∈ / Cr r (δ; Z1:τ ) ≤ δ. Applying this with q = p provides us with   M νr Pr p ∈ Cr r (δ; Z1:τ ) ≥ 1 − δ. The time-uniform guarantee follows directly from Lem. 7. If νr is consistent, then the convergence statement follows by invoking Lem. 8 for a 2-dimensional multinomial.

ν

Theorem 5. Let δ ∈ (0, 1) and M ν as in Eq. (5). Then C M is a valid confidence ν sequence, i.e. Pr ∀t ∈ N+ . P ∈ C M (δ; Z1:t ) ≥ 1 − δ and if ν(Z1:t ) converges to ν the successor distribution P a.s. then C M converges to P .

Confidence Sequences for Online MDP-SMC

39

Proof (of Thm. 5). Fix δ ∈ (0, 1) and write P := P () ∈ D(R). For Q ∈ D(R) and t ∈ N+ , write Mt (Q) := M ν (Q; Z1:t ) =

t Y

Z Bi (Q),

U (Zi ) ν(Z1:i−1 )(dU ). D(R) Q(Zi )

Bi (Q) :=

i=1

Clearly M0 (Q) = 1 and Mt (Q) ≥ 0. Test-martingale property under Q. Assume the null hypothesis P = Q, i.e., Zi ∼ Q i.i.d. and independent of Fi−1 = σ(Z1:i−1 ). Since ν(Z1:i−1 ) is Fi−1 -measurable, we have   Z U (Zi ) Fi−1 ν(Z1:i−1 )(dU ) EQ [Bi (Q) | Fi−1 ] = EQ Q(Zi ) D(R) ! Z X U (r) = Q(r) ν(Z1:i−1 )(dU ) Q(r) D(R) r∈R ! Z X U (r) ν(Z1:i−1 )(dU ) = D(R)

r∈R

Z 1 · ν(Z1:i−1 )(dU ) = 1.

= D(R)

Therefore, EQ [Mt (Q) | Ft−1 ] = EQ [Mt−1 (Q)Bt (Q) | Ft−1 ] = Mt−1 (Q), so (Mt (Q))t∈N+ is a test martingale under P = Q. ν

Inversion and Ville. Let C M (δ; Z1:t ) := {Q ∈ D(R) : Mt (Q) ≤ 1/δ}. Ville’s inequality under P = Q provides the guarantee that # " Pr sup Mt (Q) ≥ 1δ Q

≤ δ.

t∈N+

For any stopping time τ , ( {Q ∈ /C

Mν

(δ; Z1:τ )} = {Mτ (Q) > 1/δ} ⊆

) sup Mt (Q) ≥ 1/δ

.

t∈N+

  ν Therefore, PrQ Q ∈ / C M (δ; Z1:τ ) ≤ δ. Applying this with Q = P gives   ν Pr P ∈ C M (δ; Z1:τ ) ≥ 1 − δ. The time-uniform guarantee follows directly from Lem. 7. If ν is consistent, then the convergence statement is exactly Lem. 8.

Lemma 3. Let δ ∈ (0, 1), r ∈ R, and Mrνr as in Eq. (4). Then log Mrνr (q, z1:t ) is convex in q ∈ (0, 1) with minimum at µr (z1:t ) when µr (z1:t ) ∈ (0, 1).

40

K. Kueffner et al.

Proof (of Lem. 3). Fix δ ∈ (0, 1), r ∈ R, and z1:t ∈ Rt . Recall αr (q; z1:t ) := −ξr (z1:t ) log q − (t − ξr (z1:t )) log(1 − q),

q ∈ (0, 1).

Let k := ξr (z1:t ). For q ∈ (0, 1), αr′ (q; z1:t ) = −

t−k k + , q 1−q

and

αr′′ (q; z1:t ) =

t−k k + . 2 q (1 − q)2

Since k ∈ {0, 1, . . . , t} and q ∈ (0, 1), we have αr′′ (q; z1:t ) ≥ 0

for all q ∈ (0, 1),

and hence αr (·; z1:t ) is convex on (0, 1). If 0 < k < t, then αr′′ (q; z1:t ) > 0 for all q ∈ (0, 1), so αr (·; z1:t ) is strictly convex. Moreover, αr′ (q; z1:t ) = 0 ⇐⇒ −

k t−k k + = 0 ⇐⇒ q = = µr (z1:t ). q 1−q t

Thus, if 0 < µr (z1:t ) < 1, the unique minimiser is q = µr (z1:t ). If k = 0, then αr′ (q; z1:t ) =

t >0 1−q

for all q ∈ (0, 1),

so αr (·; z1:t ) is strictly increasing on (0, 1). If k = t, then αr′ (q; z1:t ) = −

t <0 q

for all q ∈ (0, 1),

so αr (·; z1:t ) is strictly decreasing on (0, 1). In all three cases, every sublevel set of αr (·; z1:t ) in (0, 1) is an interval. Theorem 6. Let t ∈ N+ , δ ∈ (0, 1), z1:t ∈ S t , and V : R → R. Assume ξr (z1:t ) > 0 for all r ∈ R (otherwise restrict to {r | ξr (z1:t ) > 0} and assign all remaining mass to an extremiser of V among {r | ξr (z1:t ) = 0}). If V is ν not constant and C M (δ; z1:t ) ̸= ∅, then ( X P̂ (z1:t ) if M ν (P̂ (z1:t ); z1:t ) = 1/δ Q⋆η ∈ arg min Q(r) · V (r) = ξr (z1:t ) P , ξu (z1:t ) otherwise Q∈C M ν (δ;z1:t ) r∈R u∈R η+V (u) η+V (r) / where η > − minr∈R V (r) is the unique solution of M ν (Q⋆η ; z1:t ) = 1/δ and M ν (Q⋆η ; z1:t ) is strictly decreasing in η. Proof (of Thm. 6). Fix t ∈ N+ , δ ∈ (0, 1), z1:t ∈ S t , and V : R → R. Write Nt (r) := ξr (z1:t ), αt (Q) := α(Q; z1:t ), and βt := β ν (z1:t ). First we deal with the zero-count states. Let Rt := {r ∈ R | Nt (r) > 0}. If Rt ̸= R, then the constraint X X αt (Q) = − Nt (r) log Q(r) = − Nt (r) log Q(r) r∈R

r∈Rt

Confidence Sequences for Online MDP-SMC

41

depends only on (Q(r))r∈Rt . Hence we may first solve the optimisation over Rt and then allocate any remaining mass X m := 1 − Q(r) r∈Rt

to an extremiser of V over R \ Rt (argmin for the infimum, argmax for the supremum). Thus, it suffices to treat the case Rt = R, equivalently Nt (r) > 0 for all r ∈ R. We restate the minimisation problem as X min Q(r)V (r) Q∈RR

s.t.

r∈R

X

αt (Q) ≤ βt ,

Q(r) = 1,

Q(r) > 0 ∀r ∈ R.

r∈R

Let P̂t := Nt (·)/t, the empirical distribution. We distinguish two cases. Case 1: αt (P̂t ) = βt . Since P̂t minimises αt over the simplex and is feasible, every feasible Q satisfies βt ≥ αt (Q) ≥ αt (P̂t ) = βt . Hence αt (Q) = βt for every feasible Q. By strict convexity of αt , the minimiser over the simplex is unique, so Q = P̂t . Hence, the releasable set is {P̂t } and P̂t is the minimiser. Case 2: αt (P̂t ) < βt . Then P̂t is a strictly feasible point, so Slater’s condition holds. Hence, the KKT conditions are necessary and sufficient. We introduce Lagrange multipliers η ∈ R for the simplex constraint and λ ≥ 0 for the log-constraint, and define ! X X Q(r)V (r) + η Q(r) − 1 + λ (αt (Q) − βt ) . L(Q, η, λ) := r∈R

r∈R

Due to stationarity with respect to Q(r), we know that the gradient of the Lagrangian w.r.t. the coordinates of Q must vanish in the optimum. Hence, we take the derivative and set it to 0, i.e., for all r ∈ R ∂L Nt (r) = V (r) + η − λ =0 ∂Q(r) Q(r)

and therefore

Q(r) =

λNt (r) . η + V (r)

Thus necessarily η > − min P r∈R V (r), as otherwise the expression becomes negative or undefined. Using r Q(r) = 1 we obtain !−1 X λNt (r) X Nt (u) 1= ⇐⇒ λ= , η + V (r) η + V (u) r∈R

u∈R

hence every KKT point is of the form Nt (r) η+V (r) Nt (u) u∈R η+V (u)

Q⋆η (r) = P

for all r ∈ R.

42

K. Kueffner et al.

If λ = 0, then stationarity implies V (r) + η = 0 which means that V is constant on R, contrary to assumption. Hence λ > 0, and complementary slackness implies that the log-constraint is active: αt (Q⋆η ) = βt . It remains to prove existence and uniqueness of η. A direct computation gives αt (Q⋆η ) = −

X

Nt (r) log Nt (r) +

r∈R

X

X

Nt (r) log(η + V (r)) + t log

r∈R

u∈R

Nt (u) η + V (u)

!

Hence αt (Q⋆η ) is continuous in η on (− minu V (u), ∞). We show that αt (Q⋆η ) is strictly decreasing in η by taking the derivative, i.e., d B(η) A(η)2 − tB(η) αt (Q⋆η ) = A(η) − t = . dη A(η) A(η) where A(η) :=

X u∈R

Nt (u) , η + V (u)

By Cauchy-Schwarz, !2 p p X Nt (u) Nt (u) 2 < A(η) = η + V (u) u∈R

B(η) :=

X u∈R

X u∈R

Nt (u) . (η + V (u))2

Nt (u) (η + V (u))2

!

! X

Nt (u)

= tB(η),

u∈R

where the inequality is strict because V is not constant on R. Thus d αt (Q⋆η ) < 0 dη

for all η > − min V (u), u∈R

Finally, if we take η ↓ − minu∈R V (u), at least one denominator tends to 0 implying that αt (Q⋆η ) → +∞, and if we take η → ∞, we get Q⋆η (r) → Nt (r)/t, together they imply αt (Q⋆η ) → αt (Nt (·)/t). Therefore, by continuity and strict monotonicity, there exists a unique η > − minu V (u) such that αt (Q⋆η ) = βt . This yields the claimed minimiser. The supremum problem is identical after replacing V by −V .

Lemma 8. Let δ ∈ (0, 1) and M ν as in Eq. (5) with a consistent ν and let ν Ct = C M (δ; Z1:t ). Then, for every ε > 0, there exists an almost surely finite random time Tε such that Ct ⊂ {Q ∈ D(R) | ∥Q − P ∥1 < ε} for all t ≥ Tε almost surely. Moreover, on the event {supt∈N+ M ν (P ; Z1:t ) ≤ 1/δ}, we have P ∈ Ct for all t ∈ N+ and diam∥·∥1 (Ct ) → 0 as t → ∞. Proof (of Lem. 8). For i ∈ N+ define the predictive mean Z Li−1 (r) := U (r)ν(Z1:i−1 )(dU ) ∈ [0, 1], D(R)

r ∈ R,

.

Confidence Sequences for Online MDP-SMC

43

so that M ν (Q; Z1:t ) =

t Y Li−1 (Zi ) i=1

Q(Zi )

.

Let P ∈ D(R). First, we show the growth rate of the test martingale. Fix any Q ∈ D(R). If Q(r) = 0 for some r ∈ R, then Zi = r occurs infinitely often a.s., hence M ν (Q; Z1:t ) = +∞ for all sufficiently large t. Thus assume Q(r) > 0 for all r ∈ R. Taking logs and adding/subtracting log P (Zi ) yields t t 1 1X 1X P (Zi ) log M ν (Q; Z1:t ) = (log Li−1 (Zi ) − log P (Zi )) + log . t t i=1 t i=1 Q(Zi )

By consistency, for every r ∈ R we have Li−1 (r) → P (r) a.s. Since R is finite and P (r) > 0 for all r, this implies max |log Li−1 (r) − log P (r)| → 0 r∈R

a.s.

Hence also log Li−1 (Zi ) − log P (Zi ) → 0 a.s., and therefore t

1X (log Li−1 (Zi ) − log P (Zi )) → 0 t i=1

a.s.

For the second term, let Pbt (r) := ξr (Z1:t )/t denote the empirical distribution. Then t

X 1X P (Zi ) P (r) log = Pbt (r) log t i=1 Q(Zi ) Q(r) r∈R

=

X r∈R

Pbt (r) X b Pbt (r) Pbt (r) log − Pt (r) log Q(r) P (r) r∈R

= KL(Pbt ∥Q) − KL(Pbt ∥P ), where we use the convention 0 log(0/x) = 0. By the strong law of large numbers, Pbt → P a.s. Since P has full support, also KL(Pbt ∥P ) → 0 a.s. Moreover, for every fixed Q = ̸ P , KL(Pbt ∥Q) → KL(P ∥Q) and therefore 1t log M ν (Q; Z1:t ) → KL(P ∥Q), which implies M ν (Q; Z1:t ) → ∞ almost surely.

Fix ε > 0 and define Kε := {Q ∈ D(R) : ∥Q − P ∥1 ≥ ε}. To obtain a uniform bound over Kε , let t

At :=

1X (log Li−1 (Zi ) − log P (Zi )) , t i=1

44

K. Kueffner et al.

so that for every Q ∈ D(R), 1 log M ν (Q; Z1:t ) = At + KL(Pbt ∥Q) − KL(Pbt ∥P ). t By the previous part, At → 0, KL(Pbt ∥P ) → 0, and Pbt → P a.s., so there exists (1) (1) an a.s. finite random time Tε such that for all t ≥ Tε , ε ∥Pbt − P ∥1 < . 2 (1)

Hence, by the reverse triangle inequality for every Q ∈ Kε and every t ≥ Tε , ε ∥Pbt − Q∥1 ≥ ∥Q − P ∥1 − ∥Pbt − P ∥1 ≥ . 2 Therefore, by Pinsker’s inequality, 1  ε 2 ε2 KL(Pbt ∥Q) ≥ = 2 2 8

for all Q ∈ Kε and all t ≥ Tε(1) .

Since At → 0 and KL(Pbt ∥P ) → 0 a.s., there exists an a.s. finite random time (2) (2) Tε such that for all t ≥ Tε , |At | ≤

ε2 32

and (1)

KL(Pbt ∥P ) ≤

ε2 . 32

(2)

Thus, for all t ≥ Tε := max{Tε , Tε } and all Q ∈ Kε , 1 ε2 ε2 ε2 ε2 log M ν (Q; Z1:t ) ≥ − + − = . t 32 8 32 16 Hence, for all t ≥ Tε and all Q ∈ Kε ,  2  ε M (Q; Z1:t ) ≥ exp t . 16 ν

By increasing Tε further if necessary, we obtain for all t ≥ Tε and all Q ∈ Kε , M ν (Q; Z1:t ) ≥

1 . δ

Therefore, for all t ≥ Tε we have Kε ∩ Ct = ∅, i.e. Ct ⊂ {Q : ∥Q − P ∥1 < ε}. Let ( ) E :=

sup M ν (P ; Z1:t ) ≤ 1/δ

.

t∈N+

By Ville’s inequality under P , Pr[E] ≥ 1 − δ. We now condition on E. Hence, we have M ν (P ; Z1:t ) < 1/δ for all t, and thus P ∈ Ct for all t. Since the previous step holds for every ε > 0, it follows that on E the sets Ct eventually lie in every ℓ1 -ball around P , so diam∥·∥1 (Ct ) → 0.

Confidence Sequences for Online MDP-SMC

E

Further Experimental Data

E.1

Individual Inference

45

In this section, we present further data on the evaluation of our inference methods on individual distributions. As distribution classes, we consider 2, 5, 10, and 50 successors, and uniform, linear, squared and one-vs-all probability distribution, as follows: Uniform distributions assign 1/n probability to each successor, linear / squared assign a relative probability of i / i2 to the i-th successor, and one-vs-all assigns 0.5 to the first and 0.5/n to all others. We then add some noise by scaling each probability with a random factor between 0.9 and 1.1. The results are summarized in Figs. 3 to 6. Before further discussion of the results, we remark that our implementation of Clopper-Pearson (relying on the apache-commons library) runs into numerical issues for large sample counts and small confidences, due to the inverse Beta-distribution (as well as the the alternative F-distribution) lacking a closed form. Similarly, our (naive) implementation of ValueTest sometimes exhibits numerical instability in the computation. We took care in our implementation to round conservatively, ensuring correctness. We also implemented a variant using arbitrary precision rationals, however this seems too slow for quick evaluation. We complement the additional data with some further discussion: Firstly, we comment on the discussion of asymptotical convergence in Sec. 3.1. For the exponentially spaced methods (suffix -Exp), we clearly see the gaps of increasing length (note the fact that the x-axis is log-scale), with the estimates stagnating. The restrained spending of exponentially spaced grids often yields quite good estimates at the individual grid points, as it “concentrates” a lot of confidence on these points. Nonetheless, they are (eventually) outperformed by several confidence sequences such as Bern-Bet, Bern-Stitch, and ValueTest. When comparing polynomially and exponential gridding, recall that Lem. 2 only considers asymptotic worst case, while we investigate a finite horizon on a fixed set of distributions. Hence, the exponential methods outperforming the sequential ones is not a contradiction to this lemma. Indeed, since the polynomial grid is much denser (gap-less), a significant penality is to be expected initially. Secondly, we compare the different confidence sequences: As for fixed-time confidence intervals (see [53]), the sequences based on Hoeffding’s inequality are overly conservative. Among the others, the differences are less pronounced, but still Bern-Bet, Bern-Stitch, and ValueTest perform well across all shapes and successor counts. In particular, in almost all plots, our novel ValueTest obtains the best precision for 105 samples, often dominating before that already.

46

K. Kueffner et al.

Hoeff-Exp Bern-Sq Hoeff-Bet ValueTest

Bern-Exp CP-Sq Bern-Bet Point CP

CP-Exp Hoeff-Stitch MLETest

Hoeff-Sq Bern-Stitch BetaTest

104 Uniform / 2 successors

105

104 Uniform / 5 successors

105

104 Uniform / 10 successors

105

104 Uniform / 50 successors

105

Fig. 3: Bounds on uniform distributions.

Confidence Sequences for Online MDP-SMC

Hoeff-Exp Bern-Sq Hoeff-Bet ValueTest

Bern-Exp CP-Sq Bern-Bet Point CP

CP-Exp Hoeff-Stitch MLETest

Hoeff-Sq Bern-Stitch BetaTest

104 Linear / 2 successors

105

104 Linear / 5 successors

105

104 Linear / 10 successors

105

104 Linear / 50 successors

105

Fig. 4: Bounds on linear distributions.

47

48

K. Kueffner et al.

Hoeff-Exp Bern-Sq Hoeff-Bet ValueTest

Bern-Exp CP-Sq Bern-Bet Point CP

CP-Exp Hoeff-Stitch MLETest

Hoeff-Sq Bern-Stitch BetaTest

104 Squared / 2 successors

105

104 Squared / 5 successors

105

104 Squared / 10 successors

105

104 Squared / 50 successors

105

Fig. 5: Bounds on squared distributions.

Confidence Sequences for Online MDP-SMC

Hoeff-Exp Bern-Sq Hoeff-Bet ValueTest

Bern-Exp CP-Sq Bern-Bet Point CP

CP-Exp Hoeff-Stitch MLETest

Hoeff-Sq Bern-Stitch BetaTest

104 105 One-vs-All / 2 successors

104 105 One-vs-All / 5 successors

104 105 One-vs-All / 10 successors

104 105 One-vs-All / 50 successors

Fig. 6: Bounds on one-vs-all distributions.

49

50

K. Kueffner et al.

Table 2: Description of all model / property combinations we consider, together with basic information about the model (number of states |S|, number of actions |A|, and average number of successors in each action Avg |∆|). Finally, we list the (arbitrarily chosen) precision and confidence values. Model

Constants

Property

|S|

|A|

bigmec N=1000 prob_max 2003 4004 consensus-mec N=2,K=2 disagree 2720 6680 consensus N=2,K=1 c2 144 208 csma N=2,K=2 all_before_max 1038 1053 evade-mdp N=3,slippery=0.7 prob_max 613 1545 firewire_dl delay=3,deadline=200 deadline 14 824 16 671 manymecs N=20 prob_max 62 122 mer n=1,x=0.1 prob_max 7526 17 773 pacman MAXSTEPS=7 crash 1272 1444 random-grid N=10,pstay=0.3,pover=0.3 prob_max 1000 4943 sensor.1 max_success 462 1068 wlan.2 COL=2 collisions 28 598 29 661 wlan4_collide COL=4,TIME_MAX=10,k=4 collide_max 345 120 355 727 wlan_dl.0 deadline=80 deadline 189 703 254 964 zeroconf reset=0,N=1000,K=1 correct_max 31 954 56 230

E.2

Avg|∆|

ε

γ

1.00 1.50 1.21 1.22 2.92 1.06 1.49 1.02 1.03 2.67 1.10 1.04 1.07 1.31 1.27

0.05 0.3 0.2 0.1 0.2 0.05 0.05 0.05 0.05 0.2 0.05 0.7 0.1 0.9 0.05

0.99 0.9 0.9 0.9 0.9 0.9 0.9 0.9 0.9 0.9 0.99 0.9 0.9 0.9 0.99

Online MDP-SMC

In this section, we provide further data on our MDP-SMC evaluation. Tab. 2 lists all models and properties together with basic data about them. Tab. 3 then provides the averaged sample counts for every benchmark and method we consider, i.e. the full data used to generate the aggregated scores in Tab. 1.

Bern-Bet Bern-Exp Bern-Sq Bern-Stitch BetaTest CAV19 CP-Exp CP-Sq Global-Bern-Exp Global-Bern-Sq Global-CP-Exp Global-CP-Sq Global-Hoeff-Exp Global-Hoeff-Sq Hoeff-Bet Hoeff-Exp Hoeff-Sq Hoeff-Stitch MLETest ValueTest

wlan_dl

wlan4_collide wlan

sensor

random-grid

pacman

mer

manymecs

firewire_dl

evade-mdp

csma

consensus

consensus-mec

bigmec

149 6971 333 297 5211 2673 8011 2230 825 1760 2377 57 3597 541 11 176 17 980 757 949 12 983 4443 8474 4763 1094 5319 4814 194 12 420 1751 42 275 20 364 1001 1144 13 962 6385 13 674 6618 1351 6051 6388 209 12 544 1668 41 98 9440 387 406 6194 2037 5246 2320 494 2672 2559 100 6182 905 18 69 4244 186 198 13 481 1233 3782 1456 525 3062 1368 28 6878 412 32 400 T/O 4409 3897 100 073 T/O 19 407 T/O 668 T/O 1 938 086 39 310 T/O T/O 452 167 6510 319 350 4961 2439 8110 2529 805 1428 1819 36 3355 220 15 185 8149 462 488 5571 4066 9311 3514 961 1845 2816 37 3381 195 18 151 T/O 4688 762 120 512 72 085 9219 T/O 851 T/O 841 198 823 467 417 T/O 17 152 585 007 1326 685 49 189 5107 7414 108 419 643 T/O 12 694 487 16 831 T/O 23 158 T/O 1031 358 T/O 42 594 7353 T/O 423 T/O 868 689 796 164 039 T/O 7 91 941 457 743 273 44 658 3120 4653 T/O 340 T/O 7988 285 6030 T/O 8 151 T/O 1433 646 850 852 58 978 6111 T/O 509 T/O 722 519 400 244 134 T/O 65 100 824 125 830 517 37 892 3591 6551 37 064 476 T/O 9266 240 8407 T/O 69 736 32 321 1692 1981 62 667 14 231 40 225 28 405 4907 9351 27 207 85 15 207 668 702 168 8250 455 500 11 799 3120 8235 5142 829 2327 4169 53 4880 396 151 209 9597 583 741 13 222 4524 10 561 6966 1233 2752 5887 50 4895 350 130 119 7025 359 466 9034 2304 5954 3909 667 1980 3693 48 4056 332 102 65 4217 190 200 13 431 1309 3782 1395 533 3088 1385 28 6872 415 35 76 4785 220 213 3173 1393 4006 1564 468 T/O 1384 30 2811 227 12

zeroconf

Table 3: Number of samples required (averaged over ten runs) of each inference approach on all considered models. For readability, we give the number of samples divided by 100, i.e. a cell value of 6 means that between 600 and 699 samples were required.

Confidence Sequences for Online MDP-SMC 51