A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown...A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.展开更多
This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG ...This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG K_1 K_2 … RF, such that L (RG)<L (K_1)<L (K_2) < … < L (RF), where RG, RF are regular program class and finitely generated recursively enumerable program class respectively, and L (K) is the first order dynamic logic of program class K.展开更多
I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself o...I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical展开更多
基金This work was partially supported by the National Natural Science Foundationof China (Grant No. 69833020) the National High Technology Development Program of China (Grant No. 2002AA144050)the National Grand Fundamental Research 973 Program of China
文摘A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.
基金Supported by HTP863 the fund of Beijing laboratory of cognitive science
文摘This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG K_1 K_2 … RF, such that L (RG)<L (K_1)<L (K_2) < … < L (RF), where RG, RF are regular program class and finitely generated recursively enumerable program class respectively, and L (K) is the first order dynamic logic of program class K.
基金Project supported by the National High Technique Planning Foundation
文摘I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical
