Probabilistic guarded KAT Modulo bisimilarity: completeness and complexity

DOI10.4230/LIPICS.ICALP.2023.136MaRDI QIDQ6638146zbMATH OpenFDO

Authors Wojciech Różowski, Tobias Kappé, Dexter Kozen, Alexandra Silva

Publication date 14 November 2024

Full work available at URL https://doi.org/10.4230/LIPICS.ICALP.2023.136

zbMATH Keywords

coalgebracompletenessKleene algebra with testsprogram equivalence

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cited in

(10)

• Kleene algebra of weighted programs with domain
• A complete quantitative axiomatisation of behavioural distance of regular expressions
• On propositional program equivalence (extended abstract)
• A general completeness theorem for skip-free star algebras
• BiGKAT: an algebraic framework for relational verification of probabilistic programs
• A completeness theorem for probabilistic regular expressions
• The relational machine calculus
• A cyclic proof system for guarded Kleene algebra with tests
• A Kleene algebra with tests for union bound reasoning about probabilistic programs
• Simulation quotients simulating bisimulation quotients

This page was built for publication: Probabilistic guarded KAT Modulo bisimilarity: completeness and complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6638146)