An Axiom System of Probabilistic Mu-Calculus

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

作者机构：College of Computer ScienceNational University of Defense TechnologyChangsha 410073China State Key Laboratory of Computer ScienceInstitute of SoftwareChinese Academy of SciencesBeijing 100190China University of Chinese Academy of SciencesBeijing 100039China Institute of Intelligent SoftwareGuangzhou 511458China 

出 版 物：《Tsinghua Science and Technology》 (清华大学学报（自然科学版（英文版）)

年 卷 期：2022年第27卷第2期

页      面：372-385页

核心收录：

学科分类：02[经济学] 0202[经济学-应用经济学] 020208[经济学-统计学] 07[理学] 0714[理学-统计学（可授理学、经济学学位）] 070103[理学-概率论与数理统计] 0701[理学-数学] 070101[理学-基础数学] 

基　　金：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) 

主　　题：PμTL axiom system aconjunctive formula tableau approach 

摘      要：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 *** of this logic,such as expressiveness and satisfiability decision,have been studied *** consider another important problem:the axiomatization of that *** extending the approaches of Kozen and Walukiewicz,we present an axiom system for Pμ*** addition,we show that the axiom system is complete for aconjunctive formulas.