Reachability Checking of Finite Precision Timed Automata
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

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

    To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.

    Reference
    Related
    Cited by
Get Citation

晏荣杰,李广元,徐雨波,刘春明,唐稚松.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 28,2004
  • Revised:July 11,2005
  • 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