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.
CITATION STYLE
Yan, R., Li, G., & Tang, Z. (2005). Symbolic model checking of finite precision timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3722 LNCS, pp. 272–287). https://doi.org/10.1007/11560647_18
Mendeley helps you to discover research relevant for your work.