微信服务号

微信订阅号

2025年5月1日 23:29 星期四
首页 > 过刊浏览>2017年第28卷第5期 >1070-1079. DOI:10.13328/j.cnki.jos.005208
PDF HTML阅读 XML下载 导出引用 引用提醒
正则模型类的时态可定义性
作者:
基金项目:

国家社会科学基金重大项目（14ZDB016）


Temporal Definability of Regular Model Classes
Author:
Fund Project:

Major Project of National Social Science Foundation of China (14ZDB016)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [17]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    正则模型是非正规模态逻辑的模型，通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算，可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭，并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力.

    Abstract:

    Regular models are models for non-normal modal logics. By defining some model operations, including disjoint union, C2t- bisimulation, generated submodel, and C2t-ultrafilter extension, this study proves that a class of regular models can be defined in the temporal language if and only if it is closed under disjoint unions, surjective C2t-bisimulations and C2t-ultrafilter extensions, while its complement is closed under ultrafilter extensions. This characterization theorem explains the expressive power of temporal language over regular models.

    参考文献
    [1] Pnueli A. The temporal logic of programs. In: Proc. of the Foundations of Computer Science. 1977. 46-57. [doi: 10.1109/SFCS.197 7.32]
    [2] Tang ZS, Zhao C. A temporal logic language oriented toward software engineering. Ruan Jian Xue Bao/Journal of Software, 1994, 5(12):1-16 (in Chinese with English abstract). http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19941201&flag=1
    [3] Duan ZH. Temporal Logic and Temporal Logic Programming. Science Press, 2005.
    [4] Burgess J. Basic Tense Logic. Handbook of Philosophical Logic. Vol.7, Springer Netherlands, 2002. [doi: 10.1007/978-94-017-046 2-5_1]
    [5] Lemmon EJ. Algebraic semantics for modal logics I. The Journal of Symbolic Logic, 1966,31(1):46-65. [doi: 10.2307/2270619]
    [6] Ma MH, Wang SX, Deng HW. Sequent calculus for minimal non-normal temporal logic. SCIENTIA SINICA Informationis, 2017,47(1):31-46 (in Chinese). [doi: 10.1360/N112015-00320]
    [7] Hodges W. A Shorter Model Theory. Cambridge University Press, 1997.
    [8] Nielsen M, Clausen C. Bisimulation for models in concurrency. In: Proc. of the Concurrency Theory. 1994. 385-400. [doi: 10.100 7/BFb0015021]
    [9] Benthem VJ. Modal correspondence theory [Ph.D. Thesis]. University of Amsterdam, 1976.
    [10] Perkov T. A generation of modal frame definability. In: Proc. of the ESSLLI 2012/2013. LNCS 8607. 2014. 142-153. [doi: 10.100 7/978-3-662-44116-9_10]
    [11] Kurtonina N, Rijke MD. Bisimulations for temporal logic. Journal of Logic, Language, and Information, 1997,6(4):403-425. [doi: 10. 1023/A:1008223921944]
    [12] Venama Y. Model definability, purely modal. In: JFAK. Essays Dedicated to Johan van Benthem on the Occasion of His 50th Birthday. Vossiuspers AUP, 1999. http://www.illc.uva.nl/j50/contribs/venema/index.html
    [13] Blackburn P, Rijke DM, Venema Y. Modal Logic. Cambridge University Press, 2011.
    [14] Bell JL, Slomson AB. Models and Ultraproducts. North-Holland Publishing Company, 1974.
    附中文参考文献:
    [2] 唐稚松,赵琛.一种面向软件工程的时序逻辑语言.软件学报,1994,5(12):1-16. http://www.jos.org.cn/ch/reader/view_abstract.aspx? file_no=19941201&flag=1
    [6] 马明辉,王善侠,邓辉文.极小非正规时序逻辑的矢列式演算系统.中国科学:信息科学,2017,47(1):31-46. [doi: 10.1360/N112015- 00320]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

王善侠,马明辉,陈武,邓辉文.正则模型类的时态可定义性.软件学报,2017,28(5):1070-1079

复制
分享
文章指标
  • 点击次数:3825
  • 下载次数: 5868
  • HTML阅读次数: 2856
  • 引用次数: 0
历史
  • 收稿日期:2016-06-30
  • 最后修改日期:2016-09-25
  • 在线发布日期: 2017-01-22
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19894625位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号