studied before, e.g. [S9]. The question addressed in this chapter was on practical aspects: how can we handle robustness efficiently, and how do specialized algorithms improve over a treatment of robustness by modeling?

The robustness verification problems are not relevant for all verification tasks. In fact, models of systems under study are often abstracted significantly for model checking to scale, and detailed considerations about small clock imprecisions are not always relevant in such abstract models. Moreover, many case studies considered in the literature could actually use a discrete notion of time, conveniently and succinctly modeled by timed automata, so robustness, as we consider here, is not appropriate to consider. Yet, some distributed systems are indeed sensitive to small variations in the activation periods; e.g. an industrial case study is presented in [AFMS19] where timed automata techniques were used to deal with these real-time constraints. We believe that the robustness problems we solve here can further be relevant for analyzing a detailed low-level model of modest size, say, an infrared controller as studied in [BS13]. Analyzing a model with real-time constraints derived from the specification sheet of such a device might be sufficiently low-level so that the robustness questions make sense. By identifying such applications, one might find new uses for formal methods to solve non-trivial problems.

The application of formal methods to probabilistic systems have targeted rich sets of properties to be handled when synthesizing schedulers, and by the way uncertainties, modeled both with probabilities and nondeterminism are handled are taken into account. In fact, we believe that the contributions of the formal methods community is meaningful, and complementary to those from the discrete mathematics, planning, and reinforcement learning communities in the extent to which these help one 1) to work with schedulers with large memory requirements, both in theory and in practice; 2) to mix temporal logic properties with various quantitative objectives, either their expectations or their probabilities of satisfaction; 3) to handle nondeterministic uncertainties when analyzing systems, where the goal is not to optimize the average performance of a scheduler but to ensure that all schedulers have guaranteed average behaviors.

These results have the advantage of providing finer guarantees in the synthesized controllers. In fact, a single objective function to optimize is often insufficient to express complex requirements one might ask for the controller. One often needs to add temporal constraints with worst-case or average-case guarantees, and have finer control on the probability distribution of the objective values. Optimizing just the expectation might be insufficient; one might want to optimize the variance as well, have constraints on percentiles, and impose worst-case guarantees either on performance or on temporal properties that must be respected at all times. As for model checking, in practice, controller synthesis is difficult to apply in one-shot because the first objectives that are written might not capture the intent of the designer. Having a rich set of objectives and conditions helps the designer to refine the objectives so as to apply controller synthesis in real applications.

The study of multiple-environment MDPs participate in the effort of solving synthesis problems under nondeterministic uncertainties of the model. One could pursue this approach to target the analysis of systems with a clear separation of both types of uncertainties, and a mix of worst-case and probabilistic guarantees. A line of work [BFRR17], [S10] consists in giving such mix guarantees on quantitative objectives, that is, ensuring some performance guarantee in the worst-case, and other guarantees in average.

Another important direction is the development of data structures and solvers for handling such uncertainties, but also developing algorithms to work efficiently with schedulers with large memory requirements and various quantitative objectives. In many theoretical works, including some of ours, quantitative objectives such as total payoff are handled by encoding integer quantities in the state
space. Although such an approach might help achieve optimal worst-case complexity, this is not
satisfactory in practice. Efforts are being made to classify the complexity of schedulers depending on
the type and quantity of memory requirements [MM21]; these might lead to finer algorithms perhaps
representing these quantities symbolically, and focusing the state space search on the control part of
the model. In short, in the same way finite-state model checking has seen over the years several data
structures and algorithms to handle larger and larger state spaces, perhaps an important objective
for the community is the development of robust and efficient data structures and algorithms for
quantitative verification over probabilistic systems that can handle various quantitative objectives
and large schedulers, in order to be able to routinely apply this rich theory to real-world applications.
References to Author's Publications

[S1] Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, and Ocan Sankur. Stochastic shortest paths and weight-bounded properties in markov decision processes. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 86–94, New York, NY, USA, 2018. ACM.

[S2] Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur. Admissiblity in con-current games. In *44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland*, pages 123:1–123:14, 2017.

[S3] Nicolas Basset, Jean-François Raskin, and Ocan Sankur. Admissible strategies in timed games. In Luca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, editors, *Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday*, pages 403–425, Cham, 2017. Springer International Publishing.

[S4] Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Dynamic network congestion games. In *40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)*, Goa, India, December 2020.

[S5] Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Semilinear representations for series-parallel atomic congestion games. In Anuj Dawar and Venkatesan Guruswami, editors, *Proceedings of the 42nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'22)*, volume 250 of *Leibniz International Proceedings in Informatics*. Leibniz-Zentrum für Informatik, December 2022.

[S6] Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized Safety Verification of Round-Based Shared-Memory Systems. In Mikołaj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, *49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)*, volume 229 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 113:1–113:20, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[S7] Patricia Bouyer, Paul Gastin, Frédéric Herbreteau, Ocan Sankur, and B. Srivathsan. Zone-based verification of timed automata: Extrapolations, simulations and what next? In Sergiy Bogomolov and David Parker, editors, *Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings*, volume 13465 of *Lecture Notes in Computer Science*, pages 16–42. Springer, 2022.
[S8] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust model-checking of timed automata via pumping in channel machines. In Uli Fahrenberg and Stavros Tripakis, editors, *Proceedings of the 9th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'11)*, volume 6919 of *Lecture Notes in Computer Science*, pages 97–112, Aalborg, Denmark, September 2011. Springer.

[S9] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robustness in timed automata. In Parosh Aziz Abdulla and Igor Potapov, editors, *Proceedings of the 7th Workshop on Reachability Problems in Computational Models (RP'13)*, volume 8169 of *Lecture Notes in Computer Science*, pages 1–18, Uppsala, Sweden, September 2013. Springer.

[S10] Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games for reactive synthesis. In Adrian-Horia Dediu, Jan Janoušek, Carlos Martín-Vide, and Bianca Truthe, editors, *Language and Automata Theory and Applications: 10th International Conference (LATA 2016)*, Prague, Czech Republic, March 14-18, 2016, volume 9618 of *Lecture Notes in Computer Science*, pages 3–23, Cham, 2016. Springer International Publishing.

[S11] Romain Brenguier, Stefan Göller, and Ocan Sankur. A comparison of succinctly represented finite-state systems. In Maciej Koutny and Irek Ulidowski, editors, *Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12)*, volume 7454 of *Lecture Notes in Computer Science*, pages 147–161, Newcastle, UK, September 2012. Springer.

[S12] Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In Roland Meyer and Uwe Nestmann, editors, *28th International Conference on Concurrency Theory (CONCUR 2017)*, volume 85 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 2:1–2:23, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[S13] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Ocan Sankur. Abssynthe: abstract synthesis from succinct safety specifications. In Krishnendu Chatterjee, Rüdiger Ehlers, and Susmit Jha, editors, *Proceedings 3rd Workshop on Synthesis (SYNT'14)*, volume 157 of *Electronic Proceedings in Theoretical Computer Science*, pages 100–116. Open Publishing Association, 2014.

[S14] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Ocan Sankur. Admissibility in quantitative graph games. In *36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science*, Chennai, India, December 2016.

[S15] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Ocan Sankur. Compositional algorithms for succinct safety games. In Pavol Černý, Viktor Kuncak, and Madhusudan Parthasarathy, editors, *Proceedings Fourth Workshop on Synthesis (SYNT'15), San Francisco, CA, USA, 18th July 2015*, volume 202 of *Electronic Proceedings in Theoretical Computer Science*, pages 98–111. Open Publishing Association, 2016.

[S16] Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. *Acta Informatica*, 54(1):41–83, 2017.
[S17] Isseïnie Calviac, Ocan Sankur, and François Schwarzentruber. Improved complexity results and an efficient solution for connected multi-agent path finding. In *22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS'23)*, May 2023. To appear.

[S18] Tristan Charrier, Arthur Queffelec, Ocan Sankur, and François Schwarzentruber. Complexity of planning for connected agents. *Auton. Agents Multi Agent Syst.*, 34(2):44, 2020.

[S19] Tristan Charrier, Arthur Queffelec, Ocan Sankur, and François Schwarzentruber. Reachability and coverage planning for connected agents. In *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019*, pages 144-150, 2019.

[S20] Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The first reactive synthesis competition (syntcomp 2014). *International Journal on Software Tools for Technology Transfer*, pages 1-24, 2016.

[S21] Thierry Jéron, Nicolas Markey, David Mentré, Reiya Noguchi, and Ocan Sankur. Incremental methods for checking real-time consistency. In *18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020.*, 2020.

[S22] Reiya Noguchi, Ocan Sankur, Thierry Jéron, Nicolas Markey, and David Mentré. Repairing real-time requirements. In Ahmed Bouajjani, Lukáš Holík, and Zhilin Wu, editors, *Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis (ATVA'22)*, Lecture Notes in Computer Science. Springer-Verlag, October 2022. To appear.

[S23] Youssouf Oualhadj, Pierre-Alain Reynier, and Ocan Sankur. Probabilistic robust timed games. In Paolo Baldan and Daniele Gorla, editors, *Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14)*, volume 8704 of *Lecture Notes in Computer Science*, pages 203-217. Springer, 2014.

[S24] Jakob Piribauer, Ocan Sankur, and Christel Baier. The Variance-Penalized Stochastic Shortest Path Problem. In Mikołaj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, *49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)*, volume 229 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 129:1-129:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[S25] Arthur Queffelec, Ocan Sankur, and François Schwarzentruber. Planning for Connected Agents in a Partially Known Environment. In *AI 2021 - 34th Canadian Conference on Artificial Intelligence*, pages 1-23, Vancouver / Virtual, Canada, May 2021.

[S26] Jean-François Raskin and Ocan Sankur. Multiple-Environment Markov Decision Processes. In Venkatesh Raman and S. P. Suresh, editors, *34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)*, volume 29 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 531-543. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2014.

[S27] Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction refinement algorithms for timed automata. In Isil Dillig and Serdar Tasiran, editors, *Computer Aided Verification (CAV'19)*, pages 22-40, Cham, 2019. Springer International Publishing.
[S28] Ocan Sankur. Symbolic quantitative robustness analysis of timed automata. In Christel Baier and Cesare Tinelli, editors, *Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15)*, volume 9035 of *Lecture Notes in Computer Science*, pages 484–498. Springer Berlin Heidelberg, 2015.

[S29] Ocan Sankur. Timed Automata Verification and Synthesis via Finite Automata Learning. In *TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*, Paris, France, April 2023.

[S30] Ocan Sankur, Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust controller synthesis in timed automata. In Pedro R. D'Argenio and Hernán Melgratti, editors, *Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13)*, volume 8052 of *Lecture Notes in Computer Science*, pages 546–560, Buenos Aires, Argentina, August 2013. Springer.

[S31] Ocan Sankur and Jean-Pierre Talpin. An abstraction technique for parameterized model checking of leader election protocols: Application to FTSP. In *Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I*, pages 23–40, 2017.

[S32] Bastien Thomas and Ocan Sankur. PyLTA: A Verification Tool for Parameterized Distributed Algorithms. In *TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*, Paris, France, April 2023.
Bibliography

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126(2):183-235, 1994.

[ADBA21] Mohamadreza Ahmadi, Anushri Dixit, Joel W Burdick, and Aaron D Ames. Risk-averse stochastic shortest path planning. arXiv:2103.14727, 2021.

[AFMS19] Étienne André, Laurent Fribourg, Jean-Marc Mota, and Romain Soulat. Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In Constantin Enea and Ruzica Piskac, editors, *VMCAI*, Lecture Notes in Computer Science, pages 409-424. Springer, 2019.

[AMP95] Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic controller synthesis for discrete and timed systems. In *Hybrid Systems II*, volume 999 of LNCS, pages 1-20. Springer, 1995.

[Ang87] Dana Angluin. Learning regular sets from queries and counterexamples. *Information and Computation*, 75(2):87-106, 1987.

[Arr70] Kenneth J. Arrow. *Essays in the Theory of Risk-Bearing*. Amsterdam, North-Holland Pub. Co., 1970.

[AT05] Karine Altisen and Stavros Tripakis. Implementation of timed automata: An issue of semantics or modeling? In Paul Pettersson and Wang Yi, editors, *Proceedings of the 3rd International Conferences on Formal Modelling and Analysis of Timed Systems, (FORMATS'05)*, volume 3829 of *Lecture Notes in Computer Science*, pages 273-288. Springer, 2005.

[BA11] Nicolas Basset and Eugene Asarin. Thin and thick timed regular languages. In Uli Fahrenberg and Stavros Tripakis, editors, *Formal Modeling and Analysis of Timed Systems*, volume 6919 of *Lecture Notes in Computer Science*, pages 113-128. Springer, 2011.

[BBC+14] Tomáš Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. Markov decision processes with multiple long-run average objectives. *Logical Methods in Computer Science*, 10(13):1-29, 2014.

[BBE+10] Tomás Brázdil, Václav Brozek, Kousha Etessami, Antonín Kucera, and Dominik Wojtczak. One-counter Markov decision processes. In *Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)*, pages 863-874. SIAM, 2010.
[BBLP06] Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, and Radek Pelánek. Lower and upper bounds in zone-based abstractions of timed automata. *International Journal on Software Tools for Technology Transfer*, 8(3):204–215, June 2006.

[BCD+07a] Gerd Behrmann, Agnes Cougnard, Alexandre David, Emmanuel Fleury, Kim G Larsen, and Didier Lime. Uppaal-tiga: Time for playing games! In *International Conference on Computer Aided Verification*, pages 121–125. Springer, 2007.

[BCD+07b] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. UPPAAL-Tiga: Time for playing games! In *Proc. 19th International Conference on Computer Aided Verification (CAV'07)*, volume 4590 of *Lecture Notes in Computer Science*, pages 121–125. Springer, 2007.

[BCF+13] Tomás Brázdil, Taolue Chen, Vojtech Forejt, Petr Novotný, and Aistis Simaitis. Solvency Markov decision processes with interest. In *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India*, pages 487–499, 2013.

[BCFK17] Tomáš Brázdil, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. Trading performance for stability in Markov decision processes. *Journal of Computer and System Sciences*, 84:144–170, 2017.

[BCP+01] V. Bertin, E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venier, D. Weil, and S. Yovine. Taxys=esterel+kronos. a tool for verifying real-time properties of embedded systems. In *Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228)*, volume 3, pages 2875–2880 vol.3, 2001.

[BDD+14] Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, and Sascha Klüppelholz. Energy-utility quantiles. In *Proc. of the 6th NASA Formal Methods Symposium (NFM)*, volume 8430 of *Lecture Notes in Computer Science*, pages 285–299. Springer, 2014.

[BDL+06a] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Håkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. Uppaal 4.0. 2006.

[BDL+06b] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Håkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In *Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA*, pages 125–126, 2006.

[BFRR14] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Ernst W. Mayr and Natacha Portier, editors, *31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, March 5-8, 2014, Lyon, France*, volume 25 of *LIPIcs*, pages 199–213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.

[BFRR17] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. *Information and Computation*, 254:259–295, 2017.
[BK08] Christel Baier and Joost-Pieter Katoen. *Principles of model checking*. MIT Press, 2008.

[BKKW17] Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Maximizing the conditional expected reward for reaching the goal. In Axel Legay and Tiziana Margaria, editors, *23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)*, volume 10206 of *Lecture Notes in Computer Science*, pages 269–285. Springer, 2017.

[BKN16] Tomás Brázdil, Antonín Kucera, and Petr Novotný. Optimizing the expected mean payoff in energy Markov decision processes. In *14th International Symposium on Automated Technology for Verification and Analysis (ATVA)*, volume 9938 of *Lecture Notes in Computer Science*, pages 32–49, 2016.

[BLN03] Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A tool for BDD-based verification of real-time systems. In *Proc. 15th International Conference on Computer Aided Verification (CAV'03)*, volume 2725 of *Lecture Notes in Computer Science*, pages 122–125. Springer, 2003.

[BLR11] Thomas Ball, Vladimir Levin, and Sriram K Rajamani. A decade of software model checking with slam. *Communications of the ACM*, 54(7):68–76, 2011.

[BM83] Bernard Berthomieu and Miguel Menasche. An enumerative approach for analyzing time Petri nets. In R. E. A. Mason, editor, *Information Processing 83 – Proceedings of the 9th IFIP World Computer Congress (WCC'83)*, pages 41–46. North-Holland/IFIP, September 1983.

[BMR06] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust model-checking of linear-time properties in timed automata. In José R. Correa, Alejandro Hevia, and Marcos Kiwi, editors, *Proceedings of the 7th Latin American Symposium on Theoretical Informatics (LATIN'06)*, volume 3887 of *Lecture Notes in Computer Science*, pages 238–249. Springer, 2006.

[BMR08] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust analysis of timed automata via channel machines. In Roberto Amadio, editor, *Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS'08)*, volume 4962 of *Lecture Notes in Computer Science*, pages 157–171. Springer, 2008.

[BS13] Timothy Bourke and Arcot Sowmya. Analyzing an embedded sensor with timed automata in Uppaal. *ACM Transactions on Embedded Computing Systems*, 13(3):Article 44, December 2013.

[BT91] Dimitri P. Bertsekas and John N. Tsitsiklis. An analysis of stochastic shortest path problems. *Mathematics of Operations Research*, 16(3):580–595, 1991.

[BY03] Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In *Advanced Course on Petri Nets*, pages 87–124. Springer, 2003.

[BY04] Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, *Lectures on Concurrency*
and Petri Nets, volume 2098 of Lecture Notes in Computer Science, pages 87–124. Springer-Verlag, 2004.

[CC77] Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238–252, 1977.

[CCK+20] Krishnendu Chatterjee, Martin Chmelík, Deep Karkhanis, Petr Novotný, and Amélie Royer. Multiple-environment markov decision processes: Efficient analysis and applications. Proceedings of the International Conference on Automated Planning and Scheduling, 30(1):48–56, Jun. 2020.

[CCT13] Krishnendu Chatterjee, Martin Chmelík, and Mathieu Tracol. What is decidable about partially observable markov decision processes with omega-regular objectives. In CSL, volume 23 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[CD11] Krishnendu Chatterjee and Laurent Doyen. Energy and mean-payoff parity Markov decision processes. In Proc. of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 6907 of Lecture Notes in Computer Science, pages 206–218. Springer, 2011.

[CDF+05a] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Lmei Didier. Efficient on-the-fly algorithms for the analysis of timed games. In CONCUR 2005, pages 66–80, London, UK, 2005. Springer-Verlag.

[CDF+05b] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 66–80. Springer, 2005.

[CES09] Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: Algorithmic verification and debugging. Commun. ACM, 52(11):74–84, nov 2009.

[CGJ+00] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In International Conference on Computer Aided Verification, pages 154–169. Springer, 2000.

[CGJ+03] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 50(5):752–794, 2003.

[CGM+19] Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta. Extending nuxmv with timed transition systems and timed temporal properties. In International Conference on Computer Aided Verification, pages 376–386. Springer, 2019.

[CGMT14] Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. IC3 modulo theories via implicit predicate abstraction. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of Lecture Notes in Computer Science, pages 46–61, 2014.
[CH09] Krishnendu Chatterjee and Thomas A. Henzinger. Probabilistic systems with limsup and liminf objectives. In Margaret Archibald, Vasco Brattka, Valentin Goranko, and Benedikt Löwe, editors, *Infinity in Logic and Computation*, volume 5489 of *Lecture Notes in Computer Science*, pages 32–45. Springer Berlin Heidelberg, 2009.

[CHK13] Taolue Chen, Tingting Han, and Marta Z. Kwiatkowska. On the complexity of model checking interval-valued discrete time markov chains. *Inf. Process. Lett.*, 113(7):210–216, 2013.

[CHP11] Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Timed parity games: Complexity and robustness. *Logical Methods in Computer Science*, 7(4), 2011.

[CHR02] Franck Cassez, Thomas A. Henzinger, and Jean-François Raskin. A comparison of control problems for timed and hybrid systems. In Claire Tomlin and Mark R. Greenstreet, editors, *Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control (HSCC'02)*, volume 2289 of *Lecture Notes in Computer Science*, pages 134–148. Springer, 2002.

[CHV+18] Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem, et al. *Handbook of model checking*, volume 10. Springer, 2018.

[CMH06] Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger. Markov decision processes with multiple objectives. In Bruno Durand and Wolfgang Thomas, editors, *STACS 2006*, volume 3884 of *Lecture Notes in Computer Science*, pages 325–336. Springer Berlin Heidelberg, 2006.

[Col97] EJ Collins. Finite-horizon variance penalised Markov decision processes. *Operations-Research-Spektrum*, 19(1):35–39, 1997.

[dA97] Luca de Alfaro. *Formal Verification of Probabilistic Systems*. PhD thesis, Stanford University, Department of Computer Science, 1997.

[dA99] Luca de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In *10th International Conference on Concurrency Theory (CONCUR)*, volume 1664 of *Lecture Notes in Computer Science*, pages 66–81, 1999.

[DDD+12] Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. *Science of Computer Programming*, 77(10):1122–1150, 2012.

[DDMR08] Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robust safety of timed automata. *Formal Methods in System Design*, 33(1-3):45–84, 2008.

[DDR05] Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP semantics: From timed models to timed implementations. *Formal Aspects of Computing*, 17(3):319–341, 2005.

[DGDF07] Carole Delporte-Gallet, Stéphane Devismes, and Hugues Fauconnier. Robust stabilizing leader election. In Toshimitsu Masuzawa and Sébastien Tixeuil, editors, *Stabilization, Safety, and Security of Distributed Systems*, pages 219–233, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.
[Die06] Henning Dierks. *Time, abstraction and heuristics - automatic verification and planning of timed systems using abstraction and heuristics*, volume 01-06 of *Berichte aus dem Department für Informatik / Universität Oldenburg / Fachbereich Informatik*. 2006.

[DK06] Conrado Daws and Piotr Kordy. Symbolic robustness analysis of timed automata. In *Eugene Asarin and Patricia Bouyer, editors, Proceedings of the 4th International Conferences on Formal Modelling and Analysis of Timed Systems, (FORMATS'06)*, volume 4202 of *Lecture Notes in Computer Science*, pages 143–155. Springer, September 2006.

[DKL07] Henning Dierks, Sebastian Kupferschmid, and Kim G Larsen. Automatic abstraction refinement for timed automata. In *International Conference on Formal Modeling and Analysis of Timed Systems*, pages 114–129. Springer, 2007.

[dR10] Luca de Alfaro and Pritam Roy. Solving games via three-valued abstraction refinement. *Information and Computation*, 208(6):666–676, 2010. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007).

[EDMM02] Eyal Even-Dar, Shie Mannor, and Yishay Mansour. Pac bounds for multi-armed bandit and markov decision processes. In *COLT'02*, volume 2375 of LNCS, pages 255–270. Springer, 2002.

[EFGP10] Rudiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jorg Peter. Fully symbolic timed model checking using constraint matrix diagrams. In *Proc. 31th IEEE Real-Time Systems Symposium (RTSS'10)*, pages 360–371. IEEE Computer Society Press, 2010.

[EKVY08] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. *Logical Methods in Computer Science*, 4(4), 2008.

[FKL89] Jerzy A Filar, Lodewijk CM Kallenberg, and Huey-Miin Lee. Variance-penalized Markov decision processes. *Mathematics of Operations Research*, 14(1):147–161, 1989.

[FKR95] Jerzy A. Filar, Dmitry Krass, and Kirsten W. Ross. Percentile performance criteria for limiting average Markov decision processes. *Automatic Control, IEEE Transactions on*, 40(1):2–10, Jan 1995.

[GBGE14] William N Goetzmann, Stephen J Brown, Martin J Gruber, and Edwin J Elton. *Modern portfolio theory and investment analysis*. John Wiley & Sons, 2014.

[GGL13] G. Geeraerts, J. Goossens, and M. Lindström. Multiprocessor schedulability of arbitrary-deadline sporadic tasks: Complexity and antichain algorithm. *Real-Time Systems, The International Journal of Time-Critical Computing Systems*, 48(2), 2013.

[GHJ97] Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. Robust timed automata. In *Proc. International Workshop on Hybrid and Real-Time Systems (HART'97)*, volume 1201 of *Lecture Notes in Computer Science*, pages 331–345. Springer, 1997.

[GS97] Susanne Graf and Hassen Saidi. Construction of abstract state graphs with pvs. In *International Conference on Computer Aided Verification*, pages 72–83. Springer, 1997.
[HJ94] Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. *Formal aspects of computing*, 6(5):512–535, 1994.

[HJMM04] Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L McMillan. Abstractions from proofs. In *Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 232–244, 2004.

[HJMS02] Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy abstraction. In *Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 58–70, 2002.

[HJMS03] Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software verification with blast. In *International SPIN Workshop on Model Checking of Software*, pages 235–239. Springer, 2003.

[HK14] Christoph Haase and Stefan Kiefer. The odds of staying on budget. *CoRR*, abs/1409.8228, 2014.

[HK15] Christoph Haase and Stefan Kiefer. The odds of staying on budget. In *Proc. of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP), Part II*, volume 9135 of *Lecture Notes in Computer Science*, pages 234–246. Springer, 2015.

[HKSW11] Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India*, pages 78–89, 2011.

[HNSY94] Thomas A Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. *Information and computation*, 111(2):193–244, 1994.

[HP] Frédéric Herbreteau and Gérald Point. The TChecker tool and libraries. https://github.com/ticktac-project/tchecker.

[HS06] Thomas A. Henzinger and Joseph Sifakis. The embedded systems design challenge. In *Formal Methods, 14th International Symposium on Formal Methods*, volume 4085 of *Lecture Notes in Computer Science*, pages 1–15, Hamilton, Canada, 2006. Springer.

[HSTW20] Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why liveness for timed automata is hard, and what we can do about it. In *ACM Transactions on Computational Logic (TOCL)*, 21(3):1–28, 2020.

[HSW13] Frédéric Herbreteau, Balaguru Srivathsan, and Igor Walukiewicz. Lazy abstractions for timed automata. In *International Conference on Computer Aided Verification*, pages 990–1005. Springer, 2013.

[HZH$^{+}$10] Fei He, He Zhu, William NN Hung, Xiaoyu Song, and Ming Gu. Compositional abstraction refinement for timed systems. In *2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering*, pages 168–176. IEEE, 2010.
[IHS14] Malte Isberner, Falk Howar, and Bernhard Steffen. The ttt algorithm: a redundancy-free approach to active automata learning. In *International Conference on Runtime Verification*, pages 307–322. Springer, 2014.

[IHS15] Malte Isberner, Falk Howar, and Bernhard Steffen. The open-source learnlib. In Daniel Kroening and Corina S. Päsäreanu, editors, *Computer Aided Verification*, pages 487–495, Cham, 2015. Springer International Publishing.

[Jaq73] Stratton C. Jaquette. Markov Decision Processes with a New Optimality Criterion: Discrete Time. *The Annals of Statistics*, 1(3):496 – 505, 1973.

[JPA+22] Swen Jacobs, Guillermo A Perez, Remco Abraham, Veronique Bruyere, Michael Cadil-hac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, et al. The reactive synthesis competition (syntcomp): 2018-2021. *arXiv preprint arXiv:2206.00251*, 2022.

[JR11a] Rémi Jaubert and Pierre-Alain Reynier. Quantitative robustness analysis of flat timed automata. In *Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software*, volume 6604 of *Lecture Notes in Computer Science*, pages 229–244. Springer, 2011.

[JR11b] Rémi Jaubert and Pierre-Alain Reynier. Quantitative robustness analysis of flat timed automata. In *Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11)*, volume 6604 of *Lecture Notes in Computer Science*, pages 229–244. Springer, 2011.

[KA06] Branislav Kusy and Sherif Abdelwahed. Fsp protocol verification using spin. May 2006.

[Kal11] Lodewijk Kallenberg. *Markov Decision Processes*. Lecture Notes. University of Leiden, 2011.

[KJN11] Roland Kindermann, Tommi Junttila, and Ilkka Niemela. Modeling for symbolic analysis of safety instrumented systems with clocks. In *Proc. 11th International Conference on Application of Concurrency to System Design (ACSD'11)*, pages 185–194. IEEE Computer Society Press, 2011.

[KLMP14] Piotr Kordy, Rom Langerak, Sjouke Mauw, and Jan Willem Polderman. A symbolic algorithm for the analysis of robust timed automata. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, *FM 2014: Formal Methods*, volume 8442 of *Lecture Notes in Computer Science*, pages 351–366. Springer, 2014.

[KM18] Jan Kretínský and Tobias Meggendorfer. Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In *33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 609–618. ACM, 2018.

[KS05] Antonín Kučera and Oldřich Stražovský. On the controller synthesis for finite-state markov decision processes. In *FSTTCS 2005*, volume 3821 of LNCS, pages 541–552. Springer, 2005.
[KSBD15] Daniel Krähmann, Jana Schubert, Christel Baier, and Clemens Dubslaff. Ratio and weight quantiles. In *40th International Conference on Mathematical Foundations of Computer Science 2015 Symposium (MFCS), Part I*, volume 9234 of *Lecture Notes in Computer Science*, pages 344–356. Springer, 2015.

[KU02] Igor O. Kozine and Lev V. Utkin. Interval-valued finite markov chains. *Reliable computing*, 8(2):97–113, 2002.

[Kur87] Masami Kurano. Markov decision processes with a minimum-variance criterion. *Journal of mathematical analysis and applications*, 123(2):572–583, 1987.

[LAL+14] Shang-Wei Lin, Étienne André, Yang Liu, Jun Sun, and Jin Song Dong. Learning assumptions for compositional verification of timed systems. *Transactions on Software Engineering*, 40(2):137–153, mar 2014.

[Lam87] Leslie Lamport. A fast mutual exclusion algorithm. *ACM Trans. Comput. Syst.*, 5(1):1–11, jan 1987.

[Lam05] Leslie Lamport. Real-time model checking is really simple. In *Advanced Research Working Conference on Correct Hardware Design and Verification Methods*, pages 162–175. Springer, 2005.

[LLTW11] Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, and Andrzej Wasowski. Robust specification of real time components. In Uli Fahrenberg and Stavros Tripakis, editors, *Formal Modeling and Analysis of Timed Systems*, volume 6919 of *Lecture Notes in Computer Science*, pages 129–144. Springer, 2011.

[LLTW14] Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, and Andrzej Wasowski. Robust synthesis for real-time systems. *Theor. Comput. Sci.*, 515:96–122, 2014.

[LOD+13] Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, and Jaco van de Pol. Multi-core emptiness checking of timed büchi automata using inclusion abstraction. In *CAV 2013*, volume 8044 of *Lecture Notes in Computer Science*, pages 968–983. Springer, 2013.

[LvBP94] Gang Luo, G. von Bochmann, and A. Petrenko. Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method. *IEEE Transactions on Software Engineering*, 20(2):149–162, 1994.

[Man71] Petr Mandl. On the variance in controlled Markov chains. *Kybernetika*, 7(1):1–12, 1971.

[Mar52] Harry Markowitz. Portfolio selection. *The Journal of Finance*, 7(1):77–91, 1952.

[McI09] A. I. McInnes. Model-checking the flooding time synchronization protocol. In *Control and Automation, 2009. ICCA 2009. IEEE International Conference on*, pages 422–429, Dec 2009.

[MKSL04] Miklós Maróti, Branislav Kusy, Gyula Simon, and Ákos Lédeczki. The flooding time synchronization protocol. In *Proceedings of the 2Nd International Conference on Embedded Networked Sensor Systems*, SenSys ’04, pages 39–49, New York, NY, USA, 2004. ACM.
[MM14] Oded Maler and Irini-Eleftheria Mens. Learning regular languages over large alphabets. In Erika Ábrahám and Klaus Havelund, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, pages 485–499, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.

[MM17] Oded Maler and Irini-Eleftheria Mens. A generic algorithm for learning symbolic automata from membership queries. In Luca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, editors, *Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday*, pages 146–169, Cham, 2017. Springer International Publishing.

[MM21] Richard Mayr and Eric Munday. Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs. In Serge Haddad and Daniele Varacca, editors, *32nd International Conference on Concurrency Theory (CONCUR 2021)*, volume 203 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 12:1–12:15, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[MPS95] Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In *STACS*, pages 229–242, 1995.

[MSTW17] Richard Mayr, Sven Schewe, Patrick Totzke, and Dominik Wojtczak. MDPs with energy-parity objectives. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, IEEE Computer Society, pages 1–12, 2017.

[MT04] Shie Mannor and John N. Tsitsiklis. The sample complexity of exploration in the multi-armed bandit problem. *J. Mach. Learn. Res.*, 5:623–648, December 2004.

[MT11] Shie Mannor and John N. Tsitsiklis. Mean-variance optimization in Markov decision processes. In *Proceedings of the 28th International Conference on Machine Learning*, ICML’11, page 177–184, Madison, WI, USA, 2011. Omnipress.

[NEG05] Arnab Nilim and Laurent El Ghaoui. Robust control of markov decision processes with uncertain transition matrices. *Operations Research*, 53(5):780–798, 2005.

[NSL+12a] Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, and Yan Liu. Improved BDD-based discrete analysis of timed systems. In *Proc. 20th International Symposium on Formal Methods (FM’12)*, volume 7436, pages 326–340. Springer, 2012.

[NSL+12b] Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, and Yan Liu. Improved BDD-based discrete analysis of timed systems. In Dimitra Giannakopoulou and Dominique Méry, editors, *Proceedings of the 18th International Symposium on Formal Methods (FM’12)*, volume 7436 of *Lecture Notes in Computer Science*, pages 326–340. Springer-Verlag, August 2012.

[Oht04] Yoshio Ohtsubo. Optimal threshold probability in undiscounted Markov decision processes with a target set. *Applied Mathematics and Computation*, 149(2):519–532, 2004.

[PB19] Jakob Piribauer and Christel Baier. Partial and conditional expectations in Markov decision processes with integer weights. In Mikolaj Bojanczyk and Alex Simpson, editors,
22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 11425 of Lecture Notes in Computer Science, pages 436–452. Springer, 2019.

[PB20] Jakob Piribauer and Christel Baier. On Skolem-hardness and saturation points in Markov decision processes. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP), volume 168 of LIPIcs, pages 138:1–138:17. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2020.

[PEM11] Hans-Jörg Peter, Rüdiger Ehlers, and Robert Mattmüller. Synthia: Verification and synthesis for timed automata. In International Conference on Computer Aided Verification, pages 649–655. Springer, 2011.

[PGB$^{+08}$] Corina S Păsăreanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design, 32(3):175–205, 2008.

[Pir21] Jakob Piribauer. On Non-Classical Stochastic Shortest Path Problems. PhD thesis, Technische Universität Dresden, Germany, 2021.

[Pnu77] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57. ieee, 1977.

[Pra64] John W. Pratt. Risk aversion in the small and in the large. Econometrica, 32(1/2):122–136, 1964.

[Pur00] Anuj Puri. Dynamical properties of timed automata. Discrete Event Dynamic Systems, 10(1-2):87–113, 2000.

[Put94] Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, NY, USA, 1st edition, 1994.

[RAB$^{+95}$] Rajeev K Ranjan, Adnan Aziz, Robert K Brayton, Bernard Plessier, and Carl Pixley. Efficient bdd algorithms for FSM synthesis and verification. IWLS95, Lake Tahoe, CA, 253:254, 1995.

[RS93] R.L. Rivest and R.E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299–347, 1993.

[SB03] Sanjit A. Seshia and Randal E. Bryant. Unbounded, fully symbolic model checking of timed automata using boolean methods. In Warren A. Hunt and Fabio Somenzi, editors, Computer Aided Verification, pages 154–166, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.

[SB18] Richard S Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.

[SF07] M. Swaminathan and M. Franzle. A symbolic decision procedure for robust safety of timed systems. In Temporal Representation and Reasoning, 14th International Symposium on, pages 192–192, June 2007.
[SFK08] Mani Swaminathan, Martin Fränzle, and Joost-Pieter Katoen. The surprising robustness of (closed) timed automata against clock-drift. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and Luke Ong, editors, *Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008*, volume 273, pages 537–553. Springer, 2008.

[SO13] Masahiko Sakaguchi and Yoshio Ohtsubo. Markov decision processes associated with two threshold probability criteria. *Journal of Control Theory and Applications*, 11(4):548–557, 2013.

[Sob82] Matthew J. Sobel. The variance of discounted markov decision processes. *Journal of Applied Probability*, 19(4):794–802, 1982.

[Sob94] Matthew J. Sobel. Mean-variance tradeoffs in an undiscounted mdp. *Operations Research*, 42(1):175–183, 1994.

[TM15] Yann Thierry-Mieg. Symbolic model-checking using ITS-tools. In *Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15)*, pages 231–237. Springer, 2015.

[TM17] Tamás Tóth and István Majzik. Lazy reachability checking for timed automata using interpolants. In *International Conference on Formal Modeling and Analysis of Timed Systems*, pages 264–280. Springer, 2017.

[Tra16] Thanh-Tung Tran. Verification of timed automata : reachability, liveness and modelling. (Vérification d'automates temporisés : sûreté, vivacité et modélisation). PhD thesis, University of Bordeaux, France, 2016.

[UB13] Michael Ummels and Christel Baier. Computing quantiles in Markov reward models. In *Proc. of the 16th International Conference on Foundations of Software Science and Computation Structures (FOSSACS)*, volume 7794 of *Lecture Notes in Computer Science*, pages 353–368. Springer, 2013.

[vdVJJ23] Marck van der Vegt, Nils Jansen, and Sebastian Junges. Robust almost-sure reachability in multi-environment mdps, 2023.

[Ver04] Tom Verhoeff. Reward variance in Markov chains: A calculational approach. In *Proceedings of Eindhoven FASTAR Days*. Citeseer, 2004.

[Wan01] Farn Wang. Symbolic verification of complex real-time systems with clock-restriction diagram. In *Proc. 21st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’01)*, volume 197 of *IFIP Conference Proceedings*, pages 235–250. Kluwer, 2001.

[WG15] Xiao Wu and Xianping Guo. First passage optimality and variance minimisation of Markov decision processes with varying discount factors. *Journal of Applied Probability*, 52(2):441–456, 2015.

[Whi93] Douglas J. White. Minimizing a threshold probability in discounted Markov decision processes. *Journal of Mathematical Analysis and Applications*, 173(2):634–646, 1993.
[WL99] Congbin Wu and Yuanlie Lin. Minimizing risk models in Markov decision processes with policies depending on target values. *Journal of Mathematical Analysis and Applications*, 231(1):47–67, 1999.

[Xia16] Li Xia. Optimization of Markov decision processes under the variance criterion. *Automatica*, 73:269–278, 2016.

[Xia18a] Li Xia. Mean–variance optimization of discrete time discounted Markov decision processes. *Automatica*, 88:76–82, 2018.

[Xia18b] Li Xia. Variance minimization of parameterized Markov decision processes. *Discrete Event Dynamic Systems*, 28(1):63–81, 2018.

[Xia20] Li Xia. Risk-sensitive Markov decision processes with combined metrics of mean and variance. *Production and Operations Management*, 29(12):2808–2827, 2020.

[XM11] Huan Xu and Shie Mannor. Probabilistic goal Markov decision processes. In *IJCAI*, pages 2046–2052, 2011.