Abstract
Markov processes are a fundamental model of probabilistic transition systems and are the underlying semantics of probabilistic programs.We give an algebraic axiomatisation of Markov processes using the framework of quantitative equational logic introduced in [13]. We present the theory in a structured way using work of Hyland et al. [9] on combining monads. We take the interpolative barycentric algebras of [13] which captures the Kantorovich metric and combine it with a theory of contractive operators to give the required axiomatisation of Markov processes both for discrete and continuous state spaces. This work apart from its intrinsic interest shows how one can extend the general notion of combining effects to the quantitative setting.
Original language | English |
---|---|
Title of host publication | LICS '18 : Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science |
Place of Publication | New York, NY. |
Pages | 679-688 |
Number of pages | 10 |
DOIs | |
Publication status | Published - 9 Jul 2018 |
Event | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018 |
Conference
Conference | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |
---|---|
Country/Territory | United Kingdom |
City | Oxford |
Period | 9/07/18 → 12/07/18 |
Funding
This research was supported by grants from the Danish Council for Independent Research (ASAP, Project 4181-00360) and from NSERC (Canada). We acknowledge the stimulating atmosphere of the Bellairs Research Institute where part of this research was carried out.
Keywords
- combining monads
- equational logic
- Markov processes
- quantitative reasoning