UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Hennessy-Milner Results for Probabilistic PDL

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. Green open access

[thumbnail of Zanasi_1-s2.0-S1571066120300694-main.pdf]
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
Downloads since deposit
22Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item