| dc.contributor | 資管系 | - |
| dc.creator (作者) | 洪智鐸 | - |
| dc.creator (作者) | Hong, Chih-Duo;Lin, Anthony W.;Rümmer, Philipp;Majumdar, Rupak | - |
| dc.date (日期) | 2025-06 | - |
| dc.date.accessioned | 27-May-2025 11:04:38 (UTC+8) | - |
| dc.date.available | 27-May-2025 11:04:38 (UTC+8) | - |
| dc.date.issued (上傳時間) | 27-May-2025 11:04:38 (UTC+8) | - |
| dc.identifier.uri (URI) | https://nccur.lib.nccu.edu.tw/handle/140.119/157080 | - |
| dc.description.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. | - |
| dc.format.extent | 104 bytes | - |
| dc.format.mimetype | text/html | - |
| dc.relation (關聯) | IEEE Transactions on Software Engineering, Vol.51, No.6, pp.1801-1817 | - |
| dc.title (題名) | Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification | - |
| dc.type (資料類型) | article | - |
| dc.identifier.doi (DOI) | 10.1109/TSE.2025.3567423 | - |
| dc.doi.uri (DOI) | https://doi.org/10.1109/TSE.2025.3567423 | - |
