Towards a Proof System for Probabilistic Dynamic Logic

Einar Broch Johnsen, Eduard Kamburjan, Raul Pardo, Erik Voogd, Andrzej Wąsowski

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationTowards a Proof System for Probabilistic Dynamic Logic
Volume15260
PublisherSpringer Nature Switzerland
Publication date2024
Pages322-338
DOIs
Publication statusPublished - 2024
EventColloquium on Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday - University of Aachen, Aachen, Germany
Duration: 7 Nov 2024 → …

Other

OtherColloquium on Principles of Verification: Cycling the Probabilistic Landscape
LocationUniversity of Aachen
Country/TerritoryGermany
CityAachen
Period07/11/2024 → …

Keywords

  • Dynamic logic
  • Probabilistic programs
  • Deductive verification

Fingerprint

Dive into the research topics of 'Towards a Proof System for Probabilistic Dynamic Logic'. Together they form a unique fingerprint.

Cite this