Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Wojciech Różowski; Tobias Kappé; Dexter Kozen; Todd Schmid; Alexandra Silva

doi:10.4230/LIPIcs.ICALP.2023.136

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Wojciech Różowski^*, Tobias Kappé^*, Dexter Kozen^*, Todd Schmid^*, Alexandra Silva^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n³ log n) time via a generic partition refinement algorithm.

Original language	English
Title of host publication	50th International Colloquium on Automata, Languages, and Programming, ICALP 2023
Editors	Kousha Etessami, Uriel Feige, Gabriele Puppis
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages	20
Volume	261
ISBN (Electronic)	9783959772785
DOIs	https://doi.org/10.4230/LIPIcs.ICALP.2023.136
Publication status	Published - Jul 2023
Event	50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023 - Paderborn, Germany Duration: 10 Jul 2023 → 14 Jul 2023 https://icalp2023.cs.upb.de/

Publication series

Series	Leibniz International Proceedings in Informatics, LIPIcs
Volume	261
ISSN	1868-8969

Conference

Conference	50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023
Country/Territory	Germany
City	Paderborn
Period	10/07/23 → 14/07/23
Internet address	https://icalp2023.cs.upb.de/

Keywords

coalgebra
completeness
Kleene Algebra with Tests
program equivalence

Access to Document

10.4230/LIPIcs.ICALP.2023.136Licence: CC BY

https://arxiv.org/abs/2305.01755Licence: CC BY

Cite this

Różowski, W., Kappé, T., Kozen, D., Schmid, T., & Silva, A. (2023). Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In K. Etessami, U. Feige, & G. Puppis (Eds.), 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023 (Vol. 261). Article 136 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ICALP.2023.136

Różowski, Wojciech ; Kappé, Tobias ; Kozen, Dexter et al. / Probabilistic Guarded KAT Modulo Bisimilarity : Completeness and Complexity. 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023. editor / Kousha Etessami ; Uriel Feige ; Gabriele Puppis. Vol. 261 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2023. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 261).

@inproceedings{580a3463d218416a9fe7c3a25bc5e241,

title = "Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity",

abstract = "We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n3 log n) time via a generic partition refinement algorithm.",

keywords = "coalgebra, completeness, Kleene Algebra with Tests, program equivalence",

author = "Wojciech R{\'o}{\.z}owski and Tobias Kapp{\'e} and Dexter Kozen and Todd Schmid and Alexandra Silva",

note = "Funding Information: Funding This work was partially supported by ERC grant Autoprobe (no. 101002697; R{\'o}{\.z}owski, Schmid and Silva), the EU{\textquoteright}s Horizon 2020 research and innovation program under Marie Sk{\l}odowska-Curie grant VERLAN (no. 101027412; Kapp{\'e}), and NSF grant CCF-2008083 (Kozen). Publisher Copyright: {\textcopyright} Wojciech R{\'o}{\.z}owski, Tobias Kapp{\'e}, Dexter Kozen, Todd Schmid, and Alexandra Silva.; 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023 ; Conference date: 10-07-2023 Through 14-07-2023",

year = "2023",

month = jul,

doi = "10.4230/LIPIcs.ICALP.2023.136",

language = "English",

volume = "261",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "Kousha Etessami and Uriel Feige and Gabriele Puppis",

booktitle = "50th International Colloquium on Automata, Languages, and Programming, ICALP 2023",

address = "Germany",

url = "https://icalp2023.cs.upb.de/",

}

Różowski, W, Kappé, T, Kozen, D, Schmid, T & Silva, A 2023, Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. in K Etessami, U Feige & G Puppis (eds), 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023. vol. 261, 136, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Leibniz International Proceedings in Informatics, LIPIcs, vol. 261, 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, Paderborn, North Rhine-Westphalia, Germany, 10/07/23. https://doi.org/10.4230/LIPIcs.ICALP.2023.136

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. / Różowski, Wojciech; Kappé, Tobias; Kozen, Dexter et al.
50th International Colloquium on Automata, Languages, and Programming, ICALP 2023. ed. / Kousha Etessami; Uriel Feige; Gabriele Puppis. Vol. 261 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2023. 136 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 261).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Probabilistic Guarded KAT Modulo Bisimilarity

T2 - 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023

AU - Różowski, Wojciech

AU - Kappé, Tobias

AU - Kozen, Dexter

AU - Schmid, Todd

AU - Silva, Alexandra

N1 - Funding Information: Funding This work was partially supported by ERC grant Autoprobe (no. 101002697; Różowski, Schmid and Silva), the EU’s Horizon 2020 research and innovation program under Marie Skłodowska-Curie grant VERLAN (no. 101027412; Kappé), and NSF grant CCF-2008083 (Kozen). Publisher Copyright: © Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva.

PY - 2023/7

Y1 - 2023/7

N2 - We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n3 log n) time via a generic partition refinement algorithm.

AB - We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n3 log n) time via a generic partition refinement algorithm.

KW - coalgebra

KW - completeness

KW - Kleene Algebra with Tests

KW - program equivalence

U2 - 10.4230/LIPIcs.ICALP.2023.136

DO - 10.4230/LIPIcs.ICALP.2023.136

M3 - Conference Article in proceeding

AN - SCOPUS:85167350253

VL - 261

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023

A2 - Etessami, Kousha

A2 - Feige, Uriel

A2 - Puppis, Gabriele

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Y2 - 10 July 2023 through 14 July 2023

ER -

Różowski W, Kappé T, Kozen D, Schmid T, Silva A. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In Etessami K, Feige U, Puppis G, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023. Vol. 261. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2023. 136. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 261). doi: 10.4230/LIPIcs.ICALP.2023.136

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this