微信服务号

微信订阅号

2025-4-21- 19
Home > Archive>Volume 28, Issue 5, 2017 >1070-1079. DOI:10.13328/j.cnki.jos.005208
PDF HTML XML Export Cite reminder
Temporal Definability of Regular Model Classes
Author:
Affiliation:

Fund Project:

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

  • Article
    • | |
  • Metrics
    • |
  • Reference [17]
    • |
  • Related [20]
    • | | |
  • Comments
    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.

    Reference
    [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]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:3818
  • PDF: 5850
  • HTML: 2832
  • Cited by: 0
History
  • Received:June 30,2016
  • Revised:September 25,2016
  • Online: January 22,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2036745Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063