CÁC BÀI BÁO KHOA HỌC 17:32:09 Ngày 16/07/2019 GMT+7
Symbolic model checking of finite precision timed automata

This paper introduces the notion of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. To reduce the state space, FPTAs only record the integer values of clock variables together with the order of their most recent resets. We provide constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA, and then present an algorithm for reachability analysis. Finally, the paper reports some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure. © Springer-Verlag Berlin Heidelberg 2005.


 Yan R., Li G., Tang Z.
   716.pdf    Gửi cho bạn bè
  Từ khóa : Algorithms; Constraint theory; Data structures; Mathematical models; Time varying systems; Finite precision; Symbolic model checking; Symbolic states; Timed automata; Finite automata