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 (SQUARE)

University of Oslo
Karlsruhe Institute of Technology

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	A Specification Logic for Programs in the Probabilistic Guarded Command Language
Antal sider	19
Vol/bind	13572
Forlag	Springer
Publikationsdato	okt. 2022
ISBN (Trykt)	978-3-031-17714-9
ISBN (Elektronisk)	978-3-031-17715-6
DOI	https://doi.org/10.1007/978-3-031-17715-6_24
Status	Udgivet - okt. 2022
Begivenhed	International Colloquium on Theoretical Aspects of Computing - Tbilisi, Georgien Varighed: 27 sep. 2022 → 30 sep. 2022 Konferencens nummer: 19 https://viam.science.tsu.ge/clas2022/ictac/

Konference

Konference	International Colloquium on Theoretical Aspects of Computing
Nummer	19
Land/Område	Georgien
By	Tbilisi
Periode	27/09/2022 → 30/09/2022
Internetadresse	https://viam.science.tsu.ge/clas2022/ictac/

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

Emneord

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

Adgang til dokumentet

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

22-ictac-preprintIndsendt manuskript, 527 KBLicens: Ikke-specificeret

https://arxiv.org/pdf/2205.04822.pdfLicens: Ikke-specificeret

Citationsformater

@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. i A Specification Logic for Programs in the Probabilistic Guarded Command Language. bind 13572, Springer, Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022, International Colloquium on Theoretical Aspects of Computing, Tbilisi, Georgien, 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. Bind 13572 Springer, 2022. (Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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. I A Specification Logic for Programs in the Probabilistic Guarded Command Language. Bind 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

Konference

Emneord

Adgang til dokumentet

Fingeraftryk

Citationsformater