Projects per year
Abstract
We introduce a version of the probabilistic µ-calculus (PMC) built on top of a probabilistic modal logic that allows encoding n-ary inequational conditions on transition probabilities. PMC extends previously studied calculi and we prove that, despite its expressiveness, it enjoys a series of good metaproperties. Firstly, we prove the decidability of satisfiability checking by establishing the small model property. An algorithm for deciding the satisfiability problem is developed. As a second major result, we provide a complete axiomatization for the alternation-free fragment of PMC. The completeness proof is innovative in many aspects combining various techniques from topology and model theory.
Original language | English |
---|---|
Title of host publication | 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science : FSTTCS 2016, December 13-15, 2016, Chennai, India |
Number of pages | 18 |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | 2016 |
Pages | 25:1-25:18 |
ISBN (Print) | 978-3-95977-027-9 |
DOIs | |
Publication status | Published - 2016 |
Event | 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science - Chennai Mathematical Institute, Chennai, India Duration: 13 Dec 2016 → 15 Dec 2016 Conference number: 36th http://www.fsttcs.org/ |
Conference
Conference | 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science |
---|---|
Number | 36th |
Location | Chennai Mathematical Institute |
Country/Territory | India |
City | Chennai |
Period | 13/12/2016 → 15/12/2016 |
Internet address |
Series | Leibniz International Proceedings in Informatics |
---|---|
Volume | 65 |
ISSN | 1868-8969 |
Fingerprint
Dive into the research topics of 'Probabilistic Mu-Calculus: Decidability and Complete Axiomatization'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Approximate Reasoning for Stochastic Markovian Systems
Mardare, R. & Larsen, K. G.
01/11/2015 → 31/10/2019
Project: Research