文章基本信息

标题：Probabilistic Mu-Calculus: Decidability and Complete Axiomatization
本地全文：下载
作者：Kim G. Larsen ; Radu Mardare ; Bingtian Xue 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：65
页码：25:1-25:18
DOI：10.4230/LIPIcs.FSTTCS.2016.25
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We introduce a version of the probabilistic mu-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 meta-properties. 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.
关键词：Markov process; probabilistic modal mu-calculus; n-ary (in-)equational modalities; satisfiability; axiomatization