Pith. sign in

REVIEW 3 major objections 5 minor 54 references

Compositional Reasoning for Parametric Probabilistic Automata

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Assume-guarantee reasoning is proved sound for parametric probabilistic automata.

desk verdict The paper genuinely extends assume-guarantee reasoning to parametric probabilistic automata, but the partial-strategy semantics is ill-defined as written and the Appendix B reduction does not repair it, so the main rules lack well-formed premises. read the letter →

arxiv 2506.08525 v1 pith:EWJBJSBT submitted 2025-06-10 cs.LO math.PR

Hannah Mertens , Tim Quatmann , Joost-Pieter Katoen This is my paper · ORCID
classification cs.LOmath.PR MSC 68Q60
keywords assume-guaranteereasoningparametricprobabilisticautomatacompositionalverificationmulti-objectivemodelcheckingexpectedtotalrewardsparametersynthesismonotonicitystrategyprojection
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 aims to show that assume-guarantee (AG) reasoning---checking each component of a parallel system separately by assuming facts about the others---remains sound when transition probabilities are polynomials in unknown parameters. The objects are parametric probabilistic automata (pPAs), and the properties covered are multi-objective queries combining probabilistic requirements and (parametric) expected total rewards. If the proof rules are correct, a large composed parametric system can be certified by verifying its components in isolation, sidestepping the exponential state-space explosion of building the full product. The paper also introduces a compositional monotonicity rule: if each component's probability or expected reward is monotone in a parameter, then so is the composed system's, which can make parameter synthesis much cheaper.

What carries the argument

The load-bearing device is the strategy projection, adapted from the non-parametric setting of [35] and originally introduced in [45]. Given a strategy of a composition $M_1 \| M_2$, its projection to $M_i$ is the conditional probability that the next action of $M_i$ is $\alpha_i$, conditioned on observing a path whose projection is the given finite path of $M_i$; Lemma 13 proves that under this projected strategy the component assigns exactly the same measure to projected path sets as the composition does. Alphabet extension $M\langle \Sigma\rangle$ adds self-loop transitions labeled by every outside letter, so that any property over an arbitrary alphabet can be re-expressed over a component; Theorem 30 then states that probabilities and expected rewards of a composition equal those of each component under the projected strategy. Lemma 18, which says the projection to one component is insensitive to the specific parameter instantiation of that component as long as the zero-transition structure is preserved, is what makes the monotonicity rule (Theorem 41) go through.

What would settle it

Enumerate small pPAs with one or two parameters and graph-preserving regions: if any pair of components whose solution functions are monotone in $p$ yields a composed solution function that is not monotone in $p$, Theorem 41 is false. A second, more formal check is to encode the equivalence asserted in Remark 6 and the projection lemma [35, Lemma 3] in a proof assistant and see whether the measure equality used in Theorem 30 holds for the functional presentation with alphabet-extension self-loops.

Watch

Extended reading notes

Core claim

The paper claims to establish the first assume-guarantee framework for parametric Markov models. Its central theorems are sound asymmetric and circular proof rules: for instance, from $M_1, R_1 \models_{\mathrm{cmp}} A_{\mathrm{safe}}$ and $M_2\langle \Sigma_A\rangle, R_2 \models_{\mathrm{prt}} A_{\mathrm{safe}} \to G_{\mathrm{safe}}$ one may conclude $M_1 \| M_2, R_1 \cap R_2 \models_{\mathrm{cmp}} G_{\mathrm{safe}}$, and the fair-strategy version of the same rule is also proved. The same framework extends to conjunctions of multi-objective queries, an asymmetric rule for more than two components, an interleaving rule for non-synchronized actions, and a rule for sums of expected rewards. The new monotonicity rule (Theorem 41) states that if the solution function of each component of a parallel composition is monotone in a parameter, then the solution function of the composition is monotone in that parameter on the intersection of the regions. The load-bearing device is the preservation theorem (Theorem 30): a strategy of the composition and its projection to a component give identical probabilities and expected rewards, which lets each rule transfer queried properties from components to the composed system.

Load-bearing premise

The soundness of every parametric rule reduces, through Theorem 30, to the non-parametric strategy-projection lemma [35, Lemma 3], and the paper assumes without a full proof that this lemma survives the switch to the functional (state-action to distribution) presentation of probabilistic automata, including the self-loops added by alphabet extension.

Editorial extensions

If this is right

  • A composed parametric system can be certified without constructing it: checking $M_1$ against a safe assumption and $M_2\langle \Sigma_A\rangle$ against the corresponding assume-guarantee triple suffices to conclude the guarantee on $M_1 \| M_2$.
  • Multi-objective queries can be handled in one pass, so a verification task can demand several probabilistic and expected-total-reward constraints at once, including conjunctions of safety properties.
  • The monotonicity rule means monotone parameter regions can be certified componentwise, replacing a monolithic, coETR-hard monotonicity check for the whole system with smaller checks on its parts.
  • Fair-strategy versions of the rules compose recursively, yielding an $n$-component asymmetric rule and enabling modular treatment of systems with many components.
  • Interleaving and reward-sum rules decompose systems with non-synchronized actions and split expected total rewards into component contributions.

Reading between the lines

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

  • The paper proves soundness but stops short of an algorithm; the natural next step is to compute the AG triples and projections symbolically as rational functions and use existing parameter-synthesis engines to check the component obligations.
  • If the monotonicity rule is correct, it gives a divide-and-conquer certificate for parameter synthesis: partition the parameter space by componentwise monotonicity, synthesize each component's satisfying region, and intersect, instead of solving one monolithic ETR instance.
  • Because the entire parametric lift rests on the non-parametric projection lemma [35, Lemma 3] via Theorem 30, a proof-assistant check of the translation in Remark 6 (from transition relations to functional presentations) would be a prudent validation before building tooling on top.
  • The framework should be testable on the classic communication-protocol examples with parameters inserted into failure probabilities; such a case study would show whether the componentwise regions are practically tight compared with monolithic verification.
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.

Referee Report

3 major / 5 minor

Summary. The paper proposes an assume-guarantee (AG) framework for compositional reasoning about parametric probabilistic automata (pPA), lifting the PA framework of Kwiatkowska et al. [35] to the parametric setting. It introduces pPAs, develops strategy projections based on conditional probabilities, and presents asymmetric, circular, interleaving, conjunction, reward-sum, and monotonicity proof rules for multi-objective probabilistic and expected-total-reward queries. The central claimed contribution is that soundness of these rules enables verification of a composed pPA by verifying its components, covering safety, general ω-regular properties, rewards, and monotonicity. The appendices contain detailed proofs, including a critical discussion of a safety-prefix issue in [35] and a proposed reduction from partial to complete strategies via a transformed automaton Mτ.

Significance. If the framework were sound, it would be a valuable contribution: compositional verification of parametric probabilistic systems is genuinely motivated by the ETR-hardness of monolithic parameter synthesis, and the extension of AG rules from PAs to pPAs, together with a compositional monotonicity rule, would be novel and useful. The paper is also commendable for shipping detailed appendix proofs, for providing an explicit repair of a technical bug in [35] concerning safety languages over infinite words, and for proving key projection lemmas (Lemmas 12, 13, 18) in the chosen presentation. However, the central technical foundation—the semantics of partial strategies—is inconsistent as written, and the appendix's repair via Mτ is itself flawed. Because the AG rules quantify over partial strategies in their premises (e.g., Theorem 33 and Theorem 35), this issue is load-bearing and must be resolved before the framework can be accepted.

major comments (3)
  1. [Section 2, Definition 4 and the measure construction] The cylinder-set measure Pr^{v,σ}_M is not countably additive for partial strategies. Consider a partial strategy σ with σ(s_init)(α)=0 for all α. Then Cyl(s_init) is the disjoint union of all cylinders Cyl(s_init,α,s'), each assigned measure 0 by the product formula, while Cyl(s_init) itself is assigned measure 1. Hence no probability measure (or even subprobability measure) with these cylinder values exists. Since Definition 20 defines |=prt by quantifying over all σ∈Str^{prt}_M, the satisfaction relation used in the premises of Theorems 33, 35, 51, 52, 53, and 54 is not well-defined. This is not a presentation issue but a fundamental gap in the formal semantics.
  2. [Appendix B, Definition 47 and Lemma 48] The proposed reduction from partial to complete strategies via Mτ does not work as written. In Definition 47, the fresh sink state sτ has no outgoing transitions, so Act(sτ)=∅; a complete strategy on Mτ, whose domain includes all finite paths, cannot be defined on any path reaching sτ. Moreover, the construction of στ in the proof of Lemma 48 assigns, for every π∈Paths_fin^M, both στ(π,α)=σ(π,α) for α∈Act_M and στ(π,τ)=1, so the resulting function is not a probability distribution; and for paths that reach sτ it refers to values σ(π,α) that are undefined because σ is only defined on paths of M. Thus Corollaries 49 and 50, which underpin the intended meaning of partial-strategy quantification, are not established.
  3. [Appendix A.2, proof of Theorems 26 and 30] The proof of Theorem 30 simply states that the claims 'follow by [35, Lemma 3]' after instantiating valuations, but [35, Lemma 3] is formulated for a PA presentation with a transition relation δ⊆S×Σ×Dist(S), whereas this paper uses a functional presentation (P,L) with at most one transition per state-action pair. Remark 6 asserts equivalence of the two formalisms but provides no proof, and the projection construction and Lemmas 12, 13 are developed directly in the functional presentation. Because Theorem 30 is the central link between measures of a composition and measures of its components—used in every AG rule and in the monotonicity proof—the authors should either prove the transfer of [35, Lemma 3] in detail or give a direct proof of Theorem 26/30 from their own Lemmas 12 and 13. As it stands, soundness of the framework rests on an unverified translation.
minor comments (5)
  1. [Section 2, Definition 7] The condition Act_i ∩ (Σ1∪Σ2) = ∅ is surprising because the examples identify actions with labels (e.g., Example 3 says 'the alphabet coincides with actions'); please clarify whether this is a typing condition and how Examples 3 and 8 satisfy it.
  2. [Appendix A.1, proof of Lemma 18] In the proof of Lemma 18, the set 'ˆv1∈{v1, v2}' should presumably be 'ˆv1∈{v1, v′1}' to match the statement of the lemma.
  3. [Section 6, proof of Theorem 41] The chain of equalities in the monotonicity proof uses expressions such as 'sol(M1⟨Σ⟩∥M2⟨Σ⟩[v]),σ(v+)' and '((M1⟨Σ⟩∥M2⟨Σ⟩[v])[v+]'. Since instantiating a composed pPA with two different valuations is delicate, this notation is confusing; please rewrite the argument with explicit instantiations, e.g., (M1⟨Σ⟩[v+]∥M2⟨Σ⟩[v])[].
  4. [Example 34] In Example 34, the largest region for the premise is written first as 'R1 = {...}' and then the region for the second premise is written as 'R = {...}'; the subscript on the second region is missing, which makes the example harder to follow.
  5. [Definition 24 and Appendix D] The fix of the safety-prefix issue relative to [35] is a welcome contribution; consider stating explicitly in the main text (Definition 24) that safety languages include finite words, since the reader otherwise might miss that this is a deliberate deviation from [35].

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the pPA assume-guarantee rules are soundness transfers from an external non-parametric framework, not re-statements of the paper's own assumptions.

full rationale

The paper's derivation chain is self-contained relative to external prior work. The central results, Theorems 33, 35, and 41, are proved by transferring properties along strategy projections, with the key transfer step being Theorem 30, whose proof states: "Then, the claims follow by [35, Lemma 3]." This is an external lemma from Kwiatkowska et al., not from the present authors, and it is not derived from the conclusions being proved. No parameter is fitted to data and then renamed as a prediction; the AG premises are independent user-supplied hypotheses, and the soundness proofs use them only as assumptions. The monotonicity rule is proved by contradiction using Theorem 30 and Lemma 18, and Lemma 18 is proved directly by a cancellation argument rather than by assuming the rule's conclusion. The paper's own Appendix D even identifies and repairs an inconsistency in the external framework, which is independent critical analysis rather than circular reuse. The remaining concern, noted in Remark 6, that the functional PA presentation is asserted to be equivalent to the relational presentation used in [35], is a correctness-transfer risk and not a circularity, because the claim is an expressiveness assertion rather than a definitional identification of the paper's target results with its inputs. Self-citations such as [37,44,48-50] appear in motivational or definitional context and are not load-bearing in the soundness proofs. Therefore no circular step is present.

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

No free parameters appear: no numerical fitting occurs. The axioms are standard domain assumptions for compositional verification of Markov models; the key one is reliance on prior PA projection results in a different formalism. No new physical or logical entities are postulated; all constructs are definitions within the model.

assumptions (2)
  • domain assumption Non-parametric projection lemma [35, Lemma 3] transfers to the functional PA presentation (P, L) used here.
    Theorem 26 and Theorem 30 cite [35, Lemma 3] to conclude that probabilities and expected rewards are preserved under strategy projection in PA. The paper uses a different but claimed-equivalent PA definition, without a detailed transfer proof.
  • domain assumption Regions are well-defined and graph-preserving where strategy classes are compared across valuations.
    Remark 21 and Proposition 10 need graph-preserving regions to swap quantifiers and keep fair-strategy sets constant, e.g., in the monotonicity rule Theorem 41. This is a stated precondition of the rules.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Compositional Reasoning for Parametric Probabilistic Automata." pith.science (2026). https://pith.science/paper/EWJBJSBT

@misc{pith2026250608525,
  author       = {Pith},
  title        = {Pith review of: Compositional Reasoning for Parametric Probabilistic Automata},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EWJBJSBT}},
  note         = {Machine review of arXiv:2506.08525}
}
read the original abstract

We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

54 extracted references · 26 canonical work pages

  1. [35]

    Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

    Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput. , 232:38--65, 2013. URL: https://doi.org/10.1016/j.ic.2013.10.001, https://doi.org/10.1016/J.IC.2013.10.001 doi:10.1016/J.IC.2013.10.001

    work page doi:10.1016/j.ic.2013.10.001 2013

  2. [1]

    Henzinger

    Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods Syst. Des. , 15(1):7--48, 1999. https://doi.org/10.1023/A:1008739929481 doi:10.1023/A:1008739929481

    work page doi:10.1023/a:1008739929481 1999

  3. [2]

    Compositional parameter synthesis

    Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih - Hong Cheng, and Harald Ruess. Compositional parameter synthesis. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings , volume 9995 of Lecture Notes...

    doi:10.1007/978-3-319-48989-6 2016

  4. [3]

    Principles of model checking

    Christel Baier and Joost - Pieter Katoen. Principles of model checking . MIT Press, 2008

    2008

  5. [4]

    Samik Basu and C. R. Ramakrishnan. Compositional analysis for verification of parameterized systems. Theor. Comput. Sci. , 354(2):211--229, 2006. URL: https://doi.org/10.1016/j.tcs.2005.11.016, https://doi.org/10.1016/J.TCS.2005.11.016 doi:10.1016/J.TCS.2005.11.016

    work page doi:10.1016/j.tcs.2005.11.016 2006

  6. [5]

    Toward implicit learning for the compositional verification of M arkov decision processes

    Redouane Bouchekir and Mohand Cherif Boukala. Toward implicit learning for the compositional verification of M arkov decision processes. In Mohamed Faouzi Atig, Saddek Bensalem, Simon Bliudze, and Bruno Monsuez, editors, Verification and Evaluation of Computer and Communication Systems - 12th International Conference, VECoS 2018, Grenoble, France, Septemb...

    doi:10.1007/978-3 2018

  7. [6]

    Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes

    Redouane Bouchekir, Sa \" da Boukhedouma, and Mohand Cherif Boukala. Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes. In Yuri Merkuryev, Tuncer I. \" O ren, and Mohammad S. Obaidat, editors, Proceedings of the 6th International Conference on Simulation and Modeling Methodologies, Technolo...

    work page doi:10.5220/00059786 2016

  8. [7]

    Compositional reverification of probabilistic safety properties for large-scale complex IT systems

    Radu Calinescu, Shinji Kikuchi, and Kenneth Johnson. Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In Radu Calinescu and David Garlan, editors, Large-Scale Complex IT Systems. Development, Operation and Management - 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012, Revised Selected Papers , v...

    work page doi:10.1007/978-3-642-34059-8 2012

Show all 54 references
  1. [8]

    Larsen, and Radu Mardare

    Luca Cardelli, Kim G. Larsen, and Radu Mardare. Modular M arkovian logic. In Luca Aceto, Monika Henzinger, and Jir \' Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II , vo...

    2011 doi

  2. [9]

    Parametric LTL on M arkov chains

    Souymodip Chakraborty and Joost - Pieter Katoen. Parametric LTL on M arkov chains. In Josep D \' az, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceeding...

    2014 doi

  3. [10]

    CEGAR for compositional analysis of qualitative properties in M arkov decision processes

    Krishnendu Chatterjee, Martin Chmelik, and Przemyslaw Daca. CEGAR for compositional analysis of qualitative properties in M arkov decision processes. Formal Methods Syst. Des. , 47(2):230--264, 2015. URL: https://doi.org/10.1007/s10703-015-0235-2, https://doi.org/10.1007/S1070...

    2015 doi

  4. [11]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Pr...

    doi

  5. [12]

    Clarke, David E

    Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989 , pages 353--362. IEEE Computer Society, 1989. https://...

    1989

  6. [13]

    Cobleigh, Dimitra Giannakopoulou, and Corina S

    Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003...

    2003

  7. [14]

    Symbolic and parametric model checking of discrete-time M arkov chains

    Conrado Daws. Symbolic and parametric model checking of discrete-time M arkov chains. In ICTAC , volume 3407 of Lecture Notes in Computer Science , pages 280--294. Springer, 2004. https://doi.org/10.1007/978-3-540-31862-0\_21 doi:10.1007/978-3-540-31862-0\_21

    2004 doi

  8. [15]

    Henzinger, and Ranjit Jhala

    Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings , vo...

    2001 doi

  9. [16]

    Pasareanu, and Sharon Shoham

    Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. Automated circular assume-guarantee reasoning. Formal Aspects Comput. , 30(5):571--595, 2018. URL: https://doi.org/10.1007/s00165-017-0436-0, https://doi.org/10.1007/S00165-017-0436-0 doi:10.1007/S00165-...

    2018 doi

  10. [17]

    Kwiatkowska, Moshe Y

    Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of M arkov decision processes. Log. Methods Comput. Sci. , 4(4), 2008. https://doi.org/10.2168/LMCS-4(4:8)2008 doi:10.2168/LMCS-4(4:8)2008

    2008 doi

  11. [18]

    Kwiatkowska, and David Parker

    Lu Feng, Marta Z. Kwiatkowska, and David Parker. Compositional verification of probabilistic systems using learning. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010 , pages 133--142. IE...

    2010 doi

  12. [19]

    Kwiatkowska, and David Parker

    Lu Feng, Marta Z. Kwiatkowska, and David Parker. Automated learning of probabilistic assumptions for compositional reasoning. In Dimitra Giannakopoulou and Fernando Orejas, editors, Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held...

    2011

  13. [20]

    Humphrey, and Ufuk Topcu

    Lu Feng, Clemens Wiltsche, Laura R. Humphrey, and Ufuk Topcu. Controller synthesis for autonomous systems interacting with human operators. In ICCPS , pages 70--79. ACM , 2015. https://doi.org/10.1145/2735960.2735973 doi:10.1145/2735960.2735973

    2015

  14. [21]

    Kwiatkowska, Gethin Norman, and David Parker

    Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Automated verification techniques for probabilistic systems. In Marco Bernardo and Val \' e rie Issarny, editors, Formal Methods for Eternal Networked Software Systems - 11th International School on Formal ...

    2011

  15. [22]

    Pasareanu, and Sarai Sheinvald

    Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, and Sarai Sheinvald. Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf. , 24(5):667--689, 2022. URL: https://doi.org/10.1007/s10009-022-00669-9, https://doi.org/1...

    2022 doi

  16. [23]

    McMillan, and Zhaohui Fu

    Anubhav Gupta, Kenneth L. McMillan, and Zhaohui Fu. Automated assumption generation for compositional verification. Formal Methods Syst. Des. , 32(3):285--301, 2008. URL: https://doi.org/10.1007/s10703-008-0050-0, https://doi.org/10.1007/S10703-008-0050-0 doi:10.1007/S10703-008-0050-0

    2008 doi

  17. [24]

    Learning weighted assumptions for compositional verification of M arkov decision processes

    Fei He, Xiaowei Gao, Miaofei Wang, Bow - Yaw Wang, and Lijun Zhang. Learning weighted assumptions for compositional verification of M arkov decision processes. ACM Trans. Softw. Eng. Methodol. , 25(3):21:1--21:39, 2016. https://doi.org/10.1145/2907943 doi:10.1145/2907943

    2016 doi

  18. [25]

    Henzinger, Shaz Qadeer, and Sriram K

    Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. You assume, we guarantee: Methodology and case studies. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proc...

    1998 doi

  19. [26]

    Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. , 5(4):596--619, 1983. https://doi.org/10.1145/69575.69577 doi:10.1145/69575.69577

    1983

  20. [27]

    Parameter synthesis in M arkov models

    Sebastian Junges. Parameter synthesis in M arkov models . PhD thesis, RWTH Aachen University, Germany, 2020. URL: https://publications.rwth-aachen.de/record/783179

    2020

  21. [28]

    Parameter synthesis for M arkov models: covering the parameter space

    Sebastian Junges, Erika \' A brah \' a m, Christian Hensel, Nils Jansen, Joost - Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for M arkov models: covering the parameter space. Formal Methods Syst. Des. , 62(1):181--259, 2024. URL: https://doi.org/10.1007...

    2024 doi

  22. [29]

    P \' e rez, and Tobias Winkler

    Sebastian Junges, Joost - Pieter Katoen, Guillermo A. P \' e rez, and Tobias Winkler. The complexity of reachability in parametric M arkov decision processes. J. Comput. Syst. Sci. , 119:183--210, 2021. https://doi.org/10.1016/J.JCSS.2021.02.006 doi:10.1016/J.JCSS.2021.02.006

    2021 doi

  23. [30]

    Sebastian Junges and Matthijs T. J. Spaan. Abstraction-refinement for hierarchical probabilistic models. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I , vo...

    2022 doi

  24. [31]

    The probabilistic model checking landscape

    Joost-Pieter Katoen. The probabilistic model checking landscape. In LICS , pages 31--45. ACM , 2016. https://doi.org/10.1145/2933575.2934574 doi:10.1145/2933575.2934574

    2016

  25. [32]

    Pasareanu, and Edmund M

    Anvesh Komuravelli, Corina S. Pasareanu, and Edmund M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13...

    2012 doi

  26. [33]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Using probabilistic model checking in systems biology. SIGMETRICS Perform. Evaluation Rev. , 35(4):14--21, 2008. https://doi.org/10.1145/1364644.1364651 doi:10.1145/1364644.1364651

    2008

  27. [34]

    Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

    Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Assume-guarantee verification for probabilistic systems. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2...

    2010

  28. [36]

    Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule

    Rui Li and Yang Liu. Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule. In 17th IEEE International Conference on Software Engineering Research, Management and Applications, SERA 2019, Honolulu, HI, USA, May 29-31, 2019 , pages 1...

    2019

  29. [37]

    Accurately computing expected visiting times and stationary distributions in M arkov chains

    Hannah Mertens, Joost - Pieter Katoen, Tim Quatmann, and Tobias Winkler. Accurately computing expected visiting times and stationary distributions in M arkov chains. In Bernd Finkbeiner and Laura Kov \' a cs, editors, Tools and Algorithms for the Construction and Analysis of S...

    2024

  30. [38]

    Namjoshi and Richard J

    Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In Marsha Chechik and Jean - Fran c ois Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the Eur...

    2016

  31. [39]

    Analysis of probabilistic contract signing

    Gethin Norman and Vitaly Shmatikov. Analysis of probabilistic contract signing. J. Comput. Secur. , 14(6):561--589, 2006. https://doi.org/10.3233/jcs-2006-14604 doi:10.3233/jcs-2006-14604

    2006 doi

  32. [40]

    Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M

    Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L * algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. , 32(3):175--205, 2008. URL: https://...

    2008 doi

  33. [41]

    Pasareanu, Divya Gopinath, and Huafeng Yu

    Corina S. Pasareanu, Divya Gopinath, and Huafeng Yu. Compositional verification for autonomous systems with deep learning components. CoRR , abs/1810.08303, 2018. URL: http://arxiv.org/abs/1810.08303, https://arxiv.org/abs/1810.08303 arXiv:1810.08303

    2018 arXiv

  34. [42]

    Pasareanu, Ravi Mangal, Divya Gopinath, and Huafeng Yu

    Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, and Huafeng Yu. Assumption generation for learning-enabled autonomous systems. In Panagiotis Katsaros and Laura Nenzi, editors, Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3-6, 2...

    2023 doi

  35. [43]

    In transition from global to modular temporal reasoning about programs

    Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8-19 October 1984 , volume 13 of NATO ASI Series , pages 123-...

    1984 doi

  36. [44]

    Parameter synthesis for M arkov models: Faster than ever

    Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost - Pieter Katoen. Parameter synthesis for M arkov models: Faster than ever. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International ...

    2016 doi

  37. [45]

    Modeling and verification of randomized distributed real-time systems

    Roberto Segala. Modeling and verification of randomized distributed real-time systems . PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA , 1995. URL: https://hdl.handle.net/1721.1/36560

    1995

  38. [46]

    Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput. , 2(2):250--273, 1995

    1995

  39. [47]

    Parametrised compositional verification with multiple process and data types

    Antti Siirtola and Keijo Heljanko. Parametrised compositional verification with multiple process and data types. In Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz - Koutny, editors, 13th International Conference on Application of Concurrency to System Design, ACSD 20...

    2013 doi

  40. [48]

    Monotonicity in M arkov models

    Jip Spel. Monotonicity in M arkov models . PhD thesis, RWTH Aachen University, Germany, 2023. URL: https://publications.rwth-aachen.de/record/974903

    2023

  41. [49]

    Jip Spel, Sebastian Junges, and Joost - Pieter Katoen. Are parametric M arkov chains monotonic? In Yu - Fang Chen, Chih - Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, Octo...

    2019 doi

  42. [50]

    Finding provably optimal M arkov chains

    Jip Spel, Sebastian Junges, and Joost - Pieter Katoen. Finding provably optimal M arkov chains. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part o...

    2021

  43. [51]

    An introduction to probabilistic automata

    Mari \" e lle Stoelinga. An introduction to probabilistic automata. Bull. EATCS , 78:176--198, 2002

    2002

  44. [52]

    Compositional solution of mean payoff games by string diagrams

    Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mari \" e lle Stoelinga, and Matthias V...

    2024

  45. [53]

    Assume-guarantee strategy synthesis for stochastic games

    Clemens Wiltsche. Assume-guarantee strategy synthesis for stochastic games . PhD thesis, University of Oxford, UK , 2015

    2015

  46. [54]

    Assume-guarantee reasoning framework for MDP-POMDP

    Xiaobin Zhang, Bo Wu, and Hai Lin. Assume-guarantee reasoning framework for MDP-POMDP . In 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016 , pages 795--800. IEEE , 2016. https://doi.org/10.1109/CDC.2016.7798365 doi:10.1109/CDC.2...

    2016

Pith tools

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