The following information was submitted:
Transactions: WSEAS TRANSACTIONS ON COMPUTERS
Transactions ID Number: 53-418
Full Name: Conghua Zhou
Position: Associate Professor
Age: ON
Sex: Male
Address: School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang, Jiangsu Province 212013, PR.China
Country: CHINA
Tel:
Tel prefix:
Fax:
E-mail address: chzhou@ujs.edu.cn
Other E-mails: zchwyl2003@163.com
Title of the Paper: three-valued abstraction in model checking real-time temporal logic of knowledge
Authors as they appear in the Paper: Conghua Zhou, Bo Sun
Email addresses of all the authors:
Number of paper pages: 20
Abstract: Model checking in real-time temporal logic of knowledge TACTLK confronts the same challenge as in traditional model checking, that is the state space explosion problem. Abstraction is one of the most effective methods to alleviate the state space explosion problem, under the traditional framework of two-valued abstraction, the abstract model obtained using abstraction techniques is only the upper approximation of the original model. In this paper, we introduce three-valued abstraction into model checking real-time temporal logic of knowledge , define the abstract model of a real time interpreted system and present the three-valued semantics of TACTLK on the abstract model. We prove that the abstract model obtained using the abstraction techniques is not only the upper approximation of the original model but also its lower approximation. Finally, the variants of the standard railroad crossing system and the active structure control system are adopted to illustrate !
the effectiveness of our abstraction techniques.
Keywords: Model checking, Real-time temporal logic of knowledge, TACTLK, State space explosion, Three-valued abstraction
EXTENSION of the file: .pdf
Special (Invited) Session:
Organizer of the Session:
How Did you learn about congress:
IP ADDRESS: 221.6.159.251
