UPPAAL TIGA expands upon UPPAAL [BDL04], offering an efficient on-the-fly game-solving algorithm.
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.
Version 4.1.0-0.9: N/A