面向传值进程的谓词μ-演算与FO(HML)的完备推演系统  

A Predicate μ-Calculus for Value-Passing Processes and A Complete Deductive System for FO(HML)

作　　者：薛锐[1] 林惠民[1] 

机构地区：[1]中国科学院软件研究所计算机科学实验室,北京100083

出　　处：《计算机学报》2002年第6期561-569,共9页Chinese Journal of Computers

基　　金：国家自然科学基金 (6983 3 0 2 0 );山西省归国留学生基金;中国科学院软件研究所开放实验室青年科学基金资助

摘　　要：作者提出一个谓词μ-演算系统 ,目的在于描述传值进程的性质 .该系统的公式和谓词相互递归定义 ,谓词中含有抽象式、谓词变元以及最大和最小不动点 .其语义模型是带赋值的符号迁移图所诱导的迁移系统 .并且该系统包含 Hennessy- Milner逻辑的一阶扩充 FO(HML )作为子系统 .作者用例子说明了本演算系统在表达传值进程性质方面的优越性 .该文后半部分主要给出了 FO(HML )的一个推演系统 ,并运用判定树 (Tableau)的方法 。A predicate μ calculus is proposed for describing properties of value passing processes. It is a first order logic with fixpoints. Propositions and predicates are mutually recursively defined. Predicates are functions from values to propositions, which has three forms: predicate variables, abstractions, as well as greatest and least fixed points. Formulae are interpreted over transition systems induced by symbolic transition graphs with assignments. For the finite fragment of the logic, which is named FO(HML) and similar to the modal logic proposed by Hennessy and Liu, a Gentzen style deductive system is presented, and its completeness proved using tableau technique.

关 键 词：传值进程 谓词μ-演算 FO 完备推演系统 计算机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]