面向传值进程的一阶模态逻辑的可判定性与模型检测
摘要
对于面向传值进程的Hennessy—Milner逻辑的一阶扩充HML(FO),给出了基于带赋值的符号迁移图的语义解释.证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的,并且讨论了判定的复杂性.最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.
出处
《中国科学（E辑）》
CSCD
北大核心
2003年第2期97-110,共14页
Science in China(Series E)
基金
国家自然科学基金(批准号:69833020)
国家高技术研究发展计划(863计划
2002AA144050)
国家"九七三"重点研究发展规划(G1999035802)
山西师范大学山西省归国留学生基金资助项目
参考文献18
-
1[1]Milner R. Communication and Concurrency. Englewood Cliffs: Prentice Hall, 1989
-
2[2]Hennessy M, Milner R. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 1985,32(1): 137～161
-
3[3]Bloom S L, Troeger D R. A logical characterization of observation equivalence. Theoretical Computer Science,1985, 35:43～53
-
4[4]Graf S, Sifakis J. A modal characterization of observation of finite terms of CCS. Information and Control,1986, 68(1-3): 125～145
-
5[5]Milner R. A modal characterization of observable machine-behavior. In: Lecture Notes in Computer Science, Vol 22. Berlin: Springer, 1981
-
6[6]Hennessy M, Liu X. A modal logic for message passing processes. Acta Informatica, 1995, 32:375～393
-
7[7]Larsen K G. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Sciences, 1990, 72:265～288
-
8[8]Stirling C. Modal logics for communicating systems. Theoretical Computer Science, 1987, 49:311～347
-
9[9]Gradel E, Otto M. On logics with two variables. Theoretical Computer Sciences, 1999, 224:73～113
-
10[10]Lin H. Symbolic transition graph with assignment. In: Proc 7th Int Conf on Concurrency Theory, Pisa, Italy,August 1996. Lecture Notes in Computer Science, Vol 1119. Berlin: Springer-Verlag, 1996. 26～29
-
1胡世华.递归结构理论的形式系统和语句的可判定性——可解决性理论Ⅱ[J].中国科学（A辑）,1990,21(12):1235-1242.
-
2曹为理.关于半群簇的几个判定问题[J].兰州大学学报（自然科学版）,1994,30(4):64-67. 被引量：1
-
3张乐,裴道武,王三民.系统_n~*的逻辑性质及其应用[J].高校应用数学学报（A辑）,2011,26(2):247-252.
-
4潘海玉,张敏,陈仪香.基于完备剩余格的双标号转换系统[J].模糊系统与数学,2012,26(5):21-29. 被引量：4
-
5左春艳,禹长龙.广义Liénard系统的中心问题[J].河北科技大学学报,2013,34(2):125-127.
-
6ZHANG Wei.On the decidability of open logic[J].Science in China(Series F),2009,52(8):1283-1291. 被引量：1
-
7朱洪,卢先捷,RichardDenis.算术结构的不可判定性[J].数学年刊（A辑）,1997,1(6):667-672.
-
8薛锐.完备布尔代数理论的计算复杂性[J].北京师范大学学报（自然科学版）,1999,35(3):303-309.
-
9汪国武,沈应兄,潘海玉.量化转换系统的格值语言包含关系[J].模糊系统与数学,2016,30(5):50-59.
-
10沈恩绍.大、小E.C.结构的可判定性[J].数学学报（中文版）,1997,40(3):465-472.
