Gu, T;
Silva, A;
Zanasi, F;
(2020)
Hennessy-Milner Results for Probabilistic PDL.
In:
Electronic Notes in Theoretical Computer Science.
(pp. pp. 283-304).
Elsevier: Duivendrecht, Netherlands.
Preview |
Text
Zanasi_1-s2.0-S1571066120300694-main.pdf - Published Version Download (342kB) | Preview |
Abstract
Kozen introduced probabilistic propositional dynamic logic (PPDL) in 1985 as a compositional framework to reason about probabilistic programs. In this paper we study expressiveness for PPDL and provide a series of results analogues to the classical HennessyMilner theorem for modal logic. First, we show that PPDL charaterises probabilistic trace equivalence of probabilistic automata (with outputs). Second, we show that PPDL can be mildly extended to yield a characterisation of probabilistic state bisimulation for PPDL models. Third, we provide a different extension of PPDL, this time characterising probabilistic event bisimulation.
| Type: | Proceedings paper |
|---|---|
| Title: | Hennessy-Milner Results for Probabilistic PDL |
| Event: | 36th Conference on the Mathematical Foundations of Programming Languages Semantics (MFPS) was co-located with the 17th International Conference on Quantum Programming Physics and Logic (QPL) |
| Location: | ELECTR NETWORK |
| Dates: | 02 June 2020 - 06 June 2020 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1016/j.entcs.2020.09.014 |
| Publisher version: | https://doi.org/10.1016/j.entcs.2020.09.014 |
| Language: | Albanian |
| Additional information: | © 2020 The Author(s). Published by Elsevier. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/). |
| Keywords: | Probabilistic Propositional Dynamic Logic, Probabilistic bisimulation, Hennessy-Milner property, BISIMULATION |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10117222 |
Archive Staff Only
 |
View Item |
