ausblenden:
Schlagwörter:
Computer Science, Software Engineering, cs.SE,Computer Science, Logic in Computer Science, cs.LO
Zusammenfassung:
Probabilistic bisimulation is a fundamental notion of process equivalence for
probabilistic systems. Among others, it has important applications including
formalizing the anonymity property of several communication protocols. There is
a lot of work on verifying probabilistic bisimulation for finite systems. This
is however not the case for parameterized systems, where the problem is in
general undecidable. In this paper we provide a generic framework for reasoning
about probabilistic bisimulation for parameterized systems. Our approach is in
the spirit of software verification, wherein we encode proof rules for
probabilistic bisimulation and use a decidable first-order theory to specify
systems and candidate bisimulation relations, which can then be checked
automatically against the proof rules. As a case study, we show that our
framework is sufficiently expressive for proving the anonymity property of the
parameterized dining cryptographers protocol and the parameterized grades
protocol, when supplied with a candidate regular bisimulation relation. Both of
these protocols hitherto could not be verified by existing automatic methods.
Moreover, with the help of standard automata learning algorithms, we show that
the candidate relations can be synthesized fully automatically, making the
verification fully automated.
