Figure 1: Uppaal TIGA on screen.
UPPAAL TIGA (Fig. 1) is an extension of
and it implements the first efficient on-the-fly algorithm for
solving games based on timed game automata with respect to
reachability and safety properties. 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.
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).
- [BDL04] Gerd Behrmann, Alexandre David, and Kim G. Larsen. A Tutorial on UPPAAL. LNCS 3185. Springer-Verlag 2004, pp 200-236.
- [CDFLL05] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient On-the-fly Algorithms for the Analysis of Timed Games. LNCS 3653. Springer-Verlag 2005, pp 66-80.
- [LS98] Xinxin Liu and Scott A. Smolka. Simple Linear-Time Algorithm for Minimal Fixed Points. LNCS 1443. Springer-Verlag 1998, pp 53-66.
Latest NewsVersion 0.16 is released.
18 Feb 2011
This version is a maintenance release fixing bug 502 and a crash when exceptions were thrown in the liveness checker of UPPAAL.Version 0.15 for Mac released.
21 Oct 2010
The Mac version of TIGA is now available, courtesy of Didier Lime.Version 0.15 released.
14 Oct 2010
Version 0.15 is released today. This version improves the simulator. Occurences of states "getting out of the strategy" are rarer now. However, verification will take longer when asking for strategies.Timed interface pre-release v1.
13 Jan 2010
A special version implementing timed interfaces is released today. This version introduces a new checker that treats timed game automata as timed I/O automata and opens the way to incremental design and compositional reasoning.Version 0.14 released.
6 Nov 2009
Version 0.14 is released today. This version improves the simulator: stop-watches are better treated and the Gantt chart respects urgent/committed states.Version 0.13 released.
11 Sep 2009
Version 0.13 is released today. This version fixes issues with the simulator and fixes bugs in the verifier. Fixes of the development versions 4.1.1 and 4.1.2 haved been ported. The simulator includes a new experimental Gantt chart. The examples in the demo directory have been fixed. This version supports simulation check of timed game automata.