Towards a Proof System for Probabilistic Dynamic Logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910722876768256 |
|---|---|
| author | Johnsen, Einar Broch Kamburjan, Eduard Pardo, Raúl Voogd, Erik Wąsowski, Andrzej |
| author_facet | Johnsen, Einar Broch Kamburjan, Eduard Pardo, Raúl Voogd, Erik Wąsowski, Andrzej |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_00906 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards a Proof System for Probabilistic Dynamic Logic Johnsen, Einar Broch Kamburjan, Eduard Pardo, Raúl Voogd, Erik Wąsowski, Andrzej Logic in Computer Science 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. |
| title | Towards a Proof System for Probabilistic Dynamic Logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2412.00906 |