A promising approach to formal verification of real-time systems is to use timed automata to model systems, and then to check whether certain "unsafe" states are reachable. Although theoretically appealing, this approach has significant practical problems because it requires expensive computation of reachable states. Fortunately computing a superset of reachable states is sometimes much cheaper. Replacing the set of reachable states with its superset is a conservative approximation, in the sense that it can occasionally cause a correct system to be declared incorrect, but can never cause an incorrect system to be declared correct. We propose two algorithms for computing a superset of reachable states of a timed automaton. Both algorithms involve only manipulation of Boolean functions, which are used to represent both sets of discrete state components and timing information. The algorithms offer different trade-offs between accuracy of approximation and efficiency of computation. Initial experimental results show that they are competitive with the best published results, but that further improvements are necessary to scale up to realistic systems.
展开▼
