UPPAAL TIGA 4.1.0-0.9
UPPAAL TIGA is an extension of UPPAAL [BDL04] and it implements the first efficient on-the-fly algorithm for solving games.
Though timed games for long have been known to be decidable there has until now been a lack of efficient and truly on-the-fly algorithms for their analysis.
UPPAAL TIGA provides a user-friendly graphical interface with its corresponding server, and a command line verifier.
The algorithm we propose [CDFLL05] is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [LS98] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space.
Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Our tool implements various optimizations of the basic symbolic algorithm, as well as methods for obtaining time-optimal winning strategies (for reachability games).
What's New in This Release:
· This version fixes two major bugs: Wrong answers (and strategies) were given for some cases involving delays, and the simulator didn't handle urgent and committed states properly.