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
关键词
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 条
  • [31] Symbolic Model Checking for Alternating Projection Temporal Logic
    Wang, Haiyang
    Duan, Zhenhua
    Tian, Cong
    COMBINATORIAL OPTIMIZATION AND APPLICATIONS, (COCOA 2015), 2015, 9486 : 481 - 495
  • [32] A Lazy Approach to Temporal Epistemic Logic Model Checking
    Cimatti, Alessandro
    Gario, Marco
    Tonetta, Stefano
    AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2016, : 1218 - 1226
  • [33] Model checking for event graphs and event temporal logic
    Xia, Wei
    Yao, Yi-Ping
    Mu, Xiao-Dong
    Ruan Jian Xue Bao/Journal of Software, 2013, 24 (03): : 421 - 432
  • [34] Model checking of pushdown systems for projection temporal logic
    Zhao, Liang
    Wang, Xiaobing
    Duan, Zhenhua
    THEORETICAL COMPUTER SCIENCE, 2019, 774 : 82 - 94
  • [35] Temporal Logic and Model Checking for Operator Precedence Languages
    Chiari, Michele
    Mandrioli, Dino
    Pradella, Matteo
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (277): : 161 - 175
  • [36] Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge
    Zhou, Conghua
    Sun, Bo
    Liu, Zhifeng
    ARTIFICIAL INTELLIGENCE AND COMPUTATIONAL INTELLIGENCE, PT I, 2010, 6319 : 209 - 221
  • [37] Model Checking Time Window Temporal Logic for Hyperproperties
    Bonnah, Ernest
    Luan Viet Nguyen
    Hoque, Khaza Anuarul
    2023 21ST ACM-IEEE INTERNATIONAL SYMPOSIUM ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN, MEMOCODE, 2023, : 100 - 110
  • [38] Abstract model checking and refinement of temporal logic in αSPIN
    Gallardo, MD
    Martínez, J
    Merino, P
    Pimentel, E
    THIRD INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2003, : 245 - 246
  • [39] Symbolic model checking for temporal-epistemic logic
    Lomuscio, Alessio
    Penczek, Wojciech
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012, 7360 LNCS : 172 - 195
  • [40] A Unified Model Checking Approach with Projection Temporal Logic
    Duan, Zhenhua
    Tian, Cong
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 5256 : 167 - 186