UPPAAL TIGA

UPPAAL TIGA is a software tool that is designed as an extension of UPPAAL [BDL04], and it stands out for its ability to implement the first efficient on-the-fly algorithm for solving games based on timed game automata concerning reachability and safety properties. Although it is acknowledged that timed games have been considered decidable, until now, there existed a lack of reliable on-the-fly algorithms for their analysis.

UPPAAL TIGA addresses this situation by providing the user with a friendly graphical interface with its corresponding server and a useful command line verifier. Furthermore, our proposed algorithm [CDFLL05] is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [LS98] for modeling and checking of finite-state systems that are linear in time. As an on-the-fly algorithm, it can terminate before the entire state-space is explored.

Additionally, the individual steps of the algorithm are efficiently carried out by the utilization of zones as the underlying data structure, which is essential to the success of the tool in carrying out its functions. UPPAAL TIGA includes a few optimization methods of the basic symbolic algorithm, as well as methods for obtaining time-optimal winnings strategies for reachability games.

In this release, there are two major bug fixes. These include correcting the answers and strategies provided for some cases involving delays and addressing an issue where the simulator lacked the ability to handle urgent and committed states properly.