Towards a Proof System for Probabilistic Dynamic Logic
| Autor: | Johnsen, Einar Broch, Kamburjan, Eduard, Pardo, Raúl, Voogd, Erik, Wąsowski, Andrzej |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | Whereas the semantics of probabilistic languages has been extensively studied, specification languages for their properties have received less attention -- with the notable exception of recent and on-going efforts by Joost-Pieter Katoen and collaborators. In this paper, we revisit probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. Building on dynamic logic, pDL can express both first-order state properties and probabilistic reachability properties. In this paper, we report on work in progress towards a deductive proof system for pDL. This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution. Comment: Pre-print of paper appearing in "In Principles of Verification: Cycling the Probabilistic Landscape-Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, 2024" (https://doi.org/10.1007/978-3-031-75783-9_13) |
| Databáze: | arXiv |
| Externí odkaz: |
|