Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910945065828352 |
|---|---|
| author | Hong, Chih-Duo Lin, Anthony W. Rümmer, Philipp Majumdar, Rupak |
| author_facet | Hong, Chih-Duo Lin, Anthony W. Rümmer, Philipp Majumdar, Rupak |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_09963 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification Hong, Chih-Duo Lin, Anthony W. Rümmer, Philipp Majumdar, Rupak Software Engineering Formal Languages and Automata Theory 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. |
| title | Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification |
| topic | Software Engineering Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2505.09963 |