An Axiom System of Probabilistic Mu-Calculus  

作　　者：Wanwei Liu Junnan Xu David N.Jansen Andrea Turrini Lijun Zhang 

机构地区：[1]College of Computer Science,National University of Defense Technology,Changsha 410073,China [2]State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China [3]University of Chinese Academy of Sciences,Beijing 100039,China [4]Institute of Intelligent Software,Guangzhou 511458,China

出　　处：《Tsinghua Science and Technology》2022年第2期372-385,共14页清华大学学报（自然科学版（英文版）

基　　金：supported by the National Science Foundation of China(No.61872371);the National Science Foundation of China(Nos.61761136011 and 61836005);the Open Fund from the State Key Laboratory of High Performance Computing of China(HPCL)(No.2020001-07);the National Key Research and Development Program of China(No.2018YFB0204301);supported by the Guangdong Science and Technology(No.2018B010107004)。

摘　　要：Mu-calculus(a.k.a.μTL)is built up from modal/dynamic logic via adding the least fixpoint operatorμ.This type of logic has attracted increasing attention since Kozen’s seminal work.PμTL is a succinct probabilistic extension of the standardμTL obtained by making the modal operators probabilistic.Properties of this logic,such as expressiveness and satisfiability decision,have been studied elsewhere.We consider another important problem:the axiomatization of that logic.By extending the approaches of Kozen and Walukiewicz,we present an axiom system for PμTL.In addition,we show that the axiom system is complete for aconjunctive formulas.

关 键 词：PμTL axiom system aconjunctive formula tableau approach 

分 类 号：O172[理学—数学] O211[理学—基础数学]