Hong, Chih-Duo and Lin, Anthony W. and Rümmer, Philipp and Majumdar, Rupak (2025) Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 51 (6). pp. 1801-1817. ISSN 0098-5589, 1939-3520
Full text not available from this repository. (Request a copy)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.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | EQUIVALENCE; INFERENCE; AUTOMATA; Probabilistic logic; Cryptography; Markov decision processes; Software systems; Cognition; Training; Model checking; Inference algorithms; Finite element analysis; Encoding; Anonymity; automata learning; parameterized system; probabilistic bisimulation; probabilistic model checking; regular model checking; uniformity |
| Subjects: | 000 Computer science, information & general works > 004 Computer science |
| Divisions: | Informatics and Data Science > General computer science > Theoretische Informatik (Prof. Dr. Philipp Rümmer) |
| Depositing User: | Dr. Gernot Deinzer |
| Date Deposited: | 10 Jun 2026 08:44 |
| Last Modified: | 10 Jun 2026 08:44 |
| URI: | https://pred.uni-regensburg.de/id/eprint/66880 |
Actions (login required)
 |
View Item |
