Construction Techniques of Anticipatory Monitors for Parameterized LTL
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

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

    This paper presents a method of constructing anticipatory monitors for PALTL (parameterized LTL (linear temporal logic)) based on automata theory. This paper on one hand investigates into the important concepts about the syntax, anticipatory semantics, valuation generation and binding of PALTL. It is assured that the binding and using are correct in syntax level. Then the concept of parameterized anticipatory monitor is presented consisting of the static part and the dynamic part. The static part is presented as parameterized Büchi automata, and the dynamic part is composed of the valuations of variables in the current state. While the system running, based on the static parameterized Büchi automata, the valuations of variables are dynamically generated and bound from the current state in an on-the-fly fashion, and the anticipatory monitor incrementally checks whether the current running system is satisfied with the given parameterized property. In this process, the parameterized monitor can precisely identify the minimal good/bad prefix of the monitored property.

    Reference
    Related
    Cited by
Get Citation

赵常智,董威,隋平,齐治昌.面向参数化LTL的预测监控器构造技术.软件学报,2010,21(2):318-333

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 15,2009
  • Revised:
  • Adopted:
  • Online:
  • 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