Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems

Alessandro Abate; Thom Badings

Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems

T0 review · 2 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read A single behavioral relation makes policy synthesis sound for systems with both stochastic noise and nondeterministic disturbances, by alternating probabilistic and adversarial reasoning.

desk verdict Abstract presents a plausible and needed generalization of probabilistic simulation relations to adversarial disturbances, but with no technical content available, soundness is entirely unverified. read the letter →

arxiv 2508.05062 v1 pith:W5DVLMQW submitted 2025-08-07 eess.SY cs.LOcs.SYmath.OC

Thom Badings , Alessandro Abate This is my paper · ORCID

classification eess.SYcs.LOcs.SYmath.OC

keywords probabilisticalternatingsimulationpolicysynthesisstochasticdynamicalsystemsnondeterministicdisturbancesMarkovdecisionprocessesabstractionformalverificationDubinsvehicle

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 tries to establish that a single behavioral relation, the probabilistic alternating simulation, is sound for policy synthesis in stochastic dynamical systems that also face nondeterministic, set-valued disturbances. It extends the classical probabilistic simulation relation, which only handles stochastic uncertainty, to settings where an adversary can choose disturbances. If correct, this means policies computed on a finite-state abstraction of the concrete system remain correct even when both kinds of uncertainty act together. The paper demonstrates the approach by synthesizing a policy for a 4D-state Dubins vehicle.

What carries the argument

The key machinery is the probabilistic alternating simulation relation: a relation between a concrete system and its finite-state abstraction such that, for every stochastic transition of the concrete system, the abstraction can respond with a matching transition that preserves the relation, while an adversary chooses the nondisturbance values. It carries the argument by guaranteeing that any policy meeting the specification on the abstraction also meets it on the concrete system.

What would settle it

Search for a concrete system and a finite abstraction that satisfy the probabilistic alternating simulation relation, yet for which the policy that is optimal on the abstraction achieves a strictly lower reachability probability on the concrete system than the specification requires. If such an example exists, the claimed soundness for policy transfer is false.

Watch

Extended reading notes

Core claim

The paper's central claim is that the probabilistic alternating simulation relation generalizes previously used probabilistic simulation relations, and that it is sound for policy transfer from finite-state abstractions to concrete systems with both stochastic and nondeterministic uncertainty. The relation lets the synthesizer reason probabilistically over stochastic noise, while treating nondeterministic disturbances adversarially. This is achieved by alternating between the two kinds of uncertainty in a single correctness framework.

Load-bearing premise

The concrete system's uncertainty must be cleanly separable into stochastic noise and nondeterministic, set-valued disturbances, and the finite-state abstraction must be a sound over-approximation of the concrete system in the alternating sense.

Editorial extensions

If this is right

Policies synthesized on finite-state Markov decision process abstractions transfer with correctness to concrete systems that have both stochastic noise and nondeterministic disturbances.
The new relation subsumes earlier probabilistic simulation relations, making them special cases and unifying their correctness arguments.
Verification and synthesis can treat stochastic uncertainty probabilistically and adversarial disturbances robustly within one framework, rather than in two separate steps.
The approach applies to systems like the 4D Dubins vehicle, opening a path to formal guarantees for a broader class of robotic and control systems.

Reading between the lines

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

If the relation is as general as claimed, it may also enable compositional synthesis, where large stochastic systems are verified by relating each component to a finite abstraction and then combining the local guarantees.
A testable extension is to compare policies synthesized through this relation against purely robust and purely probabilistic baselines on the same Dubins benchmark, to see where the hybrid approach preserves reachability or safety with less conservatism.
The soundness hinges on the abstraction being an over-approximation in the alternating sense; if a concrete adversarial disturbance choice is missing from the abstraction, the transferred policy could fail, so an explicit construction of such missing-choice cases would sharpen the method's practical boundary.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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

The abstract describes a genuine gap in the abstraction-based synthesis literature: probabilistic simulation relations are not built for systems that are simultaneously stochastic and subject to set-valued nondeterministic disturbances. The idea of an alternating-style relation that treats noise probabilistically and disturbances adversarially is coherent and, as far as the abstract shows, new. The claimed generalization of existing relations is plausible, and the 4D Dubins case study suggests the authors have at least an implementation. Credit where due: the problem is real, the proposed solution is the natural next step, and the authors know the area.

That said, the abstract alone cannot support a verdict. There are no definitions, no theorem statements, no proofs, and no experimental details. The soundness claim is simply asserted. The stress-test concern about quantifier order is worth taking seriously: alternating simulation is turn-based, while in a continuous-time SDE the disturbance and noise evolve simultaneously and are adapted to the same filtration. If the soundness theorem only covers disturbances that are piecewise-constant and fixed at interval start, then policies certified on the finite abstraction may not transfer to a concrete system with rapidly varying, noise-adapted disturbances. The abstract does not state or prove representability of continuous-time disturbance processes by discrete turn-based choices. This is not a fatal flaw as far as we can see; it is an open technical question that any competent referee would ask early.

Also missing is any comparison with the prior relations the authors claim to generalize. Without naming them and showing how the new relation subsumes them, the novelty claim stays at the level of intuition. And the experimental section, as reported, has no baselines or error bars to judge against.

For whom is this paper? For researchers in formal methods for stochastic control who use abstraction-based policy synthesis. If the technical results hold up, it would be a useful contribution. But because every load-bearing element is invisible, I would not cite it yet, and I would not put it on my reading list until a full version is out. Still, the idea is clearly worth refereeing. An editor should send this to peer review rather than desk reject it.

The recommendation is to engage with the full paper when available, and to ask the authors directly about the turn-based vs simultaneous disturbance question and the exact class of disturbance processes covered by the soundness theorem.

Referee Report

2 major / 3 minor

Summary. The manuscript, as available, consists of an abstract-only submission. It proposes a new behavioral relation, the probabilistic alternating simulation, for stochastic dynamical systems that also contain nondeterministic (set-valued) disturbances. The abstract claims that this relation generalizes existing probabilistic simulation relations, that it allows probabilistic reasoning over stochastic noise while adversarial reasoning over nondeterministic disturbances, and that it supports policy synthesis through finite MDP abstractions. A 4D Dubins vehicle case study is mentioned as an experimental demonstration.

Significance. If the claimed result is correct, it would address a real gap in abstraction-based policy synthesis: existing probabilistic simulation relations do not directly handle systems with both stochastic and nondeterministic uncertainty. The proposed alternating-style relation could enable sound policy transfer from finite-state MDP abstractions to a larger class of concrete systems. This is potentially valuable for formal synthesis in robotics and cyber-physical systems. However, because the manuscript is abstract-only, the formal content needed to assess correctness is absent, so the significance cannot be validated from the submitted material.

major comments (2)

[Abstract (entire)] The submission contains no definitions, theorem statements, proofs, or technical sections. The central claim—that the proposed probabilistic alternating simulation is sound for systems with stochastic and nondeterministic disturbances and generalizes existing relations—is asserted in the abstract but not verifiable. Please provide the formal framework: the class of concrete systems, the exact definition of the relation, the soundness theorem, and a proof that the relation is a congruence for policy synthesis.
[Abstract, sentence: 'our relation allows reasoning probabilistically over stochastic uncertainty, while reasoning robust] For continuous-time systems such as the Dubins vehicle, the quantifier order between the nondeterministic disturbance and the stochastic noise is not specified. Alternating simulation is naturally turn-based: at each step the adversary chooses the disturbance either before or after the stochastic transition. The abstract does not state whether the soundness theorem covers all adapted disturbance processes of an SDE or only a restricted class such as piecewise-constant, interval-start choices. This is a load-bearing point: if the latter, synthesized policies may not transfer to concrete systems with rapidly varying or noise-adapted disturbances. Please clarify the admissible disturbance class and, if necessary, state the representability condition explicitly.

minor comments (3)

[Abstract, last sentence] The experimental demonstration is mentioned but no quantitative results, baselines, or error measures are reported. The full paper should include standard experimental details (system parameters, comparison methods, number of runs, and metrics).
[Abstract, first sentence] The term 'probabilistic alternating simulation' is introduced without a formal definition or a reference to a numbered equation. Please define the relation precisely and locate it in the paper.
[Abstract, sentence: 'generalises existing relations used for verification and policy synthesis used in several works'] Please cite the specific existing relations and state the precise sense of generalization (for example, whether the new relation reduces to the old ones when the nondeterministic disturbance set is a singleton).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity found in the abstract-level derivation chain.

full rationale

The available text is the abstract only, so the derivation chain cannot be fully walked. What is visible is a definition-driven contribution: the paper proposes a probabilistic alternating simulation relation that (by stated intent) generalizes existing probabilistic simulation relations, and claims soundness for policy synthesis on finite abstractions. No fitted parameter is renamed as a prediction, no quantity is defined in terms of the quantity it purports to derive, and no load-bearing result is justified solely by a self-citation. The mention that the relation 'generalises existing relations used for verification and policy synthesis used in several works' is a normal literature anchor, not a circular step, and no specific equation or construction is quoted that would exhibit equivalence to inputs. The skeptic's concern about quantifier ordering (whether turn-based alternating choices faithfully represent simultaneous noise and disturbances) is a potential soundness gap or correctness risk, not a circularity of the kind this pass targets—it does not show that the conclusion is identical to the assumptions by definition. Therefore the honest finding is no significant circularity, with score 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

Abstract-only review: the ledger captures only premises visible in the abstract. No free parameters are visible; the case study may contain tuning parameters but they are not described. The axioms are the standard domain assumptions of abstraction-based synthesis: a separable model of stochastic and nondeterministic uncertainty, a sound finite abstraction, and standard MDP/probability semantics. The single invented entity is the relation itself, which is the paper's contribution; it has no external falsifiable handle visible from the abstract, hence independent_evidence is false.

assumptions (3)

domain assumption The concrete system is modeled as a stochastic dynamical system with additional nondeterministic, set-valued disturbances, and these two uncertainty types are separable.
The abstract's intuition that the relation reasons probabilistically over stochastic uncertainty and adversarially over nondeterministic disturbances presupposes a decomposition of uncertainty into these two types in the system model.
domain assumption The finite-state abstraction is a sound over-approximation of the concrete system in the alternating sense, so policies synthesized on the abstraction transfer to the concrete system.
The abstract frames the contribution as extending the classical abstraction-based synthesis approach, which requires the abstraction to faithfully represent all concrete behaviors; without this, the transferred policy guarantee would not hold.
standard math Standard Markov decision process semantics and probability theory underpin the abstraction and the behavioral relation.
The abstract defines the setting through MDPs and probabilistic simulation relations, relying on standard measure-theoretic and game semantics without introducing new mathematics.

invented entities (1)

Probabilistic alternating simulation relation
purpose: A behavioral relation that certifies correctness of policy synthesis for systems with both stochastic and nondeterministic disturbances, combining probabilistic reasoning over noise with adversarial reasoning over disturbances.
The relation is the paper's central new construct. From the abstract alone, its adequacy is argued by a soundness claim (not visible) and a single case study, with no external falsifiable handle such as a released implementation or a prediction testable outside the paper. It is a definitional contribution, not an unexplained postulate.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems." pith.science (2026). https://pith.science/paper/W5DVLMQW

@misc{pith2026250805062,
  author       = {Pith},
  title        = {Pith review of: Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W5DVLMQW}},
  note         = {Machine review of arXiv:2508.05062}
}

read the original abstract

A classical approach to formal policy synthesis in stochastic dynamical systems is to construct a finite-state abstraction, often represented as a Markov decision process (MDP). The correctness of these approaches hinges on a behavioural relation between the dynamical system and its abstraction, such as a probabilistic simulation relation. However, probabilistic simulation relations do not suffice when the system dynamics are, next to being stochastic, also subject to nondeterministic (i.e., set-valued) disturbances. In this work, we extend probabilistic simulation relations to systems with both stochastic and nondeterministic disturbances. Our relation, which is inspired by a notion of alternating simulation, generalises existing relations used for verification and policy synthesis used in several works. Intuitively, our relation allows reasoning probabilistically over stochastic uncertainty, while reasoning robustly (i.e., adversarially) over nondeterministic disturbances. We experimentally demonstrate the applicability of our relations for policy synthesis in a 4D-state Dubins vehicle.

Discussion (0). Continue with ORCID to comment.

Pith tools

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