Model checking interval temporal logic

被引：0
|
作者：
Zhang, Hai-Bin [1 ]
Duan, Zhen-Hua [1 ]
机构：
[1] School of Computer Science and Technology, Xidian Univ., Xi'an 710071, China
来源：
Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University | 2009年 / 36卷 / 02期
关键词：
Automata - Interval temporal logic - Model checking problem - Set of rules;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
To check whether a system represented by a labelled finite state automaton meets a property described by an interval temporal logic formula, a set of rules are defined. Using such rules, a chop-automaton which accepts all intervals satisfying this interval temporal logic formula can be constructed. In addition, a rule for translating a chop-automaton to a labelled finite state automaton is also defined. Thus, the model checking problem for the interval temporal logic can be solved by testing language inclusion between two labelled finite state automata.
引用
收藏
页码：338 / 342
相关论文
共 50 条
  • [41] Temporal Logic Model Checking via Probe Machine
    Zhu, Weijun
    Li, En
    Yang, Xiaoyu
    PROCEEDINGS OF 2020 IEEE 4TH INFORMATION TECHNOLOGY, NETWORKING, ELECTRONIC AND AUTOMATION CONTROL CONFERENCE (ITNEC 2020), 2020, : 623 - 626
  • [42] Temporal logic query checking: A tool for model exploration
    Gurfinkel, A
    Chechik, M
    Devereux, B
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (10) : 898 - 914
  • [43] HyLTL : a temporal logic for model checking hybrid systems
    Bresolin, Davide
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (124): : 73 - 84
  • [44] Model Checking Parallel Interval Logic on Parallel Run Structures
    Cao, Zining
    2012 THIRD INTERNATIONAL CONFERENCE ON THEORETICAL AND MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE (ICTMF 2012), 2013, 38 : 390 - 394
  • [45] On-the-fly model checking from interval logic specifications
    Hornos, MJ
    Capel, MI
    ACM SIGPLAN NOTICES, 2002, 37 (12) : 108 - 119
  • [46] Temporal logic query checking
    Bruns, G
    Godefroid, P
    16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, : 409 - 417
  • [47] Model Checking Temporal Logic Formulas Using Sticker Automata
    Zhu, Weijun
    Feng, Changwei
    Wu, Huanmei
    BIOMED RESEARCH INTERNATIONAL, 2017, 2017
  • [48] From bounded to unbounded model checking for temporal epistemic logic
    Kacprzak, M
    Lomuscio, A
    Penczek, W
    FUNDAMENTA INFORMATICAE, 2004, 63 (2-3) : 221 - 240
  • [49] Improving symbolic model checking by rewriting temporal logic formulae
    Déharbe, D
    Moreira, AM
    Ringeissen, C
    REWRITING TECHNIQUES AND APPLICATIONS, 2002, 2378 : 207 - 221
  • [50] Model checking open systems with alternating projection temporal logic
    Tian, Cong
    Duan, Zhenhua
    THEORETICAL COMPUTER SCIENCE, 2019, 774 : 65 - 81
12345