Pith. sign in

REVIEW 3 major objections 4 minor 103 references

Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read A fixed first-order sentence characterizes probabilistic bisimulation on regular weighted transition systems, making anonymity and uniformity of parameterized systems automatically checkable.

desk verdict Theorem 4 is unsound as printed; the central verification condition can accept non-bisimulations, but the framework and case studies are worth a careful look. read the letter →

arxiv 2505.09963 v1 pith:XDVUKATF submitted 2025-05-15 cs.SE cs.FL

Chih-Duo Hong , Anthony W. Lin , Philipp Rümmer , Rupak Majumdar This is my paper · ORCID
classification cs.SEcs.FL MSC 68Q6068Q4503B70
keywords probabilisticbisimulationparameterizedsystemsregularstructuresanonymityuniformityactiveautomatalearningMarkovdecisionprocessesminimaldeviationassumption
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 sets out to show that probabilistic bisimulation can be checked automatically for entire infinite families of finite-state systems, not just one instance at a time. Its central theorem gives a fixed first-order sentence such that a binary relation is a bisimulation on a weighted transition system exactly when the system extended with that relation satisfies the sentence, and the check is decidable whenever both are regular. Because anonymity and uniformity can both be expressed as the existence of a bisimulation between a system and a reference system or over a reversed chain, the same sentence covers both properties. The paper backs the theory with an active-learning procedure that synthesizes regular bisimulation relations automatically, reporting push-button verification of dining cryptographers, crowds, grades, random walks, random sums, Knuth-Yao and naive random number generators, and the ballot theorem. A sympathetic reader would care because this offers one unified route to properties that previously required distinct, often manual techniques in the parameterized setting.

What carries the argument

The load-bearing object is the first-order theory of regular structures, in which universes are regular languages and all relations are regular, so formulas are effectively reducible to automata and decidable. Inside this theory, the paper defines regular weighted transition systems, normalizing probabilities to natural-number weights under the minimal-deviation assumption, and encodes the probabilistic bisimulation condition as a fixed first-order sentence. A second mechanism is active automata learning in the style of L-star, which synthesizes a regular candidate bisimulation by asking membership queries on finite instances and equivalence queries that check the bisimulation sentence. The two mechanisms work together: the theory supplies the verification condition, and the learner supplies the proof.

What would settle it

The central claim would fail if there existed a regular weighted transition system and a regular relation such that the extended structure satisfies the fixed sentence but the relation is not a bisimulation, or vice versa. Concretely, take two states with outgoing probability masses to one equivalence class of 0.4 plus 0.1 on one side and 0.5 on the other; the sentence must reject this relation. Running the automata-based check on that two-state example and inspecting the verdict would settle whether the iterated-addition encoding inside the sentence is sound.

Watch

Extended reading notes

Core claim

At the paper's core is the claim that bisimulation on a weighted transition system is a first-order property of the system plus the relation. Theorem 4 constructs a fixed sentence expressing that the relation is an equivalence and that, for every action and every equivalence class, the total outgoing probability mass to that class is the same from any two related states. The sentence works by existentially guessing the bounded list of successors and a labeling that names their equivalence classes, then using a definable iterated addition to compare the class-wise probability sums. When the system and relation have regular presentations over finite words, satisfaction of the sentence is decidable by automata-theoretic means. The paper then shows that anonymity of a Markov decision process follows from a bisimulation between the process and a reference system, and that uniformity of a probabilistic program's output distribution follows from a bisimulation on the reversed chain whose final states are all equivalent.

Load-bearing premise

The method assumes every transition probability in the family is an integer multiple of a single epsilon greater than zero, so that probabilities can be normalized into a regular natural-number-weight encoding; the parametric-probability extension is only sketched and not proved.

Editorial extensions

If this is right

  • Any regular weighted transition system and regular relation can be certified as bisimulation or not by a single automata check, so parameterized anonymity and uniformity become proof-synthesis problems rather than per-instance model checks.
  • Protocols with unbounded participant numbers, such as dining cryptographers, crowds, and grades, get one proof covering every size parameter instead of a separate finite check for each n.
  • Randomized algorithms can be certified to sample uniformly without fixing the range parameter, as demonstrated for Knuth-Yao random number generation and the ballot theorem.
  • Because the same bisimulation sentence handles both anonymity and uniformity, tools, proofs, and learning procedures transfer between the two property classes.
  • Whenever the greatest bisimulation is regular, the active-learning procedure is guaranteed to terminate and to produce a correct answer, giving a termination guarantee for the proof search in that case.

Reading between the lines

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

  • Because bisimulation compares sums of path probabilities rather than one-to-one path couplings, this approach can prove uniform-output facts that coupling arguments cannot, while probability independence that requires self-composition lies outside its scope; a combined proof calculus is a natural next step.
  • The minimal-deviation assumption is likely the main boundary of the method: extending the sentence to parametric transition probabilities would require a correctness proof for the sketched addition axioms, and instantiating the crowds protocol with a symbolic forwarding probability would be a direct test of that extension.
  • An approximate analogue is visible from the same machinery: replacing equality of probability masses with epsilon-bisimilarity or bisimulation metrics could yield decidable checks of near-anonymity for cryptographic protocols, although the paper only lists this as future work.
  • One could try to recover completeness by alternating the learner with an enumerative synthesis procedure, since the learning algorithm alone may fail to find a regular bisimulation even when one exists.
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.

Referee Report

3 major / 4 minor

Summary. The paper proposes a first-order logical framework, based on the decidable theory of regular structures (FOreg), for verifying probabilistic bisimulation in parameterized systems. The central technical claim is Theorem 4: for every bounded-branching weighted transition system S and binary relation R, there is a fixed FO sentence Φ with S_R |= Φ iff R is a probabilistic bisimulation over S. This theorem is then used to justify an active-automata-learning procedure that synthesizes regular bisimulation relations, which are applied to verify anonymity and uniformity properties of parameterized probabilistic systems. The paper reports a prototype tool and case studies covering dining cryptographers, crowds, grades, random walks and sums, two random number generators, and the ballot theorem.

Significance. If Theorem 4 is correct and the framework is sound, this is a valuable contribution: it gives a unified, decidable proof rule for a class of infinite-state probabilistic verification problems, connects bisimulation proofs with automata learning, and provides automated verification for parameterized protocols and randomized algorithms beyond finite-state model checking. The paper is careful to state undecidability of the general problem and to present the learning procedure as a heuristic with independent verification of candidates. The choice of verification conditions in FOreg and the integration with MONA/TAPAS are concrete and reproducible in principle. However, the central characterization in Theorem 4 is unsound as printed, which invalidates the equivalence-query mechanism in Algorithm 2 and therefore the soundness of the verification procedure as stated.

major comments (3)
  1. [Theorem 4, Eq. (6)] The formula λ(s,a,s′) labels the successors of s and s′ independently: compat(u,α) constrains only pairs within u, and compat(v,β) constrains only pairs within v. There is no conjunct of the form R(u_i,v_j) ⇔ α_i = β_j, so equality of label sums can compare masses of different R-equivalence classes. Concretely, take the one-action WTS with states {s,s′,x,y}, transitions s→a x and s′→a y with weight 1, and (to make it a Markov chain) x→a x, y→a y with weight 1. Let R have classes {s,s′}, {x}, {y}; the branching bound is n=1. R is not a bisimulation because the mass from s to class {x} is 1 while the mass from s′ to {x} is 0. Yet the formula is satisfied by choosing u=x, v=y, α=β=(1): both succ conditions hold, compat is vacuous, and the label-1 sums are both 1 while all other label sums are 0. Thus S_R |= Φ holds for a non-bisimulation, contradicting the claimed iff. This makes Algorithm 2's equivalence query unsound, since it can certify a relation that is not a bisimulation. The theorem can be repaired by adding a cross-compatibility conjunct, for example ∧_{i,j}(R(u_i,v_j) ⇔ α_i = β_j), and then re-proving both directions; the formula as printed must be corrected before the paper's verification claims can be accepted.
  2. [Section V-C-b and Section VI-b] The extension to parametric probabilities is only sketched: the text defines a set Q of probability parameters, adds an addition operator over Q∪P, and posits axioms such as commutativity, but it gives no formal statement or proof that the resulting proof rule is sound and complete for bisimulation with parametric weights. This is not a cosmetic gap because Section VI-b reports verification of the Crowds protocol, whose transition probabilities involve a parameter p, and says 'We illustrate this extension in our evaluation.' If the crowds result depends on this unproved extension, the case study is not supported by Theorem 4. Please provide a precise definition of the parametric WTS semantics and a correctness theorem for the parametric bisimulation rule, or state explicitly how crowds is handled under the fixed-probability encoding.
  3. [Theorem 4 proof, succ construction] The proof of Theorem 4 requires that, for every state and action, the formula can choose n distinct configurations u_1,…,u_n containing all successors. If the state space has fewer than n distinct elements, no such tuple exists, even though the branching bound n may exceed the state count of a finite instance. The authors should either assume the universe has at least n elements, take n as min(branching bound, |S|), or otherwise handle finite universes explicitly. This is a repairable detail, but it should be stated because the parameterized instances in Section VI are finite.
minor comments (4)
  1. [Theorem 16] Condition (ii), 's0 is bisimilar only to itself with respect to R,' should be written as [s0]_R = {s0} to remove ambiguity; the proof does use this condition to justify the base case p_0(u)=p_0(v).
  2. [Section II-A and Theorem 4] Theorem 4 states decidability 'when both S and R are regular' without repeating the minimal-deviation assumption introduced in Section II-A. Since the encoding of the addition operation + and of probability weights in FOreg depends on that assumption, the theorem statement should explicitly say 'under the minimal-deviation assumption' or 'when + is regular-presentable.'
  3. [Example 3 / Figure 1] The display of the pPDA rules is garbled in places (for example the line 'dX 0.5 −−→bXX dX 0.5 −−→d b X 1 − →dXX cY 1 − →cXX'). Please reformat the rule notation for readability.
  4. [Algorithm 2 / Figure 2] The box 'Isw∈L(˜R|w|)?' in Figure 2 is unclear, and Algorithm 2's written description of the counterexample case would benefit from an explicit statement that the returned word is v⊗u, matching the symmetric-difference notation used in the learning algorithm.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the bisimulation check independently verifies the learned candidate, and cited prior work is either standard or reproved in the paper.

full rationale

The paper's central derivation is self-contained rather than circular. Theorem 4 defines a fixed first-order sentence Phi and the verification procedure checks S_R |= Phi; the learning algorithm only proposes candidate regular relations, and Algorithm 2 independently checks E subset R and Phi, so the final certificate is not fitted to the property. The main logical ingredients come from external results (Proposition 2 from Blumensath-Grädel and Colcombet-Löding, Proposition 1 from Bianco-De Alfaro and Clerc et al., and the L-star algorithm from Angluin and Rivest-Schapire), while padding and the bisimulation characterization are proved in the paper itself. The paper does invoke self-citations ([27], [48], [53], [54], [65]), but these are used for context, for standard encodings, or for optimization options such as automatic invariant generation; they are not used as a uniqueness theorem or as an unproved ansatz. The minimal-deviation assumption is an explicitly stated domain restriction, not a fitted parameter renamed as a prediction. I find no equation, fitted value, or self-citation chain that makes a claimed result coincide with its input by construction. Any concern about the soundness of the lambda formula in Eq. (6) would be a correctness defect, not circularity.

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

No new entities or fitted constants are introduced. The framework relies on standard assumptions about the class of systems (regular, weakly finite, bounded branching, minimal deviation) and on the standard correctness of the decision procedure for WS1S. The termination of learning is conditional on an unproven regularity property.

assumptions (3)
  • domain assumption Minimal deviation assumption: all transition probabilities are multiples of some epsilon > 0
    Sets the class of systems to which the encoding applies; stated in Section II-A and used in the FOreg encoding of weights.
  • domain assumption The parameterized system has a regular presentation and is bounded branching and weakly finite
    Needed for encoding in FOreg and for Theorem 4 and the learning procedure; stated in Sections II-A, III and IV.
  • domain assumption For monotone termination of learning, the greatest bisimulation of the parameterized system is regular
    Theorem 11 guarantees termination only when the greatest bisimulation is regular; the paper does not prove this for the case studies, it is empirically observed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification." pith.science (2026). https://pith.science/paper/XDVUKATF

@misc{pith2026250509963,
  author       = {Pith},
  title        = {Pith review of: Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XDVUKATF}},
  note         = {Machine review of arXiv:2505.09963}
}
read the original abstract

Bisimulation is crucial for verifying process equivalence in probabilistic systems. This paper presents a novel logical framework for analyzing bisimulation in probabilistic parameterized systems, namely, infinite families of finite-state probabilistic systems. Our framework is built upon the first-order theory of regular structures, which provides a decidable logic for reasoning about these systems. We show that essential properties like anonymity and uniformity can be encoded and verified within this framework in a manner aligning with the principles of deductive software verification, where systems, properties, and proofs are expressed in a unified decidable logic. By integrating language inference techniques, we achieve full automation in synthesizing candidate bisimulation proofs for anonymity and uniformity. We demonstrate the efficacy of our approach by addressing several challenging examples, including cryptographic protocols and randomized algorithms that were previously beyond the reach of fully automated methods.

Figures

Figures reproduced from arXiv: 2505.09963 by the authors.

Figure 1
Figure 1. Part of the configuration graph in Example 3, adapted from [31]. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. An overview of using automata learning to synthesize a bisimulation ˜ [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Example probabilistic programs for verifying probability uniformity and equivalence. We use [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: A Markov chain with uniform output distribution over [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

103 extracted references · 80 canonical work pages

  1. [27]

    Probabilistic bisimulation for parameterised systems,

    C.-D. Hong, A. W. Lin, R. Majumdar, and P. Rümmer, “Probabilistic bisimulation for parameterised systems,” in International Conference on Computer-Aided Verification (CAV). Springer, 2019, pp. 455–474

    work page 2019

  2. [1]

    Milner, A calculus of communicating systems

    R. Milner, A calculus of communicating systems . Springer, 1980

    1980

  3. [2]

    Prentice hall Englewood Cliffs, 1989, vol

    ——, Communication and Concurrency . Prentice hall Englewood Cliffs, 1989, vol. 84

    1989

  4. [3]

    Model-driven software verification,

    G. J. Holzmann and R. Joshi, “Model-driven software verification,” in International SPIN Workshop. Springer, 2004, pp. 76–91

    2004

  5. [4]

    Deriving bisimulation rela- tions from path extension based equivalence checkers,

    K. Banerjee, D. Sarkar, and C. Mandal, “Deriving bisimulation rela- tions from path extension based equivalence checkers,” IEEE Transac- tions on Software Engineering , vol. 43, no. 10, pp. 946–953, 2016

    2016

  6. [5]

    A core calculus for equational proofs of cryptographic protocols,

    J. Gancher, K. Sojakova, X. Fan, E. Shi, and G. Morrisett, “A core calculus for equational proofs of cryptographic protocols,” Symposium on Principles of Programming Languages (POPL) , vol. 7, no. POPL, pp. 866–892, 2023

    2023

  7. [6]

    Probabilistic bisimulation and equivalence for security analysis of network proto- cols,

    A. Ramanathan, J. Mitchell, A. Scedrov, and V . Teague, “Probabilistic bisimulation and equivalence for security analysis of network proto- cols,” in International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Springer, 2004, pp. 468–483

    2004

  8. [7]

    A logical char- acterization of differential privacy,

    V . Castiglioni, K. Chatzikokolakis, and C. Palamidessi, “A logical char- acterization of differential privacy,”Science of Computer Programming, vol. 188, p. 102388, 2020

    2020

Show all 103 references
  1. [8]

    Bisimulation for secure information flow analysis of multi-threaded programs,

    A. A. Noroozi, J. Karimpour, and A. Isazadeh, “Bisimulation for secure information flow analysis of multi-threaded programs,” Mathematical and Computational Applications , vol. 24, no. 2, p. 64, 2019

    2019

  2. [9]

    Refinement-based verification of device-to-device information flow,

    N. Dong, R. Guanciale, and M. Dam, “Refinement-based verification of device-to-device information flow,” inFormal Methods in Computer- Aided Design (FMCAD) , 2021, pp. 123–132

    2021

  3. [10]

    An automated quantitative information flow analysis for concurrent programs,

    K. Salehi, A. A. Noroozi, S. Amir-Mohammadian, and M. Mohagheghi, “An automated quantitative information flow analysis for concurrent programs,” in International Conference on Quantitative Evaluation of Systems (QEST). Springer, 2022, pp. 43–63

    2022

  4. [11]

    Quantifying over information change with common knowledge,

    T. Ågotnes and R. Galimullin, “Quantifying over information change with common knowledge,” Autonomous Agents and Multi-Agent Sys- tems (AAMAS), vol. 37, no. 1, p. 19, 2023

    2023

  5. [12]

    Bisimulation-based concept learning in description logics,

    T.-L. Tran, Q.-T. Ha, T.-L.-G. Hoang, L. A. Nguyen, and H. S. Nguyen, “Bisimulation-based concept learning in description logics,” Fundamenta Informaticae, vol. 133, no. 2-3, pp. 287–303, 2014

    2014

  6. [13]

    Bisimulations for knowing how logics,

    R. Fervari, F. R. Velázquez-Quesada, and Y . Wang, “Bisimulations for knowing how logics,” The Review of Symbolic Logic , vol. 15, no. 2, pp. 450–486, 2022

    2022

  7. [14]

    Trustworthy runtime verification via bisimulation (experience report),

    R. G. Scott, M. Dodds, I. Perez, A. E. Goodloe, and R. Dockins, “Trustworthy runtime verification via bisimulation (experience report),” Proceedings of the ACM on Programming Languages (POPL) , vol. 7, no. ICFP, pp. 305–321, 2023

    2023

  8. [15]

    Checking NFA equivalence with bisimulations up to congruence,

    F. Bonchi and D. Pous, “Checking NFA equivalence with bisimulations up to congruence,” ACM SIGPLAN Notices , vol. 48, no. 1, pp. 457– 468, 2013

    2013

  9. [16]

    Coinductive algorithms for büchi automata,

    D. Kuperberg, L. Pinault, and D. Pous, “Coinductive algorithms for büchi automata,” Fundamenta Informaticae, vol. 180, no. 4, pp. 351– 373, 2021

    2021

  10. [17]

    Fast coalgebraic bisimilarity minimiza- tion,

    J. Jacobs and T. Wißmann, “Fast coalgebraic bisimilarity minimiza- tion,” Symposium on Principles of Programming Languages (POPL) , vol. 7, no. POPL, pp. 1514–1541, 2023

    2023

  11. [18]

    SMT-based bisimulation minimisation of Markov models,

    C. Dehnert, J.-P. Katoen, and D. Parker, “SMT-based bisimulation minimisation of Markov models,” in Verification, Model Checking, and Abstract Interpretation (VMCAI) . Springer, 2013, pp. 28–47

    2013

  12. [19]

    A bisimulation-based foundation for scale reductions of continuous-time markov chains,

    L. Lin, J. Cao, J. Lam, L. Rutkowski, G. M. Dimirovski, and S. Zhu, “A bisimulation-based foundation for scale reductions of continuous-time markov chains,” IEEE Transactions on Automatic Control , 2024

    2024

  13. [20]

    Bq-nco: Bisimulation quotienting for efficient neural combinatorial optimiza- tion,

    D. Drakulic, S. Michel, F. Mai, A. Sors, and J.-M. Andreoli, “Bq-nco: Bisimulation quotienting for efficient neural combinatorial optimiza- tion,” Advances in Neural Information Processing Systems (NeuIPS) , vol. 36, 2024

    2024

  14. [21]

    Backward bisimulation in markov chain model checking,

    J. Sproston and S. Donatelli, “Backward bisimulation in markov chain model checking,” IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 531–546, 2006

    2006

  15. [22]

    Polynomial time algorithms for testing probabilistic bisimu- lation and simulation,

    C. Baier, “Polynomial time algorithms for testing probabilistic bisimu- lation and simulation,” in International Conference on Computer-Aided Verification (CAV). Springer, 1996, pp. 50–61

    1996

  16. [23]

    Simple O(m log n) time markov chain lumping,

    A. Valmari and G. Franceschinis, “Simple O(m log n) time markov chain lumping,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Springer, 2010, pp. 38–52

    2010

  17. [24]

    On the complexity of computing probabilistic bisimilarity,

    D. Chen, F. van Breugel, and J. Worrell, “On the complexity of computing probabilistic bisimilarity,” in International Conference on Foundations of Software Science and Computation Structures (FoS- SaCS). Springer, 2012, pp. 437–451

    2012

  18. [25]

    Infinite results,

    F. Moller, “Infinite results,” in International Conference on Concur- rency Theory (CONCUR) . Springer, 1996, pp. 195–216

    1996

  19. [26]

    Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables,

    R. Kumar, C. Zhou, and S. Basu, “Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables,” in American Control Conference. IEEE, 2006, pp. 6–pp

    2006

  20. [28]

    Bisimulation learning,

    A. Abate, M. Giacobbe, and Y . Schnitzer, “Bisimulation learning,” in International Conference on Computer Aided Verification (CAV) . Springer, 2024, pp. 161–183

    2024

  21. [29]

    Roadmap of infinite results,

    J. Srba, “Roadmap of infinite results,” in Current Trends in Theoretical Computer Science: The Challenge of the New Centuryj . World Scientific, 2004, pp. 337–350

    2004

  22. [30]

    The bisimulation problem for equational graphs of finite out-degree,

    G. Sénizergues, “The bisimulation problem for equational graphs of finite out-degree,” SIAM Journal on Computing , vol. 34, no. 5, pp. 1025–1106, 2005

    2005

  23. [31]

    Game characterization of probabilistic bisimilarity, and applications to pushdown automata,

    V . Forejt, P. Jan ˇcar, S. Kiefer, and J. Worrell, “Game characterization of probabilistic bisimilarity, and applications to pushdown automata,” Logical Methods in Computer Science (LMCS) , vol. 14, no. 4, 2018

    2018

  24. [32]

    Pushdown normal-form bisimulation: A nominal context-free approach to program equiva- lence,

    V . Koutavas, Y .-Y . Lin, and N. Tzevelekos, “Pushdown normal-form bisimulation: A nominal context-free approach to program equiva- lence,” in Symposium on Logic in Computer Science (LICS) , 2024, pp. 1–15

    2024

  25. [33]

    Equivalence checking 40 years after: a review of bisimulation tools,

    H. Garavel and F. Lang, “Equivalence checking 40 years after: a review of bisimulation tools,” A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday , pp. 213–265, 2022

    2022

  26. [34]

    Ahrendt, B

    W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich, Deductive Software Verification - The KeY Book - From Theory to Practice . Springer, 2016, vol. 10001

    2016

  27. [35]

    Deductive software verification: from pen-and-paper proofs to industrial tools,

    R. Hähnle and M. Huisman, “Deductive software verification: from pen-and-paper proofs to industrial tools,” Computing and Software Science: State of the Art and Perspectives , pp. 345–373, 2019

    2019

  28. [36]

    Loop invariants: Analysis, clas- sification, and examples,

    C. A. Furia, B. Meyer, and S. Velder, “Loop invariants: Analysis, clas- sification, and examples,” ACM Computing Surveys (CSUR) , vol. 46, no. 3, pp. 1–51, 2014

    2014

  29. [37]

    Finite presentations of infinite struc- tures: Automata and interpretations,

    A. Blumensath and E. Grädel, “Finite presentations of infinite struc- tures: Automata and interpretations,” Theory of Computing Systems (TCS), vol. 37, no. 6, pp. 641–674, 2004

    2004

  30. [38]

    Transforming structures by set interpre- tations,

    T. Colcombet and C. Löding, “Transforming structures by set interpre- tations,” Logical Methods in Computer Science (LMCS) , vol. 3, no. 2, pp. paper–4, 2007

    2007

  31. [39]

    Regular model checking revisited,

    A. W. Lin and P. Rümmer, “Regular model checking revisited,” in Model Checking, Synthesis, and Learning: Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday . Springer, 2022, pp. 97–114

    2022

  32. [40]

    Probabilistic and nondeterministic aspects of anonymity,

    R. Beauxis and C. Palamidessi, “Probabilistic and nondeterministic aspects of anonymity,” Theoretical Computer Science, vol. 410, no. 41, pp. 4006–4025, 2009

    2009

  33. [41]

    Probabilistic anonymity,

    M. Bhargava and C. Palamidessi, “Probabilistic anonymity,” in Inter- national Conference on Concurrency Theory (CONCUR) . Springer, 2005, pp. 171–185

    2005

  34. [42]

    Anonymity and information hiding in multiagent systems,

    J. Y . Halpern and K. R. O’Neill, “Anonymity and information hiding in multiagent systems,” Journal of Computer Security , vol. 13, no. 3, pp. 483–514, 2005. 16

    2005

  35. [43]

    Proving uniformity and independence by self-composition and coupling,

    G. Barthe, T. Espitau, B. Grégoire, J. Hsu, and P.-Y . Strub, “Proving uniformity and independence by self-composition and coupling,” arXiv preprint arXiv:1701.06477, 2017

    2017 arXiv

  36. [44]

    Barthe, J.-P

    G. Barthe, J.-P. Katoen, and A. Silva, Foundations of Probabilistic Programming. Cambridge University Press, 2020

    2020

  37. [45]

    The dining cryptographers problem: Unconditional sender and recipient untraceability,

    D. Chaum, “The dining cryptographers problem: Unconditional sender and recipient untraceability,” Journal of Cryptology , vol. 1, no. 1, pp. 65–75, 1988

    1988

  38. [46]

    Model checking param- eterized systems,

    P. A. Abdulla, A. P. Sistla, and M. Talupur, “Model checking param- eterized systems,” Handbook of model checking , pp. 685–725, 2018

    2018

  39. [47]

    Parameterized verification of leader/follower systems via arithmetic constraints,

    G. Kourtis, C. Dixon, and M. Fisher, “Parameterized verification of leader/follower systems via arithmetic constraints,” IEEE Transactions on Software Engineering , 2024

    2024

  40. [48]

    Liveness of randomised parameterised systems under arbitrary schedulers,

    A. W. Lin and P. Rümmer, “Liveness of randomised parameterised systems under arbitrary schedulers,” in International Conference on Computer-Aided Verification (CAV). Springer, 2016, pp. 112–133

    2016

  41. [49]

    APEX: an analyzer for open probabilistic programs,

    S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell, “APEX: an analyzer for open probabilistic programs,” in International Conference on Computer-Aided Verification (CAV) . Springer, 2012, pp. 693–698

    2012

  42. [50]

    Crowds: Anonymity for web transac- tions,

    M. K. Reiter and A. D. Rubin, “Crowds: Anonymity for web transac- tions,” ACM transactions on information and system security , vol. 1, no. 1, pp. 66–92, 1998

    1998

  43. [51]

    The complexity of nonuniform random number generation,

    D. Knuth, “The complexity of nonuniform random number generation,” Algorithms and Complexity, New Directions and Results , pp. 357–428, 1976

    1976

  44. [52]

    Feller, An introduction to probability theory and its applications

    W. Feller, An introduction to probability theory and its applications . John Wiley & Sons, 1991, vol. 81

    1991

  45. [53]

    Learning to prove safety over parameterised concurrent systems,

    Y .-F. Chen, C.-D. Hong, A. W. Lin, and P. Rümmer, “Learning to prove safety over parameterised concurrent systems,” in International Conference on Formal Methods in Computer-Aided Design (FMCAD) . Springer, 2017, pp. 76–83

    2017

  46. [54]

    Parameterized synthesis with safety properties,

    O. Markgraf, C.-D. Hong, A. W. Lin, M. Najib, and D. Neider, “Parameterized synthesis with safety properties,” in Asian Symposium on Programming Languages and Systems . Springer, 2020, pp. 273– 292

    2020

  47. [55]

    ICE: A robust framework for learning invariants,

    P. Garg, C. Löding, P. Madhusudan, and D. Neider, “ICE: A robust framework for learning invariants,” in International Conference on Computer-Aided Verification (CAV). Springer, 2014, pp. 69–87

    2014

  48. [56]

    Bisimulation through probabilistic testing,

    K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Information and Computation , vol. 94, no. 1, pp. 1–28, 1991

    1991

  49. [57]

    Klarlund and A

    N. Klarlund and A. Møller, Mona Version 1.4: User Manual. BRICS, Department of Computer Science, University of Aarhus Denmark, 2001

    2001

  50. [58]

    Lazy automata techniques for WS1S,

    T. Fiedor, L. Holík, P. Jank˚ u, O. Lengál, and T. V ojnar, “Lazy automata techniques for WS1S,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Springer, 2017, pp. 407–425

    2017

  51. [59]

    Learning regular sets from queries and counterexamples,

    D. Angluin, “Learning regular sets from queries and counterexamples,” Information and Computation , vol. 75, no. 2, pp. 87–106, 1987

    1987

  52. [60]

    Inference of finite automata using homing sequences,

    R. L. Rivest and R. E. Schapire, “Inference of finite automata using homing sequences,” Information and Computation, vol. 103, no. 2, pp. 299–347, 1993

    1993

  53. [61]

    M. J. Kearns and U. V . Vazirani, An Introduction to Computational Learning Theory. MIT press, 1994

    1994

  54. [62]

    Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations,

    K. Etessami and M. Yannakakis, “Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations,” Journal of the ACM (JACM), vol. 56, no. 1, pp. 1–66, 2009

    2009

  55. [63]

    Model checking of probabilistic and nondeterministic systems,

    A. Bianco and L. De Alfaro, “Model checking of probabilistic and nondeterministic systems,” in Foundations of Software Technology and Theoretical Computer Science (FSTTCS) . Springer, 1995, pp. 499– 513

    1995

  56. [64]

    Expressiveness of probabilistic modal logics: A gradual approach,

    F. Clerc, N. Fijalkow, B. Klin, and P. Panangaden, “Expressiveness of probabilistic modal logics: A gradual approach,” Information and Computation, vol. 267, pp. 145–163, 2019

    2019

  57. [65]

    Symbolic techniques for parameterised verification,

    C.-D. Hong, “Symbolic techniques for parameterised verification,” Ph.D. dissertation, University of Oxford, 2022

    2022

  58. [66]

    Automatic presentations of infinite structures

    V . Bárány, “Automatic presentations of infinite structures.” Ph.D. dissertation, RWTH Aachen University, Germany, 2007

    2007

  59. [67]

    Proving termination of probabilis- tic programs using patterns,

    J. Esparza, A. Gaiser, and S. Kiefer, “Proving termination of probabilis- tic programs using patterns,” in International Conference on Computer- Aided Verification (CAV). Springer, 2012, pp. 123–138

    2012

  60. [68]

    Linear automaton transformations,

    A. Nerode, “Linear automaton transformations,” Proceedings of the American Mathematical Society , vol. 9, no. 4, pp. 541–544, 1958

    1958

  61. [69]

    Woess, Denumerable Markov chains

    W. Woess, Denumerable Markov chains . European Mathematical Society, 2009

    2009

  62. [70]

    Learning probabilistic ter- mination proofs,

    A. Abate, M. Giacobbe, and D. Roy, “Learning probabilistic ter- mination proofs,” in International Conference on Computer-Aided Verification (CAV). Springer, 2021, pp. 3–26

    2021

  63. [71]

    Algorithmic probabilistic game semantics,

    S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell, “Algorithmic probabilistic game semantics,” Formal Methods in System Design (FMSD), vol. 43, no. 2, pp. 285–312, 2013

    2013

  64. [72]

    Constraint-based synthesis of coupling proofs,

    A. Albarghouthi and J. Hsu, “Constraint-based synthesis of coupling proofs,” in International Conference on Computer Aided Verification (CAV). Springer, 2018, pp. 327–346

    2018

  65. [73]

    The Armoise language,

    J. Leroux and G. Point, “The Armoise language,” https://tapas.labri.fr/ wp/?page_id=17, 2010

    2010

  66. [74]

    Tapas: The talence presburger arithmetic suite,

    ——, “Tapas: The talence presburger arithmetic suite,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 2009, pp. 182–185

    2009

  67. [75]

    Software model synthesis using satisfi- ability solvers,

    M. J. Heule and S. Verwer, “Software model synthesis using satisfi- ability solvers,” Empirical Software Engineering , vol. 18, no. 4, pp. 825–856, 2013

    2013

  68. [76]

    The thousand-and-one cryptographers,

    A. McIver and C. Morgan, “The thousand-and-one cryptographers,” Engineering Secure and Dependable Software Systems, vol. 53, p. 137, 2019

    2019

  69. [77]

    Formal certification of code-based cryptographic proofs,

    G. Barthe, B. Grégoire, and S. Zanella Béguelin, “Formal certification of code-based cryptographic proofs,” in Symposium on Principles of programming languages (POPL). ACM, 2009, pp. 90–101

    2009

  70. [78]

    A quantitative probabilistic relational hoare logic,

    M. Avanzini, G. Barthe, D. Davoli, and B. Grégoire, “A quantitative probabilistic relational hoare logic,” arXiv preprint arXiv:2407.17127 , 2024

    2024 arXiv

  71. [79]

    Abstraction for epistemic model checking of dining cryptographers-based protocols,

    O. Al Bataineh and R. van der Meyden, “Abstraction for epistemic model checking of dining cryptographers-based protocols,” in Confer- ence on Theoretical Aspects of Rationality and Knowledge , 2011, pp. 247–256

    2011

  72. [80]

    MCMAS: an open-source model checker for the verification of multi-agent systems,

    A. Lomuscio, H. Qu, and F. Raimondi, “MCMAS: an open-source model checker for the verification of multi-agent systems,” Interna- tional Journal on Software Tools for Technology Transfer , vol. 19, pp. 9–30, 2017

    2017

  73. [81]

    Parametric model checking with ver ics,

    M. Knapik, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, and A. Zbrzezny, “Parametric model checking with ver ics,” Transactions on Petri Nets and Other Models of Concurrency , pp. 98–120, 2010

    2010

  74. [82]

    Apte: an algorithm for proving trace equivalence,

    V . Cheval, “Apte: an algorithm for proving trace equivalence,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Springer, 2014, pp. 587–592

    2014

  75. [83]

    Automating open bisimulation checking for the spi calculus,

    A. Tiu and J. Dawson, “Automating open bisimulation checking for the spi calculus,” in Computer Security Foundations Symposium . IEEE, 2010, pp. 307–321

    2010

  76. [84]

    A survey of symbolic methods in computational analysis of cryptographic systems,

    V . Cortier, S. Kremer, and B. Warinschi, “A survey of symbolic methods in computational analysis of cryptographic systems,” Journal of Automated Reasoning , vol. 46, pp. 225–259, 2011

    2011

  77. [85]

    The modest toolset: An integrated environment for quantitative modeling and verification,

    A. Hartmanns and H. Hermanns, “The modest toolset: An integrated environment for quantitative modeling and verification,” in Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2014, pp. 593–598

    2014

  78. [86]

    Probabilistic analysis of an anonymity system,

    V . Shmatikov, “Probabilistic analysis of an anonymity system,” Journal of Computer Security , vol. 12, no. 3-4, pp. 355–377, 2004

    2004

  79. [87]

    PRISM 4.0: Verification of probabilistic real-time systems,

    M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of probabilistic real-time systems,” in International Conference on Computer-Aided Verification (CAV). Springer, 2011, pp. 585–591

    2011

  80. [88]

    The probabilistic model checker Storm,

    C. Hensel, S. Junges, J.-P. Katoen, T. Quatmann, and M. V olk, “The probabilistic model checker Storm,” International Journal on Software Tools for Technology Transfer, pp. 1–22, 2022

    2022

  81. [89]

    J. J. Rutten, Mathematical techniques for analyzing concurrent and probabilistic systems. American Mathematical Society, 2004, no. 23

    2004

  82. [90]

    Model checking indistinguishability of randomized security proto- cols,

    M. S. Bauer, R. Chadha, A. Prasad Sistla, and M. Viswanathan, “Model checking indistinguishability of randomized security proto- cols,” in International Conference on Computer Aided Verification (CAV). Springer, 2018, pp. 117–135

    2018

  83. [91]

    Symbolic protocol verification with dice: process equivalences in the presence of probabilities,

    V . Cheval, R. Crubillé, and S. Kremer, “Symbolic protocol verification with dice: process equivalences in the presence of probabilities,” in Computer Security Foundations Symposium (CSF) . IEEE, 2022, pp. 319–334

    2022

  84. [92]

    Psi: Exact symbolic inference for probabilistic programs,

    T. Gehr, S. Misailovic, and M. Vechev, “Psi: Exact symbolic inference for probabilistic programs,” in International Conference on Computer Aided Verification (CAV). Springer, 2016, pp. 62–83

    2016

  85. [93]

    Incremental inference for probabilistic programs,

    M. Cusumano-Towner, B. Bichsel, T. Gehr, M. Vechev, and V . K. Mansinghka, “Incremental inference for probabilistic programs,” in Conference on Programming Language Design and Implementation (PLDI), 2018, pp. 571–585

    2018

  86. [94]

    Symbolic execution for randomized programs,

    Z. Susag, S. Lahiri, J. Hsu, and S. Roy, “Symbolic execution for randomized programs,” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, pp. 1583–1612, 2022

    2022

  87. [95]

    Exploring probabilistic bisimulations, part i,

    M. Hennessy, “Exploring probabilistic bisimulations, part i,” Formal Aspects of Computing , vol. 24, no. 4, pp. 749–768, 2012

    2012

  88. [96]

    Weak bisimulation for fully probabilistic processes,

    C. Baier and H. Hermanns, “Weak bisimulation for fully probabilistic processes,” in International Conference on Computer Aided Verification (CAV). Springer, 1997, pp. 119–130

    1997

  89. [97]

    Weak bisimulation for proba- bilistic systems,

    A. Philippou, I. Lee, and O. Sokolsky, “Weak bisimulation for proba- bilistic systems,” in International Conference on Concurrency Theory (CONCUR). Springer, 2000, pp. 334–349

    2000

  90. [98]

    Branching bisimulation for probabilis- tic systems: Characteristics and decidability,

    S. Andova and T. A. Willemse, “Branching bisimulation for probabilis- tic systems: Characteristics and decidability,” Theoretical Computer Science (TCS), vol. 356, no. 3, pp. 325–355, 2006

    2006

  91. [99]

    A spectrum of approximate probabilistic bisimulations,

    T. Spork, C. Baier, J.-P. Katoen, J. Piribauer, and T. Quatmann, “A spectrum of approximate probabilistic bisimulations,” arXiv preprint arXiv:2407.07584, 2024. 17

    2024 arXiv

  92. [100]

    The algorithmics of bisimi- larity

    L. Aceto, A. Ingólfsdóttir, J. Srba et al., “The algorithmics of bisimi- larity.” Advanced Topics in Bisimulation and Coinduction , vol. 52, pp. 100–172, 2012

    2012

  93. [101]

    A behavioural pseudometric for probabilistic transition systems,

    F. Van Breugel and J. Worrell, “A behavioural pseudometric for probabilistic transition systems,” Theoretical Computer Science , vol. 331, no. 1, pp. 115–142, 2005

    2005

  94. [102]

    Regular abstractions for array systems,

    C.-D. Hong and A. W. Lin, “Regular abstractions for array systems,” Symposium on Principles of Programming Languages (POPL) , vol. 8, no. POPL, pp. 638–666, 2024

    2024

  95. [103]

    Computing inductive invariants of regular abstraction frameworks,

    P. Czerner, J. Esparza, V . Krasotin, and C. Welzel-Mohr, “Computing inductive invariants of regular abstraction frameworks,” arXiv preprint arXiv:2404.10752, 2024

    2024 arXiv

Pith tools

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