Improving search order for reachability testing in timed automata

TL;DR

This paper introduces a ranking system and waiting strategy to improve the search order in reachability analysis of timed automata, leading to more efficient algorithms that outperform standard BFS in most benchmarks.

Contribution

It proposes a novel ranking and waiting approach to optimize search order in timed automata reachability analysis, enhancing efficiency over traditional methods.

Findings

Combined approach yields optimal search order on most benchmarks

Outperforms standard BFS in reachability analysis

Effective in preventing search inefficiencies

Abstract

Standard algorithms for reachability analysis of timed automata are sensitive to the order in which the transitions of the automata are taken. To tackle this problem, we propose a ranking system and a waiting strategy. This paper discusses the reason why the search order matters and shows how a ranking system and a waiting strategy can be integrated into the standard reachability algorithm to alleviate and prevent the problem respectively. Experiments show that the combination of the two approaches gives optimal search order on standard benchmarks except for one example. This suggests that it should be used instead of the standard BFS algorithm for reachability analysis of timed automata.