Scaling Observation-aware Planning in Uncertain Domains

Adrian Zvizdenco; Alberto Lluch Lafuente; Arthur Conrado Veiga Bosquetti; Christoph Matheja

arxiv: 2605.22364 · v1 · pith:AVNLBFV4new · submitted 2026-05-21 · 💻 cs.AI

Scaling Observation-aware Planning in Uncertain Domains

Adrian Zvizdenco , Arthur Conrado Veiga Bosquetti , Alberto Lluch Lafuente , Christoph Matheja This is my paper

Pith reviewed 2026-05-22 05:01 UTC · model grok-4.3

classification 💻 cs.AI

keywords POMDPOptimal Observability ProblemSensor Selection ProblemPositional Observability ProblemPlanning under uncertaintyDecompositionParameter synthesis

0 comments

The pith

Decomposing POMDPs lets solvers handle far larger sensor selection and observability problems in uncertain planning.

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

The paper tackles the engineering problem of selecting which sensors to equip on an agent so that it can complete tasks in partially observable, uncertain settings. It models the choice as the Optimal Observability Problem over POMDPs and isolates two decidable fragments: the Sensor Selection Problem and the Positional Observability Problem. The authors improve an earlier parameter-synthesis technique and introduce a new method that decomposes the POMDP to find useful observation functions. This decomposition scales the solvable instance size by three orders of magnitude and cuts runtime by five orders. A reader should care because it turns a previously intractable design question into a practical computation for larger real-world systems.

Core claim

This work studies (sub-)symbolic techniques to scale solving of decidable fragments of the OOP, namely the Sensor Selection Problem (SSP) and the Positional Observability Problem (POP). Besides improving the original approach based on parameter synthesis, the authors develop a new solving method that identifies sensible observation functions via decomposition of POMDPs, improving performance by 3 and 5 orders of magnitude for instance size and runtime, respectively.

What carries the argument

Decomposition of a POMDP that extracts sensible observation functions while preserving decidability for the SSP and POP fragments of the Optimal Observability Problem.

If this is right

Instances up to three orders of magnitude larger become solvable.
Runtime drops by five orders of magnitude compared with prior parameter synthesis.
Engineers can now explore more sensing configurations while respecting hardware and processing costs.
The same decomposition approach can be applied to both the sensor-selection and positional-observability fragments.
The method stays inside the decidable fragments, so it inherits their formal guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar decomposition ideas might transfer to other POMDP planning problems that involve choosing what to observe.
The scaled solver could be embedded inside a larger automated design loop for robotic platforms with tight sensor budgets.
Empirical tests on navigation or manipulation benchmarks with real sensor noise would show whether the speed-up survives outside synthetic instances.
If the quality preservation holds only approximately, hybrid exact-plus-decomposition pipelines could still be useful.

Load-bearing premise

The decomposition step preserves both decidability and the exact solution quality of the original Sensor Selection and Positional Observability problems.

What would settle it

Running the new decomposition method on a small, previously solved SSP or POP instance and obtaining a different observation function or a strictly worse task-achievement guarantee than the exact parameter-synthesis baseline.

Figures

Figures reproduced from arXiv: 2605.22364 by Adrian Zvizdenco, Alberto Lluch Lafuente, Arthur Conrado Veiga Bosquetti, Christoph Matheja.

**Figure 1.** Figure 1: 3x3 grid world. For a restricted budget, we shall identify which locations provide the most meaningful information to guide the agent. In this case, 2 sensors (e.g. on s2, s5) suffice such that the agent still achieves the optimal expected number of steps. Konsta et al. [19] developed decision procedures for fragments of the OOP problem by reducing it to parameter synthesis for Markov chains (cf. [15]), i… view at source ↗

**Figure 2.** Figure 2: POMDP Mline with obs = {{s0,s4} 7→ o1,{s1,s3} 7→ o2,{s2} 7→ ✓} and underlying MDP Mline for some fixed constant p ∈ [0,1]; the initial states are s0,s1,s3,s4. The @ labels identify the observable locations in the instance. Example 1. Consider a line example involving an agent that is placed at one of the four random locations. The agent needs to reach a goal by moving to the ℓ(eft) or r(ight). Whenever it… view at source ↗

**Figure 3.** Figure 3: Observation tpMC for the MDP Mline in [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

**Figure 4.** Figure 4: Location tpMC for the location POMDP in Figure 2 with [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗

**Figure 5.** Figure 5: Simplified location tpMC DM for the location POMDP M = Mline⟨obs⟩ in Figure 4, where obs(s0) = @s0,obs(s3) = @s3,obs(s1) = obs(s4) = ⊥. 4.2 PMC Tools as Oracles Another orthogonal approach integrated probabilistic model checking (PMC) tools as symbolic alternatives to the SMT-based oracle (cf. Section 4.1). Rather than computing feasible rewards under a threshold τ as in the SMT checker, these approaches … view at source ↗

**Figure 6.** Figure 6: 3x3 grid world M and G(M). Note that in Example 7, the minimal positional budget B ∗ M (cf. Definition 5) is 2. We can transform obsG into an optimal observation function obs′ : SM → O ′ ✓ with |O ′ | = B ∗ M by combining o1 and o2 into o1,2 = o1 ∪o2. An optimal positional observation-based strategy for the POMDP M⟨obs′ ⟩ assigns down for o1,2 and right for o3. Informally, the transformed observation func… view at source ↗

**Figure 7.** Figure 7: Resulting 3 partitions for S(3,2) for the 3x3 grid world M. States marked in gray belong to the same partition block. eq(obs) = ∑ o∈O eq(o), where eq(o) = ( 1, if T s∈obs−1 (o) α ∗ (s) ̸= /0 0, otherwise. Finally, for every partition, the POMDP generated by the encoded observation function is evaluated using the SMT oracle introduced in Section 4.1 together with the inferred strategy constraints asserted… view at source ↗

**Figure 8.** Figure 8: 4x3 grid. Although S(n,k) grows super-exponentially in n, we are limited to 966 POMDP evaluations in the (Line, Maze, Grid) instances benchmarked. Line instances only have 2 actions {left,right} and there is a single optimal action per state in the encoding MDP; it follows that S(2,k) = 1. Similarly for Maze instances, which have 4 actions. Then, S(4,k) ≤ 7 [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗

**Figure 9.** Figure 9: Time to verify successful benchmark instances for various reorderings of con [PITH_FULL_IMAGE:figures/full_fig_p024_9.png] view at source ↗

**Figure 10.** Figure 10: Maze from [21] [PITH_FULL_IMAGE:figures/full_fig_p026_10.png] view at source ↗

**Figure 11.** Figure 11: For B ≥ 3, it is trivial to see that either activating sensors {@s0,@s1,@s2} or {@s4,@s5,@s6} achieves optimal minimal expected reward of 2. However, uncertainty rises for a lower budget, e.g., B = 2. Should one sensor be placed on each side of the goal, or should both be placed on the same side? If so, should they be side-byside or spread away from each other? Can the expected reward be lower if the sen… view at source ↗

**Figure 12.** Figure 12: Observation function with lowest minimal expected reward for [PITH_FULL_IMAGE:figures/full_fig_p028_12.png] view at source ↗

**Figure 13.** Figure 13: MDP Mtrap. Consider Mtrap in [PITH_FULL_IMAGE:figures/full_fig_p029_13.png] view at source ↗

read the original abstract

Deciding which sensing capabilities to deploy on an agent in uncertain domains is a fundamental engineering challenge, in which one balances task achievability against the high costs of hardware and processing. This problem has previously been formalized as the Optimal Observability Problem (OOP), based on the well-known Partially Observable Markov Decision Process (POMDP) model for decision-making. This work studies (sub-)symbolic techniques to scale solving of decidable fragments of the OOP, namely the Sensor Selection Problem (SSP) and the Positional Observability Problem (POP). Besides improving the original approach based on parameter synthesis, we develop a new solving method that identifies sensible observation functions via decomposition of POMDPs, improving performance by 3 and 5 orders of magnitude for instance size and runtime, respectively.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Decomposition scales sensor selection in POMDPs but needs explicit check that it solves the same problem as the original formulation.

read the letter

This paper's main point is a decomposition technique that breaks POMDPs into subproblems to find observation functions for the Sensor Selection and Positional Observability fragments, delivering reported gains of three orders of magnitude in instance size and five in runtime over parameter synthesis. That is the concrete advance worth noting first. The method moves past the earlier synthesis approach by directly identifying sensible observations through the split, which targets a real engineering tradeoff between sensing cost and task success in uncertain settings. If the experiments in the full paper use standard POMDP benchmarks and show the gains hold without hidden relaxations, this would be a useful practical step for robotics and planning work. The authors position it as independent of prior parameter methods, which keeps the circularity burden low. The soft spot is the equivalence question. The abstract does not include an equation or section that proves the decomposed subproblems return observation functions whose feasibility or optimality status matches what the full Optimal Observability Problem would produce on the same input. Without that check, the speedups could reflect a weaker surrogate rather than a strict improvement on the decidable fragments. I would look for a soundness argument or side-by-side verification in the body before treating the numbers as directly comparable. Minor gaps like missing benchmark tables or error analysis in the abstract are secondary if the full version supplies them. This work is aimed at readers who build or scale POMDP solvers and need better ways to choose observations under cost constraints. Someone working on agent design in partially observable domains would get usable ideas here. It deserves a serious referee because the scaling claim is specific and the underlying problem is well-motivated, even if the equivalence detail requires verification. I would send it to peer review rather than desk reject.

Referee Report

1 major / 1 minor

Summary. The manuscript develops a decomposition-based solving method for identifying sensible observation functions in decidable fragments of the Optimal Observability Problem (OOP) for POMDPs, specifically the Sensor Selection Problem (SSP) and Positional Observability Problem (POP). It reports that this approach improves upon prior parameter-synthesis techniques by three orders of magnitude in solvable instance size and five orders of magnitude in runtime.

Significance. If the decomposition is shown to preserve solution quality and feasibility status for the SSP and POP fragments, the result would enable substantially larger observation-aware planning instances in uncertain domains and constitute a meaningful engineering advance.

major comments (1)

[Decomposition method (method section)] The manuscript describes the POMDP decomposition for SSP and POP but supplies no theorem, lemma, or formal argument establishing that the observation functions returned by the decomposed subproblems are equivalent (sound and complete) to those of the original OOP formulation on the same input. This equivalence is load-bearing for the central performance claim, because without it the reported speed-ups could be achieved by solving a strictly weaker decision problem.

minor comments (1)

[Abstract] The abstract states that the new method 'improves the original approach based on parameter synthesis' without citing the specific prior work or section that defines that baseline.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying this important gap in the presentation of the decomposition method. We address the major comment below.

read point-by-point responses

Referee: The manuscript describes the POMDP decomposition for SSP and POP but supplies no theorem, lemma, or formal argument establishing that the observation functions returned by the decomposed subproblems are equivalent (sound and complete) to those of the original OOP formulation on the same input. This equivalence is load-bearing for the central performance claim, because without it the reported speed-ups could be achieved by solving a strictly weaker decision problem.

Authors: We agree with the referee that an explicit formal argument is required to establish that the decomposed subproblems for SSP and POP return observation functions that are sound and complete with respect to the original OOP formulation. The current manuscript describes the decomposition procedure and reports empirical speed-ups but does not include a dedicated theorem or proof of equivalence. In the revised version we will insert a new subsection in the method section containing (i) a formal statement of the equivalence theorem for both SSP and POP and (ii) a proof sketch showing that any observation function returned by the decomposed procedure satisfies the original constraints and that every feasible solution of the original problem is recovered by the decomposition. This addition will directly address the concern that the reported performance gains might apply only to a weaker problem. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected; derivation is self-contained

full rationale

The paper claims a new decomposition-based solving method for SSP and POP fragments of the OOP in POMDPs, with reported performance gains over parameter synthesis. The abstract and context provide no equations, self-definitions, or self-citations that reduce the central result (decomposition identifying sensible observation functions) to its inputs by construction. No fitted parameters are renamed as predictions, and no uniqueness theorems or ansatzes are smuggled via self-citation. The equivalence of the decomposition to the original problem is presented as a methodological assumption rather than a tautological redefinition. This is the expected non-finding for a paper whose core contribution is an algorithmic technique without self-referential reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the standard POMDP framework and the assumption that its decidable fragments remain tractable under decomposition.

axioms (1)

domain assumption POMDP model for decision-making under uncertainty
The work builds directly on the established Partially Observable Markov Decision Process formalism.

pith-pipeline@v0.9.0 · 5668 in / 1025 out tokens · 50205 ms · 2026-05-22T05:01:37.749582+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

develop a new solving method that identifies sensible observation functions via decomposition of POMDPs... atomic distinguishability groups... strong/weak action equivalence... AG algorithm over S(n,k) partitions
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

typed parametric Markov chains... feasibility problem for tpMCs... ETR-complete

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages · 2 internal anchors

[1]

Amrollahi, D., Preiner, M., Niemetz, A., Reynolds, A., Charikar, M., Tinelli, C., Barrett, C.: Towards SMT Solver Stability via Input Normalization (2025), https://arxiv.org/abs/ 2410.22419

work page arXiv 2025
[2]

Andriushchenko, R., ˇCeˇska, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for pomdps (2022), https://arxiv.org/abs/2203.10803

work page arXiv 2022
[3]

In: Silva, A., Leino, K.R.M

Andriushchenko, R., ˇCeˇska, M., Junges, S., Katoen, J.P., Stupinsk ´y, ˇS.: Paynt: A tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 856–869. Springer International Publishing, Cham (2021)

work page 2021
[4]

MIT press (2008)

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

work page 2008
[5]

CoRRabs/2201.08772(2022), https://arxiv.org/abs/2201.08772

Bork, A., Katoen, J., Quatmann, T.: Under-approximating expected total rewards in pomdps. CoRRabs/2201.08772(2022), https://arxiv.org/abs/2201.08772

work page arXiv 2022
[6]

In: STOC

Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC. pp. 460–

work page
[7]

In: Proceedings of the International Conference on Automated Planning and Scheduling

Chatterjee, K., Chmelik, M., Topcu, U.: Sensor synthesis for POMDPs with reachability objectives. In: Proceedings of the International Conference on Automated Planning and Scheduling. vol. 28, pp. 47–55 (2018)

work page 2018
[8]

In: Proceedings of the 26th Symposium on Operating Systems Principles

Ferraiuolo, A., Baumann, A., Hawblitzel, C., Parno, B.: Komodo: Using verification to dis- entangle secure-enclave hardware from software. In: Proceedings of the 26th Symposium on Operating Systems Principles. pp. 287–305 (2017), https://people.ece.cornell.edu/af433/ pdf/ferraiuolo-sosp-17.pdf

work page 2017
[9]

In: USENIX Symposium on Operating Systems Design and Implementation (OSDI)

Hawblitzel, C., Howell, J., Lorch, J., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: End-to-end security via automated full-system verification. In: USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX - Advanced Com- puting Systems Association (October 2014), https://www.microsoft.com/en-us/research/ publication/ir...

work page 2014
[10]

Heck, L., Mac ´ak, F., ˇCeˇska, M., Junges, S.: Constrained and robust policy synthesis with satisfiability-modulo-probabilistic-model-checking (2025), https://arxiv.org/abs/2511.08078

work page arXiv 2025
[11]

Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.P.: Gradient-descent for randomized controllers under partial observability (2021), https://arxiv.org/abs/2111.04407

work page arXiv 2021
[12]

International Journal on Software Tools for Technology Transfer24(4), 589–610 (Aug 2022)

Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., V olk, M.: The probabilistic model checker storm. International Journal on Software Tools for Technology Transfer24(4), 589–610 (Aug 2022). https://doi.org/10.1007/s10009-021-00633-z, https://doi.org/10.1007/s10009- 021-00633-z

work page doi:10.1007/s10009-021-00633-z 2022
[13]

Principles of Systems Design: Essays Dedicated to Thomas A

Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis in Markov models: A gentle survey. Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday pp. 407–437 (2022)

work page 2022
[14]

In: STAF (Co-Located Events)

Jdeed, M., Schranz, M., Bagnato, A., Suleri, S., Prato, G., Conzon, D., Sende, M., Brosse, E., Pastrone, C., Elmenreich, W.: The cpswarm technology for designing swarms of cyber- physical systems. In: STAF (Co-Located Events). CEUR Workshop Proceedings, vol. 2405, pp. 85–90. CEUR-WS.org (2019)

work page 2019
[15]

Junges, S.: Parameter synthesis in Markov models. Ph.D. thesis, Dissertation, RWTH Aachen University, 2020 (2020)

work page 2020
[16]

CONCLUSION & DISCUSSION 23

work page
[17]

Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Permissive finite-state controllers of pomdps using parameter synthesis (2018), https: //arxiv.org/abs/1710.10294

work page internal anchor Pith review Pith/arXiv arXiv 2018
[18]

Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization (2017), https://arxiv.org/ abs/1412.6980

work page internal anchor Pith review Pith/arXiv arXiv 2017
[19]

Konsta, A.M.: Synthesis and Optimal Observability for Attack Trees. Ph.D. thesis, Technical University of Denmark (2025)

work page 2025
[20]

(eds.) Computer Aided Verification

Konsta, A.M., Lluch Lafuente, A., Matheja, C.: What Should Be Observed for Optimal Re- ward in POMDPs? In: Gurfinkel, A., Ganesh, V . (eds.) Computer Aided Verification. pp. 373–394. Springer Nature Switzerland, Cham (2024)

work page 2024
[21]

In: Prieditis, A., Russell, S

Littman, M.L., Cassandra, A.R., Kaelbling, L.P.: Learning policies for partially observable environments: Scaling up. In: Prieditis, A., Russell, S. (eds.) Ma- chine Learning Proceedings 1995, pp. 362–370. Morgan Kaufmann, San Francisco (CA) (1995). https://doi.org/https://doi.org/10.1016/B978-1-55860-377-6.50052-9, https:// www.sciencedirect.com/science/...

work page doi:10.1016/b978-1-55860-377-6.50052-9 1995
[22]

In: Machine Learning Proceedings 1993, pp

McCallum, R.A.: Overcoming incomplete perception with utile distinction memory. In: Machine Learning Proceedings 1993, pp. 190–196. Morgan Kaufmann, San Francisco (CA) (1993). https://doi.org/https://doi.org/10.1016/B978-1-55860-307-3.50031-9, https:// www.sciencedirect.com/science/article/pii/B9781558603073500319

work page doi:10.1016/b978-1-55860-307-3.50031-9 1993
[23]

In: Tassarotti, J., Zetzsche, S

McLaughlin, S., Jaloyan, G., Xiang, T., Rabe, F.: Enhancing Proof Stability. In: Tassarotti, J., Zetzsche, S. (eds.) Dafny 2024 (2023)

work page 2024
[24]

Wiley Series in Probability and Statistics, Wiley (1994)

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https://doi.org/10.1002/9780470316887, https://doi.org/10.1002/9780470316887

work page doi:10.1002/9780470316887 1994
[25]

https://www.stormchecker.org/documentation/ usage/running-storm-on-parametric-models.html (2024), accessed: 2025-12-29

Storm Maintainers: Storm documentation. https://www.stormchecker.org/documentation/ usage/running-storm-on-parametric-models.html (2024), accessed: 2025-12-29

work page 2024
[26]

COURSERA: Neural Networks for Machine Learning (2012), ac- cessed: 2026-01-14

Tieleman, T., Hinton, G.: Lecture 6.5-rmsprop: Divide the gradient by a running average of its recent magnitude. COURSERA: Neural Networks for Machine Learning (2012), ac- cessed: 2026-01-14

work page 2012
[27]

In: 2023 Formal Methods in Computer- Aided Design (FMCAD)

Zhou, Y ., Bosamiya, J., Takashima, Y ., Li, J., Heule, M., Parno, B.: Mariposa: Measuring smt instability in automated program verification. In: 2023 Formal Methods in Computer- Aided Design (FMCAD). pp. 178–188 (2023). https://doi.org/10.34727/2023/isbn.978-3- 85448-060-0 26

work page doi:10.34727/2023/isbn.978-3- 2023
[28]

Au- tonomous Robots3, 31–48 (1996)

Zilberstein, S.: Resource-bounded sensing and planning in autonomous systems. Au- tonomous Robots3, 31–48 (1996). https://doi.org/10.1007/bf00162466

work page doi:10.1007/bf00162466 1996
[29]

opposite

Zvizdenco, A., Bosquetti, A.C.V .: Scaling Observation-aware Planning in Uncertain Do- mains. Master’s thesis, Technical University of Denmark (2026) 24 Adrian Zvizdenco, Arthur Bosquetti, Alberto Lluch Lafuente, et al. A Appendix: SMT Parameter Synthesis A.1 SMT Constraint Experiments 24 25 26 27 28 29 30 31 32 33 34 350 400 450 500 Instances Solved Cumu...

work page 2026

[1] [1]

Amrollahi, D., Preiner, M., Niemetz, A., Reynolds, A., Charikar, M., Tinelli, C., Barrett, C.: Towards SMT Solver Stability via Input Normalization (2025), https://arxiv.org/abs/ 2410.22419

work page arXiv 2025

[2] [2]

Andriushchenko, R., ˇCeˇska, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for pomdps (2022), https://arxiv.org/abs/2203.10803

work page arXiv 2022

[3] [3]

In: Silva, A., Leino, K.R.M

Andriushchenko, R., ˇCeˇska, M., Junges, S., Katoen, J.P., Stupinsk ´y, ˇS.: Paynt: A tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 856–869. Springer International Publishing, Cham (2021)

work page 2021

[4] [4]

MIT press (2008)

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

work page 2008

[5] [5]

CoRRabs/2201.08772(2022), https://arxiv.org/abs/2201.08772

Bork, A., Katoen, J., Quatmann, T.: Under-approximating expected total rewards in pomdps. CoRRabs/2201.08772(2022), https://arxiv.org/abs/2201.08772

work page arXiv 2022

[6] [6]

In: STOC

Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC. pp. 460–

work page

[7] [7]

In: Proceedings of the International Conference on Automated Planning and Scheduling

Chatterjee, K., Chmelik, M., Topcu, U.: Sensor synthesis for POMDPs with reachability objectives. In: Proceedings of the International Conference on Automated Planning and Scheduling. vol. 28, pp. 47–55 (2018)

work page 2018

[8] [8]

In: Proceedings of the 26th Symposium on Operating Systems Principles

Ferraiuolo, A., Baumann, A., Hawblitzel, C., Parno, B.: Komodo: Using verification to dis- entangle secure-enclave hardware from software. In: Proceedings of the 26th Symposium on Operating Systems Principles. pp. 287–305 (2017), https://people.ece.cornell.edu/af433/ pdf/ferraiuolo-sosp-17.pdf

work page 2017

[9] [9]

In: USENIX Symposium on Operating Systems Design and Implementation (OSDI)

Hawblitzel, C., Howell, J., Lorch, J., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: End-to-end security via automated full-system verification. In: USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX - Advanced Com- puting Systems Association (October 2014), https://www.microsoft.com/en-us/research/ publication/ir...

work page 2014

[10] [10]

Heck, L., Mac ´ak, F., ˇCeˇska, M., Junges, S.: Constrained and robust policy synthesis with satisfiability-modulo-probabilistic-model-checking (2025), https://arxiv.org/abs/2511.08078

work page arXiv 2025

[11] [11]

Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.P.: Gradient-descent for randomized controllers under partial observability (2021), https://arxiv.org/abs/2111.04407

work page arXiv 2021

[12] [12]

International Journal on Software Tools for Technology Transfer24(4), 589–610 (Aug 2022)

Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., V olk, M.: The probabilistic model checker storm. International Journal on Software Tools for Technology Transfer24(4), 589–610 (Aug 2022). https://doi.org/10.1007/s10009-021-00633-z, https://doi.org/10.1007/s10009- 021-00633-z

work page doi:10.1007/s10009-021-00633-z 2022

[13] [13]

Principles of Systems Design: Essays Dedicated to Thomas A

Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis in Markov models: A gentle survey. Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday pp. 407–437 (2022)

work page 2022

[14] [14]

In: STAF (Co-Located Events)

Jdeed, M., Schranz, M., Bagnato, A., Suleri, S., Prato, G., Conzon, D., Sende, M., Brosse, E., Pastrone, C., Elmenreich, W.: The cpswarm technology for designing swarms of cyber- physical systems. In: STAF (Co-Located Events). CEUR Workshop Proceedings, vol. 2405, pp. 85–90. CEUR-WS.org (2019)

work page 2019

[15] [15]

Junges, S.: Parameter synthesis in Markov models. Ph.D. thesis, Dissertation, RWTH Aachen University, 2020 (2020)

work page 2020

[16] [16]

CONCLUSION & DISCUSSION 23

work page

[17] [17]

Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Permissive finite-state controllers of pomdps using parameter synthesis (2018), https: //arxiv.org/abs/1710.10294

work page internal anchor Pith review Pith/arXiv arXiv 2018

[18] [18]

Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization (2017), https://arxiv.org/ abs/1412.6980

work page internal anchor Pith review Pith/arXiv arXiv 2017

[19] [19]

Konsta, A.M.: Synthesis and Optimal Observability for Attack Trees. Ph.D. thesis, Technical University of Denmark (2025)

work page 2025

[20] [20]

(eds.) Computer Aided Verification

Konsta, A.M., Lluch Lafuente, A., Matheja, C.: What Should Be Observed for Optimal Re- ward in POMDPs? In: Gurfinkel, A., Ganesh, V . (eds.) Computer Aided Verification. pp. 373–394. Springer Nature Switzerland, Cham (2024)

work page 2024

[21] [21]

In: Prieditis, A., Russell, S

Littman, M.L., Cassandra, A.R., Kaelbling, L.P.: Learning policies for partially observable environments: Scaling up. In: Prieditis, A., Russell, S. (eds.) Ma- chine Learning Proceedings 1995, pp. 362–370. Morgan Kaufmann, San Francisco (CA) (1995). https://doi.org/https://doi.org/10.1016/B978-1-55860-377-6.50052-9, https:// www.sciencedirect.com/science/...

work page doi:10.1016/b978-1-55860-377-6.50052-9 1995

[22] [22]

In: Machine Learning Proceedings 1993, pp

McCallum, R.A.: Overcoming incomplete perception with utile distinction memory. In: Machine Learning Proceedings 1993, pp. 190–196. Morgan Kaufmann, San Francisco (CA) (1993). https://doi.org/https://doi.org/10.1016/B978-1-55860-307-3.50031-9, https:// www.sciencedirect.com/science/article/pii/B9781558603073500319

work page doi:10.1016/b978-1-55860-307-3.50031-9 1993

[23] [23]

In: Tassarotti, J., Zetzsche, S

McLaughlin, S., Jaloyan, G., Xiang, T., Rabe, F.: Enhancing Proof Stability. In: Tassarotti, J., Zetzsche, S. (eds.) Dafny 2024 (2023)

work page 2024

[24] [24]

Wiley Series in Probability and Statistics, Wiley (1994)

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https://doi.org/10.1002/9780470316887, https://doi.org/10.1002/9780470316887

work page doi:10.1002/9780470316887 1994

[25] [25]

https://www.stormchecker.org/documentation/ usage/running-storm-on-parametric-models.html (2024), accessed: 2025-12-29

Storm Maintainers: Storm documentation. https://www.stormchecker.org/documentation/ usage/running-storm-on-parametric-models.html (2024), accessed: 2025-12-29

work page 2024

[26] [26]

COURSERA: Neural Networks for Machine Learning (2012), ac- cessed: 2026-01-14

Tieleman, T., Hinton, G.: Lecture 6.5-rmsprop: Divide the gradient by a running average of its recent magnitude. COURSERA: Neural Networks for Machine Learning (2012), ac- cessed: 2026-01-14

work page 2012

[27] [27]

In: 2023 Formal Methods in Computer- Aided Design (FMCAD)

Zhou, Y ., Bosamiya, J., Takashima, Y ., Li, J., Heule, M., Parno, B.: Mariposa: Measuring smt instability in automated program verification. In: 2023 Formal Methods in Computer- Aided Design (FMCAD). pp. 178–188 (2023). https://doi.org/10.34727/2023/isbn.978-3- 85448-060-0 26

work page doi:10.34727/2023/isbn.978-3- 2023

[28] [28]

Au- tonomous Robots3, 31–48 (1996)

Zilberstein, S.: Resource-bounded sensing and planning in autonomous systems. Au- tonomous Robots3, 31–48 (1996). https://doi.org/10.1007/bf00162466

work page doi:10.1007/bf00162466 1996

[29] [29]

opposite

Zvizdenco, A., Bosquetti, A.C.V .: Scaling Observation-aware Planning in Uncertain Do- mains. Master’s thesis, Technical University of Denmark (2026) 24 Adrian Zvizdenco, Arthur Bosquetti, Alberto Lluch Lafuente, et al. A Appendix: SMT Parameter Synthesis A.1 SMT Constraint Experiments 24 25 26 27 28 29 30 31 32 33 34 350 400 450 500 Instances Solved Cumu...

work page 2026