Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

• URL: http://arxiv.org/abs/2505.09963v1
• Date: Thu, 15 May 2025 04:56:53 GMT
• Title: Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
• Authors: Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar,
• Abstract summary: Bisimulation is crucial for verifying process equivalence in probabilistic systems.<n>This paper presents a novel framework for analyzing bisimulation in infinite families of finite-state probabilistic systems.<n>We show that essential properties like anonymity and uniformity can be encoded and verified within this framework.
• Score: 5.806034991979994
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification [14.558484523699748]
  We address the problem of formally verifying the robustness of NeSy probabilistic reasoning systems.<n>We show that a decision version of the core computation is $mathrmNPmathrmPP$-complete.<n>We propose the first approach for approximate, relaxation-based verification of probabilistic NeSy systems.
  arXiv  Detail & Related papers  (2025-02-05T15:29:41Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Probabilistic Numeric SMC Sampling for Bayesian Nonlinear System Identification in Continuous Time [0.0]
  In engineering, accurately modeling nonlinear dynamic systems from data contaminated by noise is both essential and complex. The integration of continuous-time ordinary differential equations (ODEs) is crucial for aligning theoretical models with discretely sampled data. This paper demonstrates the application of a probabilistic numerical method for solving ODEs in the joint parameter-state identification of nonlinear dynamic systems.
  arXiv  Detail & Related papers  (2024-04-19T14:52:14Z)
• Inferentialist Resource Semantics [48.65926948745294]
  This paper shows how inferentialism enables a versatile and expressive framework for resource semantics.<n>How inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications.<n>This integration enables reasoning about shared and separated resources in intuitive and familiar ways.
  arXiv  Detail & Related papers  (2024-02-14T14:54:36Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Logical Credal Networks [87.25387518070411]
  This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability. We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
  arXiv  Detail & Related papers  (2021-09-25T00:00:47Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
  Probabilistic sentential decision diagrams are logic circuits where the inputs of disjunctive gates are annotated by probability values. We develop the credal sentential decision diagrams, a generalisation of their probabilistic counterpart that allows for replacing the local probabilities with credal sets of mass functions. For a first empirical validation, we consider a simple application based on noisy seven-segment display images.
  arXiv  Detail & Related papers  (2020-08-19T16:04:34Z)
• Verification of ML Systems via Reparameterization [6.482926592121413]
  We show how a probabilistic program can be automatically represented in a theorem prover. We also prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
  arXiv  Detail & Related papers  (2020-07-14T02:19:25Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.