%0 Conference Proceedings
%T Difference Bound Constraint Abstraction for Timed Automata Reachability Checking
%+ Institute of Software Chinese Academy of Sciences [Beijing]
%+ University of Chinese Academy of Sciences [Beijing] (UCAS)
%A Wang, Weifeng
%A Jiao, Li
%Z Part 3: Real Time Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 146-160
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_10
%K Model Check
%K Negative Cycle
%K Reachability Problem
%K Time Automaton
%K Predicate Abstraction
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We consider the reachability problem for timed automata. One of the most well-known solutions for this problem is the zone-based search method. Max bound abstraction and LU-bound abstraction on zones have been proposed to reduce the state space for zone based search. These abstractions use bounds collected from the timed automata structure to compute an abstract state space. In this paper we propose a difference bound constraint abstraction for zones. In this abstraction, sets of difference bound constraints collected from the symbolic run are used to compute the abstract states. Based on this new abstraction scheme, we propose an algorithm for the reachability checking of timed automata. Experiment results are reported on several timed automata benchmarks.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767323/document
%2 https://inria.hal.science/hal-01767323/file/978-3-319-19195-9_10_Chapter.pdf
%L hal-01767323
%U https://inria.hal.science/hal-01767323
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039