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 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Bacci, Giovanni; Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim G.; Markey, Nicolas; Reynier, Pierre-Alain: Optimal and robust controller synthesis using energy timed automata with uncertainty (2021)
  2. Béchennec, Jean-Luc; Lime, Didier; Roux, Olivier H.: Logical time control of concurrent DES (2021)
  3. Chen, Mingshuai; Fränzle, Martin; Li, Yangjia; Mosaad, Peter N.; Zhan, Naijun: Indecision and delays are the parents of failure -- taming them algorithmically by synthesizing delay-resilient control (2021)
  4. van Putten, Berend Jan Christiaan; van der Sanden, Bram; Reniers, Michel; Voeten, Jeroen; Schiffelers, Ramon: Supervisor synthesis and throughput optimization of partially-controllable manufacturing systems (2021)
  5. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)
  6. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  7. Jovanović, Aleksandra; Lime, Didier; Roux, Olivier H.: A game approach to the parametric control of real-time systems (2019)
  8. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  9. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  10. Bouyer, Patricia; Markey, Nicolas; Perrin, Nicolas; Schlehuber-Caissier, Philipp: Timed-automata abstraction of switched dynamical systems using control invariants (2017)
  11. Waez, Md Tawhid Bin; Wąsowski, Andrzej; Dingel, Juergen; Rudie, Karen: Controller synthesis for dynamic hierarchical real-time plants using timed automata (2017)
  12. Bérard, Béatrice; Lafourcade, Pascal; Millet, Laure; Potop-Butucaru, Maria; Thierry-Mieg, Yann; Tixeuil, Sébastien: Formal verification of mobile robot protocols (2016)
  13. Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco: Dynamic controllability via timed game automata (2016)
  14. Forejt, Vojtěch; Kwiatkowska, Marta; Norman, Gethin; Trivedi, Ashutosh: Expected reachability-time games (2016)
  15. Jensen, Peter Gjøl; Larsen, Kim Guldstrand; Srba, Jiří: Real-time strategy synthesis for timed-arc Petri net games via discretization (2016)
  16. Dräger, Klaus; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Ujma, Mateusz: Permissive controller synthesis for probabilistic systems (2015)
  17. Larsen, Kim Guldstrand; Mikučionis, Marius; Taankvist, Jakob Haahr: Safe and optimal adaptive cruise control (2015)
  18. Waez, Md Tawhid Bin; Wąsowski, Andrzej; Dingel, Juergen; Rudie, Karen: A model for industrial real-time systems (2015)
  19. Bulychev, Peter; David, Alexandre; Larsen, Kim G.; Li, Guangyuan: Efficient controller synthesis for a fragment of (\mathrmMTL_0,\infty) (2014)
  20. David, Alexandre; Fang, Huixing; Larsen, Kim Guldstrand; Zhang, Zhengkui: Verification and performance evaluation of timed game strategies (2014)

1 2 3 next