区间时序逻辑的模型检查

• Original Articles • Previous Articles Next Articles

Model checking interval temporal logic

ZHANG Hai-bin;DUAN Zhen-hua

(School of Computer Science and Technology, Xidian Univ., Xi’an 710071， China)

Received:2008-02-20 Revised:1900-01-01 Online:2009-04-20 Published:2009-05-23
Contact: ZHANG Hai-bin E-mail:hbzhang@mail.xidian.edu.cn

Abstract

Abstract: 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.

Key words: model checking, temporal logic, automata

CLC Number:

TP301

ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic
[J].J4, 2009, 36(2): 338-342.

[1]	SHEN Lixiang,MU Dejun,CAO Guo,XIE Guangqian,SHU Fangyong. Constructing formal verification models for hardware Trojans [J]. Journal of Xidian University, 2021, 48(3): 146-153.
[2]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[3]	DING Ming,ZHANG Shuling,ZHANG Chen,Zhang Jun. Method for the verification of safety requirements of avionics systems [J]. Journal of Xidian University, 2019, 46(3): 66-73.
[4]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	QIN Tao;CAI Li;YANG Xiaokuo. Reversible adder circuits with the quantum-dot cellular automata [J]. Journal of Xidian University, 2017, 44(2): 133-139.
[6]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[7]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[8]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[9]	YANG Yuanyuan;MA Wenping;LIU Weibo;YU You;GU Jian. Automatic detection of security protocols with XOR [J]. J4, 2012, 39(4): 120-125+183.
[10]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[11]	WANG Xiao-bing;DUAN Zhen-hua. Implementation of objected-oriented mechanism in framed temporal logic language MSVL [J]. J4, 2010, 37(3): 559-564+575.
[12]	JIN Jun;SHU Hong-ping. Secure multiple image watermarking based on cellular automata [J]. J4, 2010, 37(1): 174-180.
[13]	YANG Xiao-xiao;DUAN Zhen-hua. Verification of programs based on an axiom system for the MSVL language [J]. J4, 2010, 37(1): 96-101.
[14]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.
[15]	WANG Xiao-bing;DUAN Zhen-hua. Pointers in framing projection temporal logic programming languages [J]. J4, 2008, 35(6): 1069-1074.

Model checking interval temporal logic

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 0