Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet

David Parker; Eline M. Bovy; Marnix Suilen; Nils Jansen; Thom Badings

REVIEW 1 major objections 4 minor 122 references

Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet

T0 review · 1 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Robust MDPs are presented as the unifying framework for decision-making under probability uncertainty across AI and formal methods, with a tutorial showing how to solve them by adding an inner worst-case step to value and policy iteration.

desk verdict Solid RMDP tutorial that deserves a serious referee, but Section 3.2 oversells its reach-reward algorithms by leaving the graph-preservation qualifier out of the main equations. read the letter →

arxiv 2411.11451 v2 pith:WTTYBBAM submitted 2024-11-18 cs.AI math.OC

Marnix Suilen , Thom Badings , Eline M. Bovy , David Parker , Nils Jansen This is my paper · ORCID

classification cs.AImath.OC MSC 90C4068Q6093E35

keywords robustMarkovdecisionprocessesuncertaintysetsrectangularityvalueiterationpolicyreach-rewardobjectivesintervalMDPsformalverificationandreinforcementlearning

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper is a tutorial survey arguing that robust Markov decision processes (RMDPs) are the natural common framework when transition probabilities are not precisely known, which is the rule in both AI and formal verification. It develops RMDP semantics as a game between an agent and an adversarial nature that chooses from an uncertainty set, then shows that the familiar Bellman machinery survives: value iteration and policy iteration extend by replacing the expectation over a fixed transition function with an inner minimization over the uncertainty set at each state-action pair. The central tutorial claim is that for convex (s,a)-rectangular RMDPs this robust dynamic programming solves reach-reward objectives and that stationary deterministic optimal policies exist, using the same preprocessing as ordinary MDPs provided the uncertainty set is graph-preserving. A sympathetic reader comes away with a single recipe for turning any MDP solver into an RMDP solver, plus a map of where that recipe breaks down.

What carries the argument

The central object is the uncertain transition function P : U → (S×A ⇀ D(S)) with an uncertainty set U over transition variables, together with the notion of rectangularity that decides whether the adversary decomposes per state-action pair. The load-bearing identity is the robust Bellman equation $V^{{n+1}}$(s) = max_a { R(s,a) + inf_{P(s,a) ∈ P(s,a)} ∑_{s'} P(s,a,s') V^n(s') }, which reduces RMDP solving to ordinary value iteration with an extra inner optimization. For interval MDPs that inner problem is solved by a sorting and bisection algorithm; for L1-MDPs by a dual sorting algorithm; for general convex sets by convex optimization. Static versus dynamic uncertainty semantics and last-action observability are the two semantic knobs that, together with rectangularity and convexity, determine which policy class is sufficient.

What would settle it

Build a two-state RMDP where one transition has probability zero in one admissible transition function and positive probability in another, while the uncertainty set is still convex and (s,a)-rectangular. Running Equation (3) with the paper's preprocessing would classify that state inconsistently depending on which transition function is considered, making S∞ or S? ill-defined; observing that the value or the preprocessing changes discontinuously when the zero is changed to a small positive number shows the graph-preservation assumption is load-bearing and that the tutorial's claim is scoped to it.

Watch

Extended reading notes

Core claim

The survey's central claim is that RMDPs are a unifying model: they generalize bounded-parameter MDPs, L1-MDPs, multi-environment MDPs, and interval MDPs, and they carry over the standard solution methods. Robust value iteration replaces the sum over successor states by inf over the uncertainty set at each state-action pair, and under (s,a)-rectangularity the global adversary decomposes into local choices per state-action pair; if the uncertainty set is convex, the inner problem is efficiently solvable and stationary deterministic policies suffice. Robust policy iteration uses the same inner minimization in both policy evaluation and improvement. The paper is explicit that the reach-reward version requires graph preservation: every transition function in the uncertainty set must share the same zero-probability support, otherwise the standard S∞ and S? preprocessing is not well-defined.

Load-bearing premise

The recipe assumes graph preservation: every transition function in the uncertainty set must put probability zero on exactly the same transitions, so the standard reach-reward preprocessing is well-defined; if that fails, the presented algorithms do not apply.

Editorial extensions

If this is right

If the tutorial's recipe is correct, any MDP solver with value and policy iteration can be upgraded to handle convex (s,a)-rectangular RMDPs by plugging in an inner worst-case solver, and the resulting procedure inherits the same preprocessing and policy-extraction steps.
Reachability, discounted reward, and reach-reward objectives all fall out of the same framework by modifying the Bellman equation and preprocessing, so the recipe covers most objectives used in practice.
For s-rectangular, nonconvex, or non-rectangular uncertainty sets, the simple recipe stops working: optimal policies may need randomization and history, and policy evaluation becomes NP-hard, so these cases require specialised algorithms.
The same algorithms support optimistic variants, where the agent and nature cooperate, by replacing the inner infimum with a supremum, giving a dual view of the same uncertainty set.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Inference: the paper's dependence on graph preservation suggests that uncertainty sets built directly from sparse transition data, where some transitions are observed zero times in some states, fall outside the tutorial's algorithm; those sets would need a different preprocessing or a different inner problem.
Inference: the survey's comparison of robust value iteration and robust policy iteration points to a concrete open question the paper does not answer: whether policy iteration really is faster in practice because it solves fewer inner minimization problems.
Inference: the static/dynamic coincidence for (s,a)-rectangular RMDPs together with its failure in robust POMDPs suggests that partial observability is the real source of semantic fragility, so richer temporal-logic objectives for RMDPs may exhibit a similar sensitivity; the paper flags this as future work.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things you should know up front. This is a genuinely useful tutorial survey of robust MDPs, and if you need to point a newcomer to one place, this is a good candidate. And there is a real scoping problem in Section 3.2: Equations (3)–(5) are presented as the reach-reward adaptation for convex (s,a)-rectangular RMDPs, but they are only correct under the graph-preservation assumption of Remark 1, and that qualifier is not carried into the equations. The stress-test example is valid. Take a single non-target state with one action, reward 1, transitions to target with probability p and self-loop with probability 1−p, p∈[0,1]. The set is convex and (s,a)-rectangular but not graph preserving at p=0. The paper's preprocessing classifies s as S∞ because there exists a P that never reaches the target, so the equations give V(s)=∞. The game semantics of Section 4.2 make nature minimize, and nature would choose p=1 to stop the reward, giving value 1. So the tutorial's central algorithm is wrong on this model if applied literally. The paper does flag Remark 1 and later says adaptation to reach-reward is straightforward 'provided the graph preservation property is met,' but that caveat appears after Equations (3)–(5) have been asserted as a direct adaptation. A one-sentence 'throughout this section we assume graph preservation' before Equation (3) would fix the issue. The same caution applies to L1-MDPs, whose balls can have varying support; the IMDP definition correctly enforces zero-lower-bound-iff-zero-upper-bound, so that class is safe. What the paper does well: clean definitions, worked examples that check out (I verified Example 3 on last-action observability), a good complexity table, and a useful map of connections to stochastic games, POMDPs, pMDPs, and RL. It fills a real gap, since the only other RMDP survey is oriented to recent results rather than fundamentals. Technical content is attributed to the right sources, and the self-citations are appropriate for a survey from active authors. There is no new theorem, but a tutorial does not need one. Minor issue: references [40] and [95] both cite arXiv:2305.10546, but they are different papers; one arXiv ID is wrong. Bottom line: this paper deserves a careful referee and a conditional accept after a minor revision that moves the graph-preservation caveat into the main algorithmic section. I would cite it as the entry-point tutorial.

Referee Report

1 major / 4 minor

Summary. The paper is a survey and tutorial on robust Markov decision processes (RMDPs) intended to bridge the AI and formal-methods communities. After recalling MDPs and classical value iteration/policy iteration, it introduces RMDPs, classifies uncertainty sets by rectangularity, convexity, static/dynamic semantics, and graph preservation, and then presents robust dynamic programming for the (s,a)-rectangular case. It gives concrete inner-problem algorithms for interval MDPs and L1-MDPs, discusses instances such as multi-environment MDPs, and surveys connections to parametric MDPs, stochastic games, robust POMDPs, and distributional uncertainty. The final sections cover learning, abstraction, tool support, and future challenges.

Significance. The survey fills a genuine gap: there is little accessible tutorial material on RMDPs that speaks to both the AI and formal-methods communities. Its strengths are its clear progression from definitions to algorithms, the worked examples (notably Example 3 on last-action observability), the compact summary in Table 1, and the broad coverage of applications and tools. It is honest about several subtle semantic assumptions, for example by flagging graph preservation in Remark 1 and by pointing out that static/dynamic equivalence does not carry over to POMDPs. If the graph-preservation qualification is properly attached to the reach-reward equations, the tutorial will be a reliable entry point for researchers; with that fix, I would regard the survey as a solid contribution.

major comments (1)

[§3.2, Eqs. (3)-(5), with Remark 1] The reach-reward value-iteration and policy-iteration equations are displayed for convex (s,a)-rectangular RMDPs, but their correctness at the preprocessing level requires graph preservation (Remark 1), and this condition is not carried into the displayed statements. The S∞/S? preprocessing of §2.2 is defined via graph properties; without a fixed support, whether a state is in S∞ depends on which P∈P is considered. Concretely, take S={s,t}, T={t}, one action a, R(s,a)=1, and P(s,a,t)=p, P(s,a,s)=1-p with p∈[0,1]. This uncertainty set is convex and (s,a)-rectangular but not graph preserving. Applying the §2.2 preprocessing pointwise classifies s∈S∞ (the p=0 transition never reaches t), so Eq. (3) yields V(s)=∞. Under the game semantics described in §3.1 and §4.2, nature minimizes the agent's reward and chooses p=1, giving value V(s)=1. Thus the equations as stated are incorrect for this valid convex (s,a)-rectangular RMDP. The caveat in the 'Other objectives' paragraph later in §3.2 mentions graph preservation, but it appears after Eqs. (3)-(5) have already been asserted, and it is not linked to Definition 6 for L1-MDPs, whose L1 balls generally do not preserve support. I recommend explicitly restricting Eqs. (3)-(5) to graph-preserving convex (s,a)-rectangular RMDPs, or stating a separate robust definition of S∞/S? and showing that the equations remain correct without fixed support.

minor comments (4)

[§3.3, Algorithm 1] In Algorithm 1, lines 5-11, when the while loop exhausts all successor states (e.g., two successors with lower bounds 0 and upper bounds 0.5), i becomes m+1 and line 10 indexes outside the sorted list; the algorithm as printed does not return a valid distribution in that boundary case. Add a guard or return the all-upper-bound distribution. The text also calls this a bisection algorithm, while the pseudocode is a water-filling greedy method; the description should be aligned with the code.
[References] Reference [95] lists arXiv identifier 2305.10546, which is the same as reference [40] (Fijalkow et al., 'Games on graphs'); the identifier for [95] appears to be a typo.
[Definition 3] The symbol P is used for both the uncertain transition function (a set-valued object) and an element P∈P, which may confuse readers because Definition 1 uses P for a single transition function. Consider using a different script for the set.
[§3.1, Example 3] Example 3 is correct and helpful, but the arithmetic behind the values 55 and 75 could be spelled out explicitly for both actions to make the last-action-observability point fully transparent.

Circularity Check

0 steps flagged · score 1.0 of 10

Survey is a self-contained tutorial; no load-bearing circularity, with a minor scope caveat on graph preservation.

full rationale

This is a survey and tutorial rather than an original derivation chain, and its core algorithmic claims are imported from external prior work rather than from the authors' own results. The robust value iteration recursion in Eq. (3) is explicitly defined as replacing the standard MDP inner sum with an inner minimization over P, and Eqs. (4)-(5) follow from rectangularity and convexity; the optimal-policy-class facts are attributed to Wiesemann et al. [118] and Iyengar [64], not to the present authors. Self-citations such as [17], [110], and [112] point to related RPOMDP and MEMDP work and are not used to justify the tutorial's Bellman equations. The one substantive caveat is that the reach-reward treatment in Section 3.2 requires graph preservation (Remark 1). This is a genuine scope restriction, and the paper later acknowledges it: 'Adaptation to reachability objectives, such as the reach-reward maximization we consider, is usually straightforward, provided the graph preservation property of Remark 1 is met.' That is a correctness and scope concern, not circularity: the algorithm's assumptions are stated, albeit not repeated at every equation, and no fitted parameter or quantity defined in terms of the target result is presented as a prediction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

This survey introduces no free parameters and no invented entities. Its technical claims rest on established results it cites (Bellman optimality, Iyengar's static/dynamic equivalence, Wiesemann et al.'s complexity analysis) and on two structural assumptions it makes explicit: (s,a)-rectangularity of the uncertainty set for the dynamic programming tutorial, and graph preservation for reach-reward objectives. These assumptions limit the scope but are stated in the text.

assumptions (4)

standard math Bellman optimality: the optimal value function is the unique least fixed point of the Bellman equation, and stationary deterministic policies suffice for reach-reward MDPs.
Used throughout Section 2.2 and Equation (1); standard results from Puterman [99] and Baier & Katoen [14].
domain assumption (s,a)-rectangularity: the uncertainty set factors into independent sets per state-action pair.
Section 3.2, Equation (4) replaces the global infimum by a local one; without this, robust value iteration is not valid and policy evaluation can become NP-hard (Table 1).
domain assumption Graph preservation: every transition function in the uncertainty set has the same support.
Remark 1 in Section 3.2 states this is assumed for reach-reward preprocessing; Definition 5 (IMDP) also enforces it. Non-graph-preserving sets are excluded.
domain assumption Static and dynamic uncertainty semantics coincide for (s,a)-rectangular RMDPs under stationary policies.
Lemma 1 in Section 3.1, attributed to Iyengar [64]; the survey treats this as a known theorem and relies on it when discussing semantics.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet." pith.science (2026). https://pith.science/paper/WTTYBBAM

@misc{pith2026241111451,
  author       = {Pith},
  title        = {Pith review of: Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WTTYBBAM}},
  note         = {Machine review of arXiv:2411.11451}
}

read the original abstract

Markov decision processes (MDPs) are a standard model for sequential decision-making problems and are widely used across many scientific areas, including formal methods and artificial intelligence (AI). MDPs do, however, come with the restrictive assumption that the transition probabilities need to be precisely known. Robust MDPs (RMDPs) overcome this assumption by instead defining the transition probabilities to belong to some uncertainty set. We present a gentle survey on RMDPs, providing a tutorial covering their fundamentals. In particular, we discuss RMDP semantics and how to solve them by extending standard MDP methods such as value iteration and policy iteration. We also discuss how RMDPs relate to other models and how they are used in several contexts, including reinforcement learning and abstraction techniques. We conclude with some challenges for future work on RMDPs.

Figures

Figures reproduced from arXiv: 2411.11451 by the authors.

**Figure 1.** An MDP and RMDP for Example 1. The agent can choose between action a and b in state s0 and has singleton choices in the other states. An adversary, nature, chooses variable assignments for x0a0, x0a1, x0b1, x0b2, x2a0, and x2a2. As mentioned above, the restriction that each state-action pair is assigned a valid probability distribution is implied by the definition of the uncertain transition function P. We can there… view at source ↗

**Figure 2.** An RMDP for Example 3. last-action observability does influence the optimal policy and value, as demonstrated by Example 3. The question of last-action observability corresponds to the difference between agent first and nature first semantics in [17]. Example 3 (Last-action observability) [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗

**Figure 3.** An example IMDP. 3.3 Well-Known RMDP Instances We review common types of RMDPs often used in formal verification and AI, namely interval MDPs, L1-MDPs, and multi-environment MDPs. We provide a more commonly used tuple definition for each and explain how it fits the general RMDP framework. Interval MDPs Interval MDPs (IMDPs) [93], also referred to as bounded-parameter MDPs [46] or uncertain MDPs [111, 119], are a spe… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

122 extracted references · 72 canonical work pages

[95]

CoRR abs/2305.10546 (2024)

Ou, W., Bi, S.: Sequential decision-making under uncert ainty: A robust mdps review. CoRR abs/2305.10546 (2024)

arXiv 2024
[1]

Automatica 44(11), 2724 – 2734 (2008)

Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabi listic reachability and safety for controlled discrete time stochastic hybrid syst ems. Automatica 44(11), 2724 – 2734 (2008)

2008
[2]

Proceedings of the IEEE 88(7), 971–984 (2000)

Alur, R., Henzinger, T.A., Laﬀerriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88(7), 971–984 (2000)

2000
[3]

In: IBERAMIA

Andrés, I., de Barros, L.N., Mauá, D.D., Simão, T.D.: When a robot reaches out for human help. In: IBERAMIA. Lecture Notes in Computer Scie nce, vol. 11238, pp. 277–289. Springer (2018)

2018
[4]

Tools at the Frontiers of Quantitative Verification

Andriushchenko, R., Bork, A., Budde, C.E., Ceska, M., Gro ver, K., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Jung es, S., Köhl, M.A., Könighofer, B., Kretínský, J., Meggendorfer, T., Parker, D ., Pranger, S., Quat- mann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative veriﬁc...

work page Pith review arXiv 2024
[5]

In: QEST

Arming, S., Bartocci, E., Chatterjee, K., Katoen, J., Sok olova, A.: Parameter- independent strategies for pmdps via pomdps. In: QEST. Lect ure Notes in Com- puter Science, vol. 11024, pp. 53–70. Springer (2018)

2018
[6]

In: CA V (1)

Ashok, P., Kretínský, J., Weininger, M.: PAC statistical model checking for markov decision processes and stochastic games. In: CA V (1) . Lecture Notes in Computer Science, vol. 11561, pp. 497–519. Springer (2019)

2019
[7]

Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Kat oen, J., Topcu, U.: Scenario-based veriﬁcation of uncertain parametric mdps. Int. J. Softw. Tools Technol. Transf. 24(5), 803–819 (2022)

2022

Show all 122 references

[8]

In: CA V (2)

Badings, T.S., Jansen, N., Junges, S., Stoelinga, M., Vol k, M.: Sampling-based veriﬁcation of ctmcs with uncertain rates. In: CA V (2). Lect ure Notes in Computer Science, vol. 13372, pp. 26–47. Springer (2022)

2022
[9]

In: AAAI

Badings, T.S., Romao, L., Abate, A., Jansen, N.: Probabil ities are not enough: Formal controller synthesis for stochastic dynamical mode ls with epistemic un- certainty. In: AAAI. pp. 14701–14710. AAAI Press (2023)

2023
[10]

Badings, T.S., Romao, L., Abate, A., Parker, D., Poonawa la, H.A., Stoelinga, M., Jansen, N.: Robust control for dynamical systems with no n-gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341–391 (2023)

2023
[11]

Badings, T.S., Simão, T.D., Suilen, M., Jansen, N.: Deci sion-making under uncer- tainty: beyond probabilities. Int. J. Softw. Tools Technol . Transf. 25(3), 375–391 (2023)

2023
[12]

In: FoSSaCS

Baier, C., Bertrand, N., Größer, M.: On decision problem s for probabilistic büchi automata. In: FoSSaCS. Lecture Notes in Computer Science, v ol. 4962, pp. 287–
[13]

In: Computing and Software Science, Lecture Notes in Comput er Science, vol

Baier, C., Hermanns, H., Katoen, J.: The 10, 000 facets of MDP model checking. In: Computing and Software Science, Lecture Notes in Comput er Science, vol. 10000, pp. 420–451. Springer (2019)

2019
[14]

MIT Press (2008)

Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)

2008
[15]

In: CA V (1)

Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderl ich, S.: Ensuring the reli- ability of your model checker: Interval iteration for marko v decision processes. In: CA V (1). Lecture Notes in Computer Science, vol. 10426, pp. 1 60–180. Springer (2017)

2017
[16]

In: NeurIPS

Behzadian, B., Petrik, M., Ho, C.P.: Fast algorithms for l∞-constrained s- rectangular robust mdps. In: NeurIPS. pp. 25982–25992 (202 1) 24 M. Suilen et al
[17]

CoRR abs/2405.04941 (2024)

Bovy, E.M., Suilen, M., Junges, S., Jansen, N.: Imprecis e probabilities meet par- tial observability: Game semantics for robust pomdps. CoRR abs/2405.04941 (2024)

2024 arXiv
[18]

In: ATV A

Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kr etínský, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Veriﬁcation of markov decision p rocesses using learn- ing algorithms. In: ATV A. Lecture Notes in Computer Science , vol. 8837, pp. 98–114. Springer (2014)

2014
[19]

Campi, M.C., Carè, A., Garatti, S.: The scenario approac h: A tool at the service of data-driven decision making. Annu. Rev. Control. 52, 1–17 (2021)

2021
[20]

Campi, M.C., Garatti, S.: The exact feasibility of rando mized solutions of uncer- tain convex programs. SIAM J. Optim. 19(3), 1211–1230 (2008)

2008
[21]

In: TACAS (2)

Cauchi, N., Abate, A.: Stochy: Automated veriﬁcation an d synthesis of stochastic processes. In: TACAS (2). Lecture Notes in Computer Science , vol. 11428, pp. 247–264. Springer (2019)

2019
[22]

Chamie, M.E., Mostafa, H.: Robust action selection in pa rtially observable markov decision processes with model uncertainty. In: CDC. pp. 558 6–5591. IEEE (2018)

2018
[23]

, Royer, A.: Multiple- environment markov decision processes: Eﬃcient analysis a nd applications

Chatterjee, K., Chmelík, M., Karkhanis, D., Novotný, P. , Royer, A.: Multiple- environment markov decision processes: Eﬃcient analysis a nd applications. In: ICAPS. pp. 48–56. AAAI Press (2020)

2020
[24]

In: MFCS

Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitativ e analysis of partially- observable markov decision processes. In: MFCS. Lecture No tes in Computer Science, vol. 6281, pp. 258–269. Springer (2010)

2010
[25]

CoRR abs/2312.13912 (2023)

Chatterjee, K., Goharshady, E.K., Karrabi, M., Novotný , P., Zikelic, D.: Solving long-run average reward robust mdps via stochastic games. CoRR abs/2312.13912 (2023)

2023 arXiv
[26]

Chen, T., Han, T., Kwiatkowska, M.Z.: On the complexity o f model checking interval-valued discrete time markov chains. Inf. Process . Lett. 113(7), 210–216 (2013)

2013
[27]

In: LASER Summer School

Clarke, E.M., Klieber, W., Novácek, M., Zuliani, P.: Mod el checking and the state explosion problem. In: LASER Summer School. Lecture N otes in Computer Science, vol. 7682, pp. 1–30. Springer (2011)

2011
[28]

CoRR abs/2404.08344 (2024)

Coppola, R., Peruﬀo, A., Romao, L., Abate, A., Jr., M.M.: Data-driven interval MDP for robust control synthesis. CoRR abs/2404.08344 (2024)

2024 arXiv
[29]

In: AAAI

Costen, C., Rigter, M., Lacerda, B., Hawes, N.: Planning with hidden parameter polynomial mdps. In: AAAI. pp. 11963–11971. AAAI Press (202 3)
[30]

In: TACAS (2)

Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Papus ha, I., Poonawala, H.A., Topcu, U.: Sequential convex programming for the eﬃcient ve riﬁcation of para- metric mdps. In: TACAS (2). Lecture Notes in Computer Scienc e, vol. 10206, pp. 133–150 (2017)

2017
[31]

In: ATV A

Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu , U.: Synthesis in pmdps: A tale of 1001 parameters. In: ATV A. Lecture Notes in Compute r Science, vol. 11138, pp. 160–176. Springer (2018)

2018
[32]

In: TACAS (1)

Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu , U.: Scenario-based ver- iﬁcation of uncertain mdps. In: TACAS (1). Lecture Notes in C omputer Science, vol. 12078, pp. 287–305. Springer (2020)

2020
[33]

IEEE Trans

Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu , U.: Convex optimiza- tion for parameter synthesis in mdps. IEEE Trans. Autom. Con trol. 67(12), 6333– 6348 (2022)

2022
[34]

In: AAA I

Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suil en, M., Topcu, U.: Ro- bust ﬁnite-state controllers for uncertain pomdps. In: AAA I. pp. 11792–11800. AAAI Press (2021) Robust MDPs: A Place Where AI and Formal Methods Meet 25

2021
[35]

In: TACAS

Daca, P., Henzinger, T.A., Kretínský, J., Petrov, T.: Fa ster statistical model checking for unbounded temporal properties. In: TACAS. Lec ture Notes in Com- puter Science, vol. 9636, pp. 112–129. Springer (2016)

2016
[36]

In: CA V (1)

Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk , M., Bruintjes, H., Katoen, J., Ábrahám, E.: Prophesy: A probabilistic parameter synth esis tool. In: CA V (1). Lecture Notes in Computer Science, vol. 9206, pp. 214–231. S pringer (2015)

2015
[37]

In: MBMV

Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk , M., Katoen, J., Ábrahám, E., Bruintjes, H.: Parameter synthesis for probabilistic s ystems. In: MBMV. pp. 72–74. Albert-Ludwigs-Universität Freiburg (2016)

2016
[38]

Dynamic Games and A pplications (2023)

Delage, A., Buﬀet, O., Dibangoye, J.S., Saﬃdine, A.: HSV I can solve zero-sum partially observable stochastic games. Dynamic Games and A pplications (2023)

2023
[39]

In: SPIN

Fecher, H., Leucker, M., Wolf, V.: Don ’t Know in probabilistic systems. In: SPIN. Lecture Notes in Computer Science, vol. 3925, pp. 71–88. Spr inger (2006)

2006
[41]

In: Bernardo, M., Is sarny, V

Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Aut omated veriﬁcation techniques for probabilistic systems. In: Bernardo, M., Is sarny, V. (eds.) Formal Methods for Eternal Networked Software Systems (SFM’11). L NCS, vol. 6659, pp. 53–113. Springer (2011)

2011
[42]

In: AAAI

Gadot, U., Derman, E., Kumar, N., Elfatihi, M.M., Levy, K ., Mannor, S.: Solving non-rectangular reward-robust mdps via frequency regular ization. In: AAAI. pp. 21090–21098. AAAI Press (2024)

2024
[43]

CoRR abs/2408.08770 (2024)

Galesloot, M.F.L., Suilen, M., Simão, T.D., Carr, S., Sp aan, M.T.J., Topcu, U., Jansen, N.: Pessimistic iterative planning for robust p omdps. CoRR abs/2408.08770 (2024)

2024 arXiv
[44]

In: NIPS

Ghavamzadeh, M., Petrik, M., Chow, Y.: Safe policy impro vement by minimizing robust baseline regret. In: NIPS. pp. 2298–2306 (2016)

2016
[45]

IEEE Trans

Girard, A., Pappas, G.J.: Approximation metrics for dis crete and continuous sys- tems. IEEE Trans. Autom. Control. 52(5), 782–798 (2007)

2007
[46]

Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter m arkov decision pro- cesses. Artif. Intell. 122(1-2), 71–109 (2000)

2000
[47]

Goyal, V., Grand-Clément, J.: Robust markov decision pr ocesses: Beyond rectan- gularity. Math. Oper. Res. 48(1), 203–226 (2023)

2023
[48]

In: Neur IPS (2023)

Grand-Clément, J., Petrik, M.: Reducing blackwell and a verage optimality to discounted mdps via the blackwell discount factor. In: Neur IPS (2023)

2023
[49]

CoRR abs/2312.03618 (2023)

Grand-Clément, J., Petrik, M., Vieille, N.: Beyond disc ounted returns: Ro- bust markov decision processes with average and blackwell o ptimality. CoRR abs/2312.03618 (2023)

2023 arXiv
[50]

In: NIPS

Guez, A., Silver, D., Dayan, P.: Eﬃcient bayes-adaptive reinforcement learning using sample-based search. In: NIPS. pp. 1034–1042 (2012)

2012
[51]

Haddad, S., Monmege, B.: Reachability in mdps: Reﬁning c onvergence of value iteration. In: RP. Lecture Notes in Computer Science, vol. 8 762, pp. 125–137. Springer (2014)

2014
[52]

Formal Aspects Comput

Hansson, H., Jonsson, B.: A logic for reasoning about tim e and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)

1994
[53]

In: TACAS (1)

Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: TACAS (1). Lecture Not es in Computer Science, vol. 13993, pp. 469–488. Springer (2023) 26 M. Suilen et al

2023
[54]

In: CA V (2)

Hartmanns, A., Kaminski, B.L.: Optimistic value iterat ion. In: CA V (2). Lecture Notes in Computer Science, vol. 12225, pp. 488–511. Springe r (2020)

2020
[55]

In: Vojnar, T., Zhang, L

Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Rui jters, E.: The quan- titative veriﬁcation benchmark set. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25 th International Conference, TACAS 2019, Held as Part of th...

2019
[56]

In: LATA

Hashemi, V., Hermanns, H., Song, L., Subramani, K., Turr ini, A., Wojciechowski, P.: Compositional bisimulation minimization for interval markov decision pro- cesses. In: LATA. Lecture Notes in Computer Science, vol. 96 18, pp. 114–126. Springer (2016)

2016
[57]

Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M .: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022)

2022
[58]

In: ICML

Ho, C.P., Petrik, M., Wiesemann, W.: Fast bellman update s for robust mdps. In: ICML. Proceedings of Machine Learning Research, vol. 80, pp . 1984–1993. PMLR (2018)

2018
[59]

Ho, C.P., Petrik, M., Wiesemann, W.: Partial policy iter ation for l1-robust markov decision processes. J. Mach. Learn. Res. 22, 275:1–275:46 (2021)

2021
[60]

In: NeurIPS (2022)

Ho, C.P., Petrik, M., Wiesemann, W.: Robust φ -divergence mdps. In: NeurIPS (2022)

2022
[61]

Journal of the American Statistical Association pp

Hoeﬀding, W.: Probability inequalities for sums of boun ded random variables. Journal of the American Statistical Association pp. 13–30 ( 1963)

1963
[62]

Hüllermeier, E., Waegeman, W.: Aleatoric and epistemic uncertainty in machine learning: an introduction to concepts and methods. Mach. Le arn. 110(3), 457–506 (2021)

2021
[63]

Itoh, H., Nakamura, K.: Partially observable markov dec ision processes with im- precise parameters. Artif. Intell. 171(8-9), 453–490 (2007)

2007
[64]

Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257–280 (2005)

2005
[65]

In: ISoLA ( 1)

Jaeger, M., Bacci, G., Bacci, G., Larsen, K.G., Jensen, P .G.: Approximating eu- clidean by imprecise markov decision processes. In: ISoLA ( 1). Lecture Notes in Computer Science, vol. 12476, pp. 275–289. Springer (2020)

2020
[66]

Jaksch, T., Ortner, R., Auer, P.: Near-optimal regret bo unds for reinforcement learning. J. Mach. Learn. Res. 11, 1563–1600 (2010)

2010
[67]

In: Principles of Systems Design

Jansen, N., Junges, S., Katoen, J.: Parameter synthesis in markov models: A gen- tle survey. In: Principles of Systems Design. Lecture Notes in Computer Science, vol. 13660, pp. 407–437. Springer (2022)

2022
[68]

In: Proceedings of the Sixth Annual Symposium on Log ic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18 , 1991

Jonsson, B., Larsen, K.G.: Speciﬁcation and reﬁnement o f probabilistic pro- cesses. In: Proceedings of the Sixth Annual Symposium on Log ic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18 , 1991. pp. 266–

1991
[69]

Formal Methods Syst

Junges, S., Ábrahám, E., Hensel, C., Jansen, N., Katoen, J., Quatmann, T., Volk, M.: Parameter synthesis for markov models: covering the par ameter space. Formal Methods Syst. Des. 62(1), 181–259 (2024)

2024
[70]

Junges, S., Katoen, J., Pérez, G.A., Winkler, T.: The com plexity of reachability in parametric markov decision processes. J. Comput. Syst. Sci . 119, 183–210 (2021) Robust MDPs: A Place Where AI and Formal Methods Meet 27

2021
[71]

Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Plann ing and acting in partially observable stochastic domains. Artif. Intell. 101(1-2), 99–134 (1998)

1998
[72]

In: LICS

Katoen, J.: The probabilistic model checking landscape . In: LICS. pp. 31–45. ACM (2016)

2016
[73]

In: CA V

Katoen, J., Klink, D., Leucker, M., Wolf, V.: Three-valu ed abstraction for continuous-time markov chains. In: CA V. Lecture Notes in Co mputer Science, vol. 4590, pp. 311–324. Springer (2007)

2007
[74]

Katoen, J., Klink, D., Leucker, M., Wolf, V.: Three-valu ed abstraction for prob- abilistic systems. J. Log. Algebraic Methods Program. 81(4), 356–389 (2012)

2012
[75]

Formal Meth- ods Syst

Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-reﬁnement framework for markov decision proc esses. Formal Meth- ods Syst. Des. 36(3), 246–280 (2010)

2010
[76]

INFORMS J

Kaufman, D.L., Schaefer, A.J.: Robust modiﬁed policy it eration. INFORMS J. Comput. 25(3), 396–410 (2013)

2013
[77]

In: NeurIPS (2023)

Kumar, N., Derman, E., Geist, M., Levy, K.Y., Mannor, S.: Policy gradient for rectangular robust markov decision processes. In: NeurIPS (2023)

2023
[78]

In: QEST

Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based a bstraction for markov decision processes. In: QEST. pp. 157–166. IEEE Computer So ciety (2006)

2006
[79]

Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic m odel checking. In: SFM. Lecture Notes in Computer Science, vol. 4486, pp. 220–270. S pringer (2007)

2007
[80]

In: CA V

Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Ve riﬁcation of proba- bilistic real-time systems. In: CA V. Lecture Notes in Compu ter Science, vol. 6806, pp. 585–591. Springer (2011)

2011
[81]

IEEE Trans

Lahijanian, M., Andersson, S.B., Belta, C.: Formal veri ﬁcation and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Cont rol. 60(8), 2031–2045 (2015)

2015
[82]

In: ICML

Laroche, R., Trichelair, P., des Combes, R.T.: Safe poli cy improvement with base- line bootstrapping. In: ICML. Proceedings of Machine Learn ing Research, vol. 97, pp. 3652–3661. PMLR (2019)

2019
[83]

Larsen, K.G., Skou, A.: Bisimulation through probabili stic testing. Inf. Comput. 94(1), 1–28 (1991)

1991
[84]

Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automat ed veriﬁcation and syn- thesis of stochastic hybrid systems: A survey. Autom. 146, 110617 (2022)

2022
[85]

IEEE Control

Lavaei, A., Soudjani, S., Frazzoli, E., Zamani, M.: Cons tructing MDP abstractions using data with formal guarantees. IEEE Control. Syst. Lett . 7, 460–465 (2023)

2023
[86]

In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K ., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N

Legay, A., Delahaye, B., Bensalem, S.: Statistical mode l checking: An overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K ., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Veriﬁca tion - First Inter- national Conference, R V 2010, S...

2010 doi
[87]

Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic plan- ning and related stochastic optimization problems. Artif. Intell. 147(1-2), 5–34 (2003)

2003
[88]

Mannor, S., Simester, D., Sun, P., Tsitsiklis, J.N.: Bia s and variance approxima- tion in value function estimates. Manag. Sci. 53(2), 308–322 (2007)

2007
[89]

Mathiesen, F.B., Lahijanian, M., Laurenti, L.: Interva lmdp.jl: Accelerated value iteration for interval markov decision processes. Tech. Re p. arXiv:2401.04068, arXiv (2024) 28 M. Suilen et al

2024 arXiv
[90]

CoRR abs/2404.05424 (2024)

Meggendorfer, T., Weininger, M., Wienhöft, P.: What are the odds? improving the foundations of statistical model checking. CoRR abs/2404.05424 (2024)

2024 arXiv
[91]

Moos, J., Hansel, K., Abdulsamad, H., Stark, S., Clever, D., Peters, J.: Robust re- inforcement learning: A review of foundations and recent ad vances. Mach. Learn. Knowl. Extr. 4(1), 276–315 (2022)

2022
[92]

Nakao, H., Jiang, R., Shen, S.: Distributionally robust partially observable markov decision process with moment-based ambiguity. SIAM J. Opti m. 31(1), 461–488 (2021)

2021
[93]

Nilim, A., Ghaoui, L.E.: Robust control of markov decisi on processes with uncer- tain transition matrices. Oper. Res. 53(5), 780–798 (2005)

2005
[94]

In: ICML

Osogami, T.: Robust partially observable markov decisi on process. In: ICML. JMLR Workshop and Conference Proceedings, vol. 37, pp. 106– 115. JMLR.org (2015)

2015
[96]

In: FOCS

Pnueli, A.: The temporal logic of programs. In: FOCS. pp. 46–57. IEEE Computer Society (1977)

1977
[97]

In: ICAPS

Ponnambalam, C.T., Oliehoek, F.A., Spaan, M.T.J.: Abst raction-guided policy recovery from expert demonstrations. In: ICAPS. pp. 560–56 8. AAAI Press (2021)

2021
[98]

In: CA V

Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., S eshia, S.A.: Polynomial-time veriﬁcation of PCTL properties of mdps with convex uncertai nties. In: CA V. Lecture Notes in Computer Science, vol. 8044, pp. 527–542. S pringer (2013)

2013
[99]

Wiley Series in Probability and Statistics, Wile y (1994)

Puterman, M.L.: Markov Decision Processes: Discrete St ochastic Dynamic Pro- gramming. Wiley Series in Probability and Statistics, Wile y (1994)

1994
[100]

In: ATV A

Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Kato en, J.: Parameter syn- thesis for markov models: Faster than ever. In: ATV A. Lecture Notes in Computer Science, vol. 9938, pp. 50–67 (2016)

2016
[101]

In: CA V (1)

Quatmann, T., Katoen, J.: Sound value iteration. In: CA V (1). Lecture Notes in Computer Science, vol. 10981, pp. 643–661. Springer (2018)

2018
[102]

In: FSTTCS

Raskin, J., Sankur, O.: Multiple-environment markov d ecision processes. In: FSTTCS. LIPIcs, vol. 29, pp. 531–543. Schloss Dagstuhl - Lei bniz-Zentrum für Informatik (2014)

2014
[103]

CoRR abs/2312.06344 (2023)

Rickard, L., Abate, A., Margellos, K.: Learning robust policies for uncertain para- metric markov decision processes. CoRR abs/2312.06344 (2023)

2023 arXiv
[104]

In: AAAI

Rigter, M., Lacerda, B., Hawes, N.: Minimax regret opti misation for robust plan- ning in uncertain markov decision processes. In: AAAI. pp. 1 1930–11938. AAAI Press (2021)

2021
[105]

In: NeurIPS

Rigter, M., Lacerda, B., Hawes, N.: Risk-averse bayes- adaptive reinforcement learning. In: NeurIPS. pp. 1142–1154 (2021)

2021
[106]

Saghaﬁan, S.: Ambiguous partially observable markov d ecision processes: Struc- tural results and applications. J. Econ. Theory 178, 1–35 (2018)

2018
[107]

In: AAAI

Simão, T.D., Suilen, M., Jansen, N.: Safe policy improv ement for pomdps via ﬁnite-state controllers. In: AAAI. pp. 15109–15117. AAAI P ress (2023)

2023
[108]

Strehl, A.L., Li, L., Littman, M.L.: Reinforcement lea rning in ﬁnite mdps: PAC analysis. J. Mach. Learn. Res. 10, 2413–2444 (2009)

2009
[109]

Strehl, A.L., Littman, M.L.: An analysis of model-base d interval estimation for markov decision processes. J. Comput. Syst. Sci. 74(8), 1309–1331 (2008)

2008
[110]

In: IJCAI

Suilen, M., Jansen, N., Cubuktepe, M., Topcu, U.: Robus t policy synthesis for uncertain pomdps via convex optimization. In: IJCAI. pp. 41 13–4120. ijcai.org (2020) Robust MDPs: A Place Where AI and Formal Methods Meet 29

2020
[111]

In: NeurIPS (2022)

Suilen, M., Simão, T.D., Parker, D., Jansen, N.: Robust anytime learning of markov decision processes. In: NeurIPS (2022)

2022
[112]

CoRR abs/2407.07006 (2024)

Suilen, M., van der Vegt, M., Junges, S.: A pspace algori thm for almost-sure rabin objectives in multi-environment mdps. CoRR abs/2407.07006 (2024)

2024 arXiv
[113]

Adaptive computation and machine learning, MIT Press (1998)

Sutton, R.S., Barto, A.G.: Reinforcement learning - an introduction. Adaptive computation and machine learning, MIT Press (1998)

1998
[114]

In: TACAS (1)

van der Vegt, M., Jansen, N., Junges, S.: Robust almost- sure reachability in multi-environment mdps. In: TACAS (1). Lecture Notes in Com puter Science, vol. 13993, pp. 508–526. Springer (2023)

2023
[115]

In: ICML

Wang, Q., Ho, C.P., Petrik, M.: Policy gradient in robus t mdps with global conver- gence guarantee. In: ICML. Proceedings of Machine Learning Research, vol. 202, pp. 35763–35797. PMLR (2023)

2023
[116]

Hew lett-Packard Labs, Tech

Weissman, T., Ordentlich, E., Seroussi, G., Verdu, S., Weinberger, M.J.: Inequali- ties for the l1 deviation of the empirical distribution. Hew lett-Packard Labs, Tech. Rep (2003)

2003
[117]

In: IJCAI

Wienhöft, P., Suilen, M., Simão, T.D., Dubslaﬀ, C., Bai er, C., Jansen, N.: More for less: Safe policy improvement with stronger performance gu arantees. In: IJCAI. pp. 4406–4415. ijcai.org (2023)

2023
[118]

Wiesemann, W., Kuhn, D., Rustem, B.: Robust markov deci sion processes. Math. Oper. Res. 38(1), 153–183 (2013)

2013
[119]

Wolﬀ, E.M., Topcu, U., Murray, R.M.: Robust control of u ncertain markov deci- sion processes with temporal logic speciﬁcations. In: CDC. pp. 3372–3379. IEEE (2012)

2012
[120]

CoRR abs/2401.03555 (2024)

Wooding, B., Lavaei, A.: Impact: Interval MDP parallel construction for controller synthesis of large-scale stochastic systems. CoRR abs/2401.03555 (2024)

2024 arXiv
[121]

Xu, H., Mannor, S.: Distributionally robust markov dec ision processes. Math. Oper. Res. 37(2), 288–300 (2012)

2012
[122]

In: IJCAI

Yang, C., Littman, M.L., Carbin, M.: On the (in)tractab ility of reinforcement learning for LTL objectives. In: IJCAI. pp. 3650–3658. ijca i.org (2022)

2022
[277]

https://doi.org/10.11 09/LICS.1991.151651, https://doi.org/10.1109/LICS.1991.151651

IEEE Computer Society (1991). https://doi.org/10.11 09/LICS.1991.151651, https://doi.org/10.1109/LICS.1991.151651

1991

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [95]

CoRR abs/2305.10546 (2024)

Ou, W., Bi, S.: Sequential decision-making under uncert ainty: A robust mdps review. CoRR abs/2305.10546 (2024)

arXiv 2024

[2] [1]

Automatica 44(11), 2724 – 2734 (2008)

Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabi listic reachability and safety for controlled discrete time stochastic hybrid syst ems. Automatica 44(11), 2724 – 2734 (2008)

2008

[3] [2]

Proceedings of the IEEE 88(7), 971–984 (2000)

Alur, R., Henzinger, T.A., Laﬀerriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88(7), 971–984 (2000)

2000

[4] [3]

In: IBERAMIA

Andrés, I., de Barros, L.N., Mauá, D.D., Simão, T.D.: When a robot reaches out for human help. In: IBERAMIA. Lecture Notes in Computer Scie nce, vol. 11238, pp. 277–289. Springer (2018)

2018

[5] [4]

Tools at the Frontiers of Quantitative Verification

Andriushchenko, R., Bork, A., Budde, C.E., Ceska, M., Gro ver, K., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Jung es, S., Köhl, M.A., Könighofer, B., Kretínský, J., Meggendorfer, T., Parker, D ., Pranger, S., Quat- mann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative veriﬁc...

work page Pith review arXiv 2024

[6] [5]

In: QEST

Arming, S., Bartocci, E., Chatterjee, K., Katoen, J., Sok olova, A.: Parameter- independent strategies for pmdps via pomdps. In: QEST. Lect ure Notes in Com- puter Science, vol. 11024, pp. 53–70. Springer (2018)

2018

[7] [6]

In: CA V (1)

Ashok, P., Kretínský, J., Weininger, M.: PAC statistical model checking for markov decision processes and stochastic games. In: CA V (1) . Lecture Notes in Computer Science, vol. 11561, pp. 497–519. Springer (2019)

2019

[8] [7]

Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Kat oen, J., Topcu, U.: Scenario-based veriﬁcation of uncertain parametric mdps. Int. J. Softw. Tools Technol. Transf. 24(5), 803–819 (2022)

2022