A Specification Logic for Programs in the Probabilistic Guarded Command Language

Raúl Pardo; Einar Broch Johnsen; Ina Schaefer; Andrzej Wasowski

doi:10.1007/978-3-031-17715-6_24

A Specification Logic for Programs in the Probabilistic Guarded Command Language

Raúl Pardo
, Einar Broch Johnsen
, Ina Schaefer
, Andrzej Wasowski

Software Quality Research

University of Oslo
Karlsruhe Institute of Technology

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.

Original language	English
Title of host publication	A Specification Logic for Programs in the Probabilistic Guarded Command Language
Number of pages	19
Volume	13572
Publisher	Springer
Publication date	Oct 2022
ISBN (Print)	978-3-031-17714-9
ISBN (Electronic)	978-3-031-17715-6
DOIs	https://doi.org/10.1007/978-3-031-17715-6_24
Publication status	Published - Oct 2022
Event	International Colloquium on Theoretical Aspects of Computing - Tbilisi, Georgia Duration: 27 Sept 2022 → 30 Sept 2022 Conference number: 19 https://viam.science.tsu.ge/clas2022/ictac/

Conference

Conference	International Colloquium on Theoretical Aspects of Computing
Number	19
Country/Territory	Georgia
City	Tbilisi
Period	27/09/2022 → 30/09/2022
Internet address	https://viam.science.tsu.ge/clas2022/ictac/

Series	Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022

Keywords

Probabilistic Dynamic Logic
Probabilistic Guarded Command Language
First-Order State Properties
Probabilistic Reachability
Markov Decision Processes

Access to Document

10.1007/978-3-031-17715-6_24

22-ictac-preprintSubmitted manuscript, 527 KBLicence: Unspecified

https://arxiv.org/pdf/2205.04822.pdfLicence: Unspecified

Cite this

@inproceedings{5bb0e63bd32f479b9961ed759f0bc6ed,

title = "A Specification Logic for Programs in the Probabilistic Guarded Command Language",

abstract = "The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.",

keywords = "Probabilistic Dynamic Logic, Probabilistic Guarded Command Language, First-Order State Properties, Probabilistic Reachability, Markov Decision Processes, Probabilistic Dynamic Logic, Probabilistic Guarded Command Language, First-Order State Properties, Probabilistic Reachability, Markov Decision Processes",

author = "Ra{\'u}l Pardo and \{Broch Johnsen\}, Einar and Ina Schaefer and Andrzej Wasowski",

year = "2022",

month = oct,

doi = "10.1007/978-3-031-17715-6\_24",

language = "English",

isbn = "978-3-031-17714-9",

volume = "13572",

series = "Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022",

publisher = "Springer",

booktitle = "A Specification Logic for Programs in the Probabilistic Guarded Command Language",

address = "Germany",

note = "International Colloquium on Theoretical Aspects of Computing, ICTAC ; Conference date: 27-09-2022 Through 30-09-2022",

url = "https://viam.science.tsu.ge/clas2022/ictac/",

}

Pardo, R, Broch Johnsen, E, Schaefer, I & Wasowski, A 2022, A Specification Logic for Programs in the Probabilistic Guarded Command Language. in A Specification Logic for Programs in the Probabilistic Guarded Command Language. vol. 13572, Springer, Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022, International Colloquium on Theoretical Aspects of Computing, Tbilisi, Georgia, 27/09/2022. https://doi.org/10.1007/978-3-031-17715-6_24

A Specification Logic for Programs in the Probabilistic Guarded Command Language. / Pardo, Raúl; Broch Johnsen, Einar; Schaefer, Ina et al.
A Specification Logic for Programs in the Probabilistic Guarded Command Language. Vol. 13572 Springer, 2022. (Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - A Specification Logic for Programs in the Probabilistic Guarded Command Language

AU - Pardo, Raúl

AU - Broch Johnsen, Einar

AU - Schaefer, Ina

AU - Wasowski, Andrzej

N1 - Conference code: 19

PY - 2022/10

Y1 - 2022/10

N2 - The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.

AB - The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.

KW - Probabilistic Dynamic Logic

KW - Probabilistic Guarded Command Language

KW - First-Order State Properties

KW - Probabilistic Reachability

KW - Markov Decision Processes

KW - Probabilistic Dynamic Logic

KW - Probabilistic Guarded Command Language

KW - First-Order State Properties

KW - Probabilistic Reachability

KW - Markov Decision Processes

U2 - 10.1007/978-3-031-17715-6_24

DO - 10.1007/978-3-031-17715-6_24

M3 - Article in proceedings

SN - 978-3-031-17714-9

VL - 13572

T3 - Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022

BT - A Specification Logic for Programs in the Probabilistic Guarded Command Language

PB - Springer

T2 - International Colloquium on Theoretical Aspects of Computing

Y2 - 27 September 2022 through 30 September 2022

ER -

Pardo R, Broch Johnsen E, Schaefer I, Wasowski A. A Specification Logic for Programs in the Probabilistic Guarded Command Language. In A Specification Logic for Programs in the Probabilistic Guarded Command Language. Vol. 13572. Springer. 2022. (Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022). doi: 10.1007/978-3-031-17715-6_24

A Specification Logic for Programs in the Probabilistic Guarded Command Language

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this