UPPAAL TIGA

UPPAAL TIGA (Fig. 1) is an extension of UPPAAL [BDL04] 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).


References in zbMATH (referenced in 45 articles )

Showing results 21 to 40 of 45.
Sorted by year (citations)
  1. Larsen, Kim G.; Legay, Axel; Traonouez, Louis-Marie; Wąsowski, Andrzej: Robust synthesis for real-time systems (2014)
  2. Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis: PRISM-games: a model checker for stochastic multi-player games (2013)
  3. Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico: CGMurphi: automatic synthesis of numerical controllers for nonlinear hybrid systems (2013)
  4. Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Model-based verification, optimization, synthesis and performance evaluation of real-time systems (2013)
  5. Jovanović, Aleksandra; Lime, Didier; Roux, Olivier H.: Synthesis of bounded integer parameters for parametric timed reachability games (2013)
  6. Legay, Axel; Traonouez, Louis-Marie: \textscPyecdar: towards open source implementation for timed systems (2013) ioport
  7. Norman, Gethin; Parker, David; Sproston, Jeremy: Model checking for probabilistic timed automata (2013)
  8. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  9. Bertrand, Nathalie; Legay, Axel; Pinchinat, Sophie; Raclet, Jean-Baptiste: Modal event-clock specifications for timed component-based design (2012)
  10. Bourke, Timothy; David, Alexandre; Larsen, Kim G.; Legay, Axel; Lime, Didier; Nyman, Ulrik; Wąsowski, Andrzej: New results on timed specifications (2012)
  11. Bulychev, Peter; Cassez, Franck; David, Alexandre; Larsen, Kim Guldstrand; Raskin, Jean-François; Reynier, Pierre-Alain: Controllers with minimal observation power (application to timed systems) (2012)
  12. Finkbeiner, Bernd; Peter, Hans-Jörg: Template-based controller synthesis for timed systems (2012)
  13. Cheng, Chih-Hong; Rueß, Harald; Knoll, Alois; Buckl, Christian: Synthesis of fault-tolerant embedded systems using games: from theory to practice (2011)
  14. Bouyer, Patricia; Brenguier, Romain; Markey, Nicolas: Nash equilibria for reachability objectives in multi-player timed games (2010)
  15. Bouyer, Patricia; Brenguier, Romain; Markey, Nicolas: Computing equilibria in two-player timed games via turn-based finite games (2010)
  16. David, Alexandre; Larsen, Kim G.; Legay, Axel; Nyman, Ulrik; Wasowski, Andrzej: Timed I/O automata: a complete specification theory for real-time systems (2010)
  17. David, Alexandre; Larsen, Kim G.; Legay, Axel; Nyman, Ulrik; Wąsowski, Andrzej: Methodologies for specification of real-time systems using timed I/O automata (2010)
  18. Ehlers, Rüdiger; Mattmüller, Robert; Peter, Hans-Jörg: Combining symbolic representations for solving timed games (2010)
  19. Fahrenberg, Uli; Larsen, Kim G.; Thrane, Claus R.: Verification, performance analysis and controller synthesis for real-time systems (2010)
  20. Bouyer, Patricia; Duflot, Marie; Markey, Nicolas; Renault, Gabriel: Measuring permissivity in finite games (2009)