现代模态逻辑在计算机科学中的应用研究

摘要/Abstract

摘要： 现代模态逻辑是在经典数理逻辑基础上发展起来的,主要包括狭义模态逻辑、道义逻辑、认知逻辑、信念逻辑、时态逻辑与动态逻辑。克里普克语义模型的建立,使得模态逻辑成为现代逻辑的重要分支之一,并成功应用到数学、经济学、社会科学、计算机科学和量子力学等众多领域。介绍了现代模态逻辑研究的主要内容,重点综述了现代模态逻辑在计算机科学的程序设计语言、知识表示与多代理系统以及模型检测、定理机器证明和非单调逻辑5个方面的应用,阐述了现代模态逻辑在计算机科学领域的研究目标、研究进展和发展趋势,最后指出现代模态逻辑研究中存在的问题,并预测其未来可能的研究与发展方向。

关键词: 模态逻辑,可能世界,多Agent系统,模型检测,量子力学

Abstract: Modern modal logic is set up on the basis of classical mathematical logic,and mainly includes narrow modal logic,deontic logic,epistemic logic,belief logic,temporal logic and dynamic logic．With the emergence of the Kripke semantic model,modal logic has become one of the most important branches of logics,and has been successfully applied to many fields such as mathematics,economics,social science,computer science and quantum mechanics．This paper introduced the main contents of modern modal logic,and mainly overviewed the following three application aspects of modern modal logic which include programming language,knowledge representation,multi-agent system,model checking,mechanical theorem proving and no monotonic logic．At the same time,this paper presented the research targets,the research advances and the development trend of modern modal logic．At last,the paper pointed out the problems in research on modern modal logic and suggested the trend of future development and research.

Key words: Modal logic,Possible world,Multi-agent system,Model checking,Quantum mechanics

陈志远,黄少滨,韩丽丽. 现代模态逻辑在计算机科学中的应用研究[J]. 计算机科学, 2013, 40(Z6): 70-76. https://doi.org/

CHEN Zhi-yuan,HUANG Shao-bin and HAN Li-li. Research on Applications of Modern Modal Logic in Computer Science[J]. Computer Science, 2013, 40(Z6): 70-76. https://doi.org/

参考文献

[1] Perkins M R．Modal expressions in English[M]．Ablex Publi-shing Corporation Oates,1983:22-28
[2] 弓肇祥．广义模态逻辑[M]．北京:中国社会科学出版社,1993:112-119
[3] 周北海．模态逻辑导论[M]．北京:北京大学出版社,1997:32-41
[4] Hughes G E,Cresswell M J．A new introduction to modal logic[M]．Burns & Oates,1996:110-118
[5] Blackburn P,De Rijke M,Venema Y．Modal logic[M]．Cambridge Univ Pr,2002:88-93
[6] Bull R,Segerberg K．Basic modal logic[J]．Handbook of philo-sophical logic,1984,2:1-88
[7] Lewis C I IV．Implication and the algebra of logic[J]．Mind,1912,21(84):522
[8] Lewis C I V．Discussions:the calculus of strict implication[J]．Mind,1914,23(1):240
[9] Lewis C I,Langford C H．Symbolic logic[M]．The Century co.,1932:32-45
[10] Carnap R．Philosophy and logical syntax[M]．K．Paul,Trench,Trubner&Co.,ltd.,1935:135-146
[11] Carnap R．Testability and meaning[J]．Philosophy of science,1936,3(4):419-471
[12] Kanger S．On the characterization of modalities[J]．Theoria,1957,23(3):152-155
[13] Hintikka J．Models for modalities[M]．Reidel,1969:43-56
[14] Kripke S．Semantical considerations on modal logic[J]．Acta philosophica fennica,1963,16:83-94
[15] Von Wright G H I．DEONTIC LOGIC[J]．Mind,1951,60(237):1
[16] Hintikka J．Individuals,possible worlds,and epistemic logic[J]．Nous,1967,1(1):33-62
[17] Cocchiarella N B．Tense and Modal Logic:a study in the topology of temporal reference[J]．Unpublished Dissertation,UCLA,1966:12-18
[18] 周祯祥．现代模态逻辑的多元视野[J]．华南师范大学学报:社会科学版,2006(5):7-11
[19] Manna Z,Pnueli A．Verification of concurrent programs:Thetemporal framework[J]．The correctness problem in computer science,1981:215-273
[20] Manna Z,Pnueli A．The temporal logic of reactive and concurrent systems:Specification[M]．Springer,1992:231-234
[21] Prior A N.Now[J]．Nous,1968,2(2):101-119
[22] Rescher N,Urquhart A．Temporal logic[M]．New York:Springer-Verlag,1971:203-207
[23] 唐稚松．XYZ系统的设计思想[J]．软件学报,1990,1:47-54
[24] Zhu Xue-yang,T Zhi-song．A Temporal Logic-Based SoftwareArchitecture Description Language XYZ/ADL[J]．Journal of Software,2003,4:35-42
[25] 韩俊刚,王岩冰,沈武威．用 XYZ/E 语言描述和验证硬件的行为[J]．软件学报,1996,7(11):676-682
[26] 阎安,唐稚松．基于 XYZ/E的混成系统[J]．软件学报,2000,11(1):1-7
[27] 郭亮,唐稚松．XYZ/E面向对象程序语义概述[J]．软件学报,2003,14(3):356-361
[28] 张广泉,唐稚松．基于时序逻辑语言 XYZ/E 的软件体系结构描述方法[J]．淮阴师范学院学报:自然科学版,2002(1):26-31
[29] 朱雪阳,唐稚松．UML 活动图的时序逻辑语义[J]．计算机研究与发展,2005,42(9):1478-1484
[30] Nilsson N J,Automation A M．An Application of Artificial Intelligence Techniques[C]∥Proceedings of the 1st International Joint Conference on Artificial Intelligence．1969:509-520
[31] Winston P H．New progress in artificial intelligence[J]．AITR-310,1974:77-86
[32] Moore R C,Center S P．A formal theory of knowledge and action[J]．1984:226-238
[33] Moore R C,Center S P．Possible-world semantics for auto epistemic logic[J]．1984:116-128
[34] Wooldridge M,Jennings N R．Intelligent agents:Theory andpractice[J]．The knowledge engineering review,2009,10(02):115-152
[35] Nwana H S．Software agents:An overview[J]．The Knowledge Engineering Review,2009,11(3):205-244
[36] Wendt A E．The agent-structure problem in international relations theory[J]．International Organization,2009,41(3):335-370
[37] Cossentino M,Burrafato P,Lombardo S,et al．Introducing pattern reuse in the design of multi-agent systems[J]．Agent Technologies,Infrastructures,Tools,and Applications for E-Ser-vices,2010:107-120
[38] Jennings N R．Commitments and conventions:The foundation ofcoordination in multi-agent systems[J]．The knowledge engineering review,2009,8(3):223-250
[39] Cohen P R,Levesque H J．Intention is choice with commitment[J]．Artificial intelligence,1990,42(2/3):213-261
[40] Cohen P R,Levesque H J．Communicative actions for artificial agents[C]//Proceedings of the First International Conference on Multi-Agent Systems(ICMAS-95)．1995:65-72
[41] Rao A S,Georgeff M P．BDI agents:From theory to practice[C]∥Proceedings of the first international conference on multi-agent systems(ICMAS-95)．1995:312-319
[42] Konolige K,Pollack M E．A representation list theory of intention[C]//International Joint Conference on Artificial Intelligence．1993,13:390-390
[43] Gaspar G,Coelho H．Where do intentions come from?:A framework for goals and intentions adoption,derivation and evolution[J]．Progress in Artificial Intelligence,1995:115-127
[44] Queille J,Sifakis J．Specification and verification of concurrentsystems in CESAR[C]∥International Symposium on Programming．1982:337-351
[45] Clarke E M,Emerson E A．Design and verification of synchronization skeletons using branching time temporal logic[C]∥Proceedings of Workshop on Logic of Programs．2002:52-71
[46] Clarke E M,Grumberg O,Long D E．Model checking and ab-straction[J]．ACM Transactions on Programming Languages and Systems(TOPLAS),1994,16(5):1512-1542
[47] Long D E．Model checking,abstraction,and compositional verification[D]．Citeseer,1993
[48] Zheng H,Yao H,Yoneda T．Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement[J]．IEEE Transactions on Computers,2010,59(4):561-573
[49] De Moura L,Ruess H,Sorea M．Bounded model checking andinduction:From refutation to verification[C]∥Computer Aided Verification．2003:14-26
[50] Eén N,Sorensson N．Temporal induction by incremental SAT solving[J]．Electronic Notes in Theoretical Computer Science,2003,89(4):543-560
[51] McMillan K L．A methodology for hardware verification using compositional model checking[J]．Science of Computer Programming,2000,37(1-3):279-309
[52] Edelkamp S,Leue S,Lluch-Lafuente A．Directed explicit-statemodel checking in the validation of communication protocols[J]．International Journal on Software Tools for Technology Transfer(STTT),2004,5(2):247-267
[53] Argón P,Delzanno G,Mukhopadhyay S,et al．Model Checking Communication Protocols[C]//SOFSEM 2001:Theory and Practice of Informatics．2001:160-170
[54] Faber J,Meyer R．Model checking data-dependent real-timeproperties of the European Train Control System[C]∥Formal Methods in Computer Aided Design,FMCAD’06．2006:76-77
[55] Clarke E,Fehnker A,Han Z,et al．Abstraction and counterexample-guided refinement in model checking of hybrid systems[M]．Citeseer,2003:233-237
[56] Marrero W,Clarke E,Jha S．A model checker for authentication protocols[D]．Rutgers University,1997:188-196
[57] Basin D,Modersheim S,Vigano L．An on-the-fly model-checker for security protocol analysis[D]．Computer Security-ESORICS,2003:253-270
[58] Clarke E M,Emerson E A,Sistla A P．Automatic verification of finite-state concurrent systems using temporal logic[J]．ACM Transactions on Programming Languages and Systems,1986,8:244-263
[59] Vardi M Y,Wolper P A．An automata-theoretic approach to automatic program verification[C]∥Proceedings of the First Symposium on Logic in Computer Science．1986:322-331
[60] Bradfield L,Stirling C．Modal logics and mu-calculi:an introduction[M]．Handbook of Process Algebra,2001:293-330
[61] Emerson E A,Lei C L．Efficient model checking in fragments of the propositional mu-calculus[J]．1986:267-278
[62] Stirling C,Walker D．Local model checking in the modal mu-calculus[C]∥TAPSOFT''89．1989:369-383
[63] Emerson E A,Jutla C S,Sistla A P．On model checking for the -calculus and its fragments[J]．Theoretical Computer Science,2001,258(1/2):491-522
[64] Clarke E M,Emerson E A,Sifakis J．Model checking:algorithmic verification and debugging[J]．Communications of the ACM,2009,52(11):74-84
[65] McMillan K L．Symbolic model checking:an approach to thestate explosion problem[R]．Carnegie-Mellon University,Department of Computer Science,Report CMU-CS-92-131．1992
[66] Holzmann G J．The model checker SPIN[J]．IEEE Transactions on software engineering,1997,23(5):279-295
[67] Holzmann G J,Smith M H．Software model checking:Extracting verification models from source code[J]．Software Testing,Verification and Reliability,2001,11(2):65-79
[68] Godefroid P．VeriSoft:A tool for the automatic analysis of concurrent reactive software[C]∥Computer Aided Verification．1997:476-479
[69] Telelogic T A U．A SDL tools for real time systems develop-ment．http://www．telelogic．com
[70] Cleavel R,Parrow J,Steffen B．The concurrency workbench:A semantics based verification tool for the verification of concurrent systems[J]．ACM Trans．on Programming Languages and Systems,1993,5(1):36-72
[71] 傅海仑.定理机器证明思想的产生与发展[J].科技导报,2001:14-18
[72] 林作铨.一个模态非单调逻辑[J]．中国科学E辑,1996,6(3):276-288

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed