Różowski, W;
Kappé, T;
Kozen, D;
Schmid, T;
Silva, A;
(2023)
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity.
In:
Leibniz International Proceedings in Informatics (LIPIcs).
Leibniz-Zentrum für Informatik: Paderborn, Germany.
Preview |
Text
LIPIcs-ICALP-2023-136.pdf - Published Version Download (990kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity |
| Event: | The 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.ICALP.2023.136 |
| Publisher version: | https://www.dagstuhl.de/en/publishing/series/detai... |
| Language: | English |
| Additional information: | This work is licensed under a Creative Commons Attribution 4.0 International License. The images or other third-party material in this article are included in the Creative Commons license, unless indicated otherwise in the credit line; if the material is not included under the Creative Commons license, users will need to obtain permission from the license holder to reproduce the material. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/ |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10175566 |
Archive Staff Only
 |
View Item |
