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 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Forejt, Vojtěch; Kwiatkowska, Marta; Norman, Gethin; Trivedi, Ashutosh: Expected reachability-time games (2016)
  2. Drager, Klaus; Forejt, Vojtech; Kwiatkowska, Marta; Parker, David; Ujma, Mateusz: Permissive controller synthesis for probabilistic systems (2015)
  3. Waez, Md Tawhid Bin; Wąsowski, Andrzej; Dingel, Juergen; Rudie, Karen: A model for industrial real-time systems (2015)
  4. Bulychev, Peter; David, Alexandre; Larsen, Kim G.; Li, Guangyuan: Efficient controller synthesis for a fragment of $\mathrmMTL_0,\infty$ (2014)
  5. David, Alexandre; Fang, Huixing; Larsen, Kim Guldstrand; Zhang, Zhengkui: Verification and performance evaluation of timed game strategies (2014)
  6. Larsen, Kim G.; Legay, Axel; Traonouez, Louis-Marie; Wąsowski, Andrzej: Robust synthesis for real-time systems (2014)
  7. Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis: PRISM-games: a model checker for stochastic multi-player games (2013)
  8. Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico: CGMurphi: automatic synthesis of numerical controllers for nonlinear hybrid systems (2013)
  9. Jovanović, Aleksandra; Lime, Didier; Roux, Olivier H.: Synthesis of bounded integer parameters for parametric timed reachability games (2013)
  10. Legay, Axel; Traonouez, Louis-Marie: Pyecdar: towards open source implementation for timed systems (2013)
  11. Norman, Gethin; Parker, David; Sproston, Jeremy: Model checking for probabilistic timed automata (2013)
  12. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  13. Bertrand, Nathalie; Legay, Axel; Pinchinat, Sophie; Raclet, Jean-Baptiste: Modal event-clock specifications for timed component-based design (2012)
  14. 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)
  15. Finkbeiner, Bernd; Peter, Hans-Jörg: Template-based controller synthesis for timed systems (2012)
  16. Cheng, Chih-Hong; Rueß, Harald; Knoll, Alois; Buckl, Christian: Synthesis of fault-tolerant embedded systems using games: from theory to practice (2011)
  17. Bouyer, Patricia; Brenguier, Romain; Markey, Nicolas: Computing equilibria in two-player timed games via turn-based finite games (2010)
  18. Bouyer, Patricia; Brenguier, Romain; Markey, Nicolas: Nash equilibria for reachability objectives in multi-player timed games (2010)
  19. 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)
  20. Ehlers, Rüdiger; Mattmüller, Robert; Peter, Hans-Jörg: Combining symbolic representations for solving timed games (2010)

1 2 next