Model Checking for Event Graphs and Event Temporal Logic
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This paper proposes an event temporal logic (ETL) because there has been no suitable temporal logic that can directly describe the properties of event graph (EG) models. ETL takes events as its atomic propositions and has the abilities to describe the event canceling edge, the passing parameter values between events, time constraints and the priorities of coinstantaneous events, which can facilitate the description of properties for EGs. A model checking method for EG and ETL on the basis of theory of automata is also proposed in this paper to check whether properties hold for models, according to the accepted language is an empty set or not. The experimental results show ETL is powerful enough to describe EG models, and the model checking method for EG and ETL is effective.

    Reference
    Related
    Cited by
Get Citation

夏薇,姚益平,慕晓冬.面向事件图和事件时态逻辑的模型检验方法.软件学报,2013,24(3):421-432

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 23,2011
  • Revised:November 17,2011
  • Adopted:
  • Online: March 01,2013
  • Published:
You are the firstVisitors
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