R. Alur and M. Bernadsky, Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems, Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control, pp.19-33, 2006.
DOI : 10.1007/11730637_5

[. Alur, C. Courcoubetis, and D. L. Dill, Model-checking for probabilistic real-time systems, Proceedings of the 18th International Colloquium on Automata, Languages and Programming (ICALP'91), pp.115-126, 1991.
DOI : 10.1007/3-540-54233-7_128

[. Alur, C. Courcoubetis, and D. L. Dill, Verifying automata specifications of probabilistic real-time systems, Proceedings of the REX Workshop on Real-Time: Theory in Practice, pp.28-44, 1992.
DOI : 10.1007/BFb0031986

R. Alur and D. L. Dill, Automata for modeling real-time systems, Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP'90), pp.322-335, 1990.
DOI : 10.1007/BFb0032042

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

[. Alur, L. Fix, and T. A. Henzinger, A determinizable class of timed automata, Proceedings of the 6th International Conference on Computer Aided Verification (CAV'94), pp.1-13, 1994.
DOI : 10.1007/3-540-58179-0_39

[. Alur, S. L. Torre, and G. J. Pappas, Optimal Paths in Weighted Timed Automata, Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control, pp.49-62, 2001.
DOI : 10.1007/3-540-45351-2_8

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis, Controller synthesis for timed automata, Proceedings of IFAC Symposium on System Structure and Control, pp.469-474, 1998.

A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic, vol.1, issue.1, pp.162-170, 2000.
DOI : 10.1145/343369.343402

J. Karl, N. Aström, E. Basset, and . Asarin, Optimal control of Markov decision processes with incomplete state estimation Thin and thick timed regular languages, Proceedings of the 9th International Colloquium on Formal Modeling and Analysis of Timed Systems (FORMATS'11), pp.174-205, 1965.

[. Basset, A Maximal Entropy Stochastic Process for a Timed Automaton,, Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13), pp.61-73, 2013.
DOI : 10.1007/978-3-642-39212-2_9
URL : https://hal.archives-ouvertes.fr/hal-00808909

[. Briones and E. Brinksma, A Test Generation Framework for quiescent Real-Time Systems, Proceedings of the 4th International Workshop on Formal Approaches to Software Testing, pp.64-78, 2005.
DOI : 10.1007/978-3-540-24732-6_8

C. Baier, N. Bertrand, P. Bouyer, T. Brihaye, and M. Größer, Probabilistic and Topological Semantics for Timed Automata, Proceedings of the 27th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp.179-191, 2007.
DOI : 10.1007/978-3-540-77050-3_15
URL : https://hal.archives-ouvertes.fr/inria-00424526

C. Baier, N. Bertrand, P. Bouyer, T. Brihaye, and M. Größer, Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.217-226, 2008.
DOI : 10.1109/LICS.2008.25
URL : https://hal.archives-ouvertes.fr/inria-00424520

N. Bertrand, P. Bouyer, T. Brihaye, Q. Menet, C. Baier et al., Stochastic Timed Automata, Logical Methods in Computer Science, vol.10, issue.4, p.2014
DOI : 10.2168/LMCS-10(4:6)2014
URL : https://hal.archives-ouvertes.fr/hal-01102368

C. Baier, N. Bertrand, P. Bouyer, and T. Brihaye, When Are Timed Automata Determinizable?, Proceedings of the 36th International Colloquium on Automata, Languages and Programming, pp.43-54, 2009.
DOI : 10.1007/978-3-642-02930-1_4
URL : https://hal.archives-ouvertes.fr/inria-00424351

N. Bertrand, P. Bouyer, T. Brihaye, and N. Markey, Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.55-64, 2008.
DOI : 10.1109/QEST.2008.19
URL : https://hal.archives-ouvertes.fr/inria-00424518

N. Bertrand, P. Bouyer, T. Brihaye, and A. Stainer, Emptiness and Universality Problems in Timed Automata with Positive Frequency, Proceedings of the 38th International Colloquium on Automata, Languages and Programming, pp.246-257, 2011.
DOI : 10.1007/978-3-540-28644-8_25
URL : https://hal.archives-ouvertes.fr/inria-00629172

N. Baier, M. Bertrand, and . Größer, On decision problems for probabilistic Büchi automata, Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pp.287-301, 2008.

N. Baier, M. Bertrand, and . Grösser, Probabilistic ??-automata, Journal of the ACM, vol.59, issue.1, 2012.
DOI : 10.1145/2108242.2108243
URL : https://hal.archives-ouvertes.fr/hal-00743907

N. Bertrand, T. Brihaye, and B. Genest, Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata, Proceedings of the 11th International Conference on Quantitative Evaluation of Systems (QEST'14), pp.313-328, 2014.
DOI : 10.1007/978-3-319-10696-0_25
URL : https://hal.archives-ouvertes.fr/hal-01088113

P. Ballarini, N. Bertrand, A. Horváth, M. Paolieri, and E. Vicario, Transient Analysis of Networks of Stochastic Timed Automata Using Stochastic State Classes, Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST'13), pp.355-371, 2013.
DOI : 10.1007/978-3-642-40196-1_30
URL : https://hal.archives-ouvertes.fr/hal-00915026

P. Bouyer, T. Brihaye, M. Jurdzinski, and Q. Menet, Almost-Sure Model-Checking of Reactive Timed Automata, 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp.138-147, 2012.
DOI : 10.1109/QEST.2012.10

[. Bouyer, E. Brinksma, and K. G. Larsen, Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design, BBS06] Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. A note on the attractorproperty of infinite-state Markov chains. Information Processing Letters, pp.2-2358, 2006.

[. Bouyer, F. Chevalier, D. Deepak, and . Souza, Fault Diagnosis Using Timed Automata, Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'05), pp.219-233, 2005.
DOI : 10.1007/978-3-540-31982-5_14

[. Berwanger and L. Doyen, On the power of imperfect information, Proceedings of 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'08), volume 2 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.73-82, 2008.

E. Peter, A. Bulychev, K. G. David, A. Larsen, G. Legay et al., Monitor-based statistical model checking for weighted metric temporal logic, 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'18), pp.168-182, 2012.

N. Bertrand and P. Fournier, Parameterized verification of many identical probabilistic timed processes, Proceedings of the 33rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'13), volume 24 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.501-513, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00914263

A. Bfh-+-01-]-gerd-behrmann, T. Fehnker, K. G. Hune, P. Larsen, J. Pettersson et al., Minimum-cost reachability for priced timed automata, Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of Lecture Notes in Computer Science, pp.147-161, 2001.

N. Bertrand, E. Fabre, S. Haar, S. Haddad, and L. Hélouët, Active Diagnosis for Probabilistic Systems, Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), pp.29-42, 2014.
DOI : 10.1007/978-3-642-54830-7_2
URL : https://hal.archives-ouvertes.fr/hal-00930919

P. Bouyer, U. Fahrenberg, K. G. Larsen, and N. Markey, Quantitative analysis of real-time systems using priced timed automata, Communications of the ACM, vol.54, issue.9, pp.78-87, 2011.
DOI : 10.1145/1995376.1995396
URL : https://hal.archives-ouvertes.fr/hal-01088030

N. Bertrand, P. Fournier, and A. Sangnier, Playing with Probabilities in Reconfigurable Broadcast Networks, Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), pp.134-148, 2014.
DOI : 10.1007/978-3-642-54830-7_9
URL : https://hal.archives-ouvertes.fr/hal-01082129

N. Bertrand, P. Fournier, and A. Sangnier, Distributed local strategies in broadcast networks, Proceedings of the 26th International Conference on Concurrency Theory (CONCUR'15), volume 42 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.44-57, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01243595

C. Baier and M. Größer, Recognizing omega-regular languages with probabilistic automata, Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS'05), pp.137-146, 2005.

N. Bertrand and B. Genest, Minimal disclosure in partially observable Markov decision processes, Proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), volume 13 of Leibniz International Proceedings in Informatics Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.411-422, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00672845

N. Bertrand, B. Genest, and H. Gimbert, Qualitative Determinacy and Decidability of Stochastic Games with Signals, 2009 24th Annual IEEE Symposium on Logic In Computer Science, pp.319-328, 2009.
DOI : 10.1109/LICS.2009.31
URL : https://hal.archives-ouvertes.fr/hal-00356566

N. Bertrand and S. Haddad, Contrôle, probabilités et observation partielle, Informatique Mathématique : Une photographie en 2015, pp.177-227, 2015.

C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, Model-checking algorithms for continuous-time markov chains, IEEE Transactions on Software Engineering, vol.29, issue.6, pp.524-541, 2003.
DOI : 10.1109/TSE.2003.1205180

[. Bertrand, S. Haddad, and E. Lefaucheux, Foundation of diagnosis and predictability in probabilistic systems, Proceedings of the 34th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.417-429, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01088117

N. Bertrand, T. Jéron, A. Stainer, and M. Krichen, Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), pp.96-111, 2011.
DOI : 10.1016/j.ipl.2006.04.015
URL : https://hal.archives-ouvertes.fr/inria-00550923

N. Bertrand, T. Jéron, A. Stainer, and M. Krichen, Off-line test selection with test purposes for non-deterministic timed automata, Logical Methods in Computer Science, vol.8, issue.4, p.2012
URL : https://hal.archives-ouvertes.fr/inria-00550923

C. Baier and J. Katoen, Principles of model checking, 2008.

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, Modal event-clock specifications for timed component-based design, Science of Computer Programming, vol.77, issue.12, pp.1212-1234, 2012.
DOI : 10.1016/j.scico.2011.01.007
URL : https://hal.archives-ouvertes.fr/hal-00752449

[. Bouyer, N. Markey, and O. Sankur, Robustness in Timed Automata, Proceedings of the 7th Workshop on Reachability Problems in Computational Models (RP'13), pp.1-18, 2013.
DOI : 10.1007/978-3-642-41036-9_1

N. Bertrand, S. Pinchinat, and J. Raclet, Refinement and Consistency of Timed Modal Specifications, Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), pp.152-163, 2009.
DOI : 10.1007/3-540-56922-7_21
URL : https://hal.archives-ouvertes.fr/inria-00424283

G. Bucci, R. Piovosi, L. Sassoli, and E. Vicario, Introducing probability within state class analysis of dense-time-dependent systems, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), pp.13-22, 2005.
DOI : 10.1109/QEST.2005.17

G. Bruce, E. H. Buchanan, and . Shortliffe, Rule Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project, 1984.

N. Bertrand and P. Schnoebelen, Model Checking Lossy Channels Systems Is Probably Decidable, Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'03), pp.120-135, 2003.
DOI : 10.1007/3-540-36576-1_8
URL : https://hal.archives-ouvertes.fr/inria-00424339

N. Bertrand and S. Schewe, Playing Optimally on Timed Automata with Random Delays, Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'12), pp.43-58, 2012.
DOI : 10.1007/978-3-642-33365-1_5
URL : https://hal.archives-ouvertes.fr/hal-00752440

N. Bertrand and P. Schnoebelen, Computable fixpoints in well-structured symbolic model checking. Formal Methods in System Design, pp.233-267, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00906826

N. Bertrand and P. Schnoebelen, Solving stochastic büchi games on infinite arenas with a finite attractor, Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'13) of Electronic Proceedings in Theoretical Computer Science, pp.116-131, 2013.

N. Bertrand, A. Stainer, T. Jéron, and M. Krichen, A Game Approach to Determinize Timed Automata, Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), pp.245-259, 2011.
DOI : 10.1007/978-3-642-19805-2_17
URL : https://hal.archives-ouvertes.fr/hal-01102472

N. Bertrand, A. Stainer, T. Jéron, and M. Krichen, A game approach to determinize timed automata Formal Methods in System Design Partial-observation stochastic games: How to win when belief fails, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS'12), pp.42-80, 2012.

[. Chatterjee, M. Luca-de-alfaro, A. Faella, and . Legay, Qualitative logics and equivalences for probabilistic systems, Logical Methods in Computer Science, vol.5, issue.2, 2009.

[. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, Randomness for Free, Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science 2010 (MFCS'10), pp.246-257, 2010.
DOI : 10.1007/978-3-642-15155-2_23
URL : https://hal.archives-ouvertes.fr/hal-01006409

[. Chatterjee, L. Doyen, and T. A. Henzinger, A survey of partialobservation stochastic parity games. Formal Methods in System Design, pp.268-284, 2013.

K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, Algorithms for Omega-Regular Games with Imperfect Information, Logical Methods in Computer Science, vol.3, issue.34, pp.1-23, 2007.
DOI : 10.1007/11874683_19

T. Chen, T. Han, J. Katoen, and A. Mereacre, Modelchecking of continuous-time Markov chains against timed automata specifications, Logical Methods in Computer Science, vol.7, issue.112, pp.1-34, 2011.

J. Chen and R. Kumar, Polynomial Test for Stochastic Diagnosability of Discrete-Event Systems, IEEE Transactions on Automation Science and Engineering, vol.10, issue.4, pp.969-979, 2013.
DOI : 10.1109/TASE.2013.2251334

J. Chen and R. Kumar, Failure prognosability of stochastic discrete event systems, Proceedings of the American Control Conference (ACC'14), pp.2041-2046, 2014.

R. Chadha, A. P. Sistla, and M. Viswanathan, On the expressiveness and complexity of randomization in finite state monitors, Journal of the ACM, vol.56, issue.5, 2009.

R. Chadha, A. P. Sistla, and M. Viswanathan, Power of Randomization in Automata on Infinite Strings, Proceedings of the 20th International Conference on Concurrency Theory, pp.229-243, 2009.
DOI : 10.1016/S0019-9958(63)90290-0

R. Chadha, A. P. Sistla, M. Viswanathan, and Y. Ben, Decidable and Expressive Classes of Probabilistic Automata, Proceedings of the 18th International Conference onFoundations of Software Science and Computation Structures (FoSSaCS'15 Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00), pp.200-214, 2000.
DOI : 10.1007/978-3-662-46678-0_13

D. Pedro, H. Argenio, J. Hermanns, R. Katoen, and . Klaren, MoDeST -A modelling and description language for stochastic timed systems, Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV'01), volume 2165 of Lecture Notes in Computer Science, pp.87-104, 2001.

[. Donatelli, S. Haddad, and J. Sproston, Model Checking Timed and Stochastic Properties with CSL^{TA}, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.224-240, 2009.
DOI : 10.1109/TSE.2008.108

K. G. David, A. Larsen, U. Legay, A. Nyman, and . Wasowski, Timed I/O automata, Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, HSCC '10, pp.91-100, 2010.
DOI : 10.1145/1755952.1755967

G. Delzanno, A. Sangnier, R. Traverso, and G. Zavattaro, On the complexity of parameterized reachability in reconfigurable broadcast networks, Proceedings of the 32nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), volume 18 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.289-300, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00740518

G. Delzanno, A. Sangnier, and G. Zavattaro, Parameterized Verification of Ad Hoc Networks, Proceedings of the 21st International Conference on Concurrency Theory (CONCUR'10), pp.313-327, 2010.
DOI : 10.1007/978-3-642-15375-4_22

G. Delzanno, A. Sangnier, and G. Zavattaro, On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks, Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS'11), pp.441-455, 2011.
DOI : 10.1007/978-3-642-19805-2_30

G. Delzanno, A. Sangnier, and G. Zavattaro, Parameterized Verification of Safety Properties in Ad Hoc Network Protocols, Proceedings of the 1st International Workshop on Process Algebra and Coordination (PACO'11), volume 60 of Electronic Proceedings in Theoretical Computer Science, pp.56-65, 2011.
DOI : 10.4204/EPTCS.60.4

G. Delzanno, A. Sangnier, and G. Zavattaro, Verification of Ad Hoc Networks with Node and Communication Failures, Proceedings of the joint 14th IFIP WG 6.1 International Conference and 32nd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS, pp.235-250, 2012.
DOI : 10.1007/978-3-642-30793-5_15
URL : https://hal.archives-ouvertes.fr/hal-00909367

O. Finkel, Undecidable Problems About Timed Automata, Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems (FOR- MATS'06), pp.187-199, 2006.
DOI : 10.1007/11867340_14
URL : https://hal.archives-ouvertes.fr/hal-00121529

M. Fruth, Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol, Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (isola 2006), pp.290-297, 2006.
DOI : 10.1109/ISoLA.2006.34

H. Gimbert and Y. Oualhadj, Probabilistic Automata on Finite Words: Decidable and Undecidable Problems, Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10), pp.527-538, 2010.
DOI : 10.1007/978-3-642-14162-1_44
URL : https://hal.archives-ouvertes.fr/hal-00456538

V. Gripon and O. Serre, Qualitative Concurrent Stochastic Games with Imperfect Information, Proceedings of the 36th International Colloquium on Automata, Languages and Programming, pp.200-211, 2009.
DOI : 10.1007/978-3-642-02930-1_17
URL : https://hal.archives-ouvertes.fr/hal-00360857

S. Haar, S. Haddad, T. Melliti, and S. Schwoon, Optimal constructions for active diagnosis, Proceedings of the 33rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'13), volume 24 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.527-539, 2013.
DOI : 10.1016/j.jcss.2016.04.007
URL : https://hal.archives-ouvertes.fr/hal-00926098

S. Jiang, Z. Huang, V. Chandra, and R. Kumar, A polynomial algorithm for testing diagnosability of discrete-event systems, IEEE Transactions on Automatic Control, vol.46, issue.8, pp.1318-1321, 2001.
DOI : 10.1109/9.940942

[. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston, Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, chapter Verification of Real-Time Probabilistic Systems, pp.249-288, 2008.

M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Verifying Quantitative Properties of Continuous Probabilistic Timed Automata, Proceedings of the 11th International Conference on Concurrency Theory, pp.123-137, 2000.
DOI : 10.1007/3-540-44618-4_11

M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol.282, issue.1, pp.101-150, 2002.
DOI : 10.1016/S0304-3975(01)00046-9

[. Kosaraju and G. F. Sullivan, Detecting cycles in dynamic graphs in polynomial time (preliminary version), STOC'88, pp.398-406, 1988.

M. Krichen and S. Tripakis, Conformance testing for real-time systems, Formal Methods in System Design, vol.10, issue.1???2, pp.238-304, 2009.
DOI : 10.1007/s10703-009-0065-1

I. S. Joost-pieter-katoen, E. Zapreev, H. Moritz-hahn, D. N. Hermanns, and . Jansen, The Ins and Outs of The Probabilistic Model Checker MRMC, Proceedings of the 6th International Conference on the Quantitative Evaluation of Systems Quantitative (QEST'09), pp.167-176, 2009.

[. Lusena, J. Goldsmith, and M. Mundhenk, Nonapproximability results for partially observable Markov decision processes, Journal of Artificial Intelligence Research, vol.14, 2001.

[. Laroussinie, N. Markey, and P. Schnoebelen, Model Checking Timed Automata with One or Two Clocks, Proceedings of the 15th International Conference on Concurrency Theory, pp.387-401, 2004.
DOI : 10.1007/3-540-45931-6_19
URL : https://hal.archives-ouvertes.fr/hal-01194617

J. Daniel, M. O. Lehmann, and . Rabin, On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem, Proceedings of the 8th ACM Symposium on Principles of Programming Languages (POPL'81), pp.133-138, 1981.

O. Madani, S. Hanks, and A. Condon, On the undecidability of probabilistic planning and related stochastic optimization problems, Artificial Intelligence, vol.147, issue.1-2, pp.5-34, 2003.
DOI : 10.1016/S0004-3702(02)00378-8

M. Minsky, Computation: Finite and Infinite Machines, 1967.

L. Manasa, S. Narayanan, and K. , Integer reset timed automata: Clock reduction and determinizability, 2010.

B. Nielsen and A. Skou, Automated test generation from timed automata, International Journal on Software Tools for Technology Transfer, vol.34, issue.1, pp.59-77, 2003.
DOI : 10.1007/s10009-002-0094-1

[. Parry, Intrinsic Markov chains. Transactions of the, pp.55-66, 1964.

A. Paz, Introduction to probabilistic automata, 1971.

[. Iyer and M. Narasimha, Probabilistic lossy channel systems, Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97, pp.667-681, 1997.
DOI : 10.1007/BFb0030633

A. Pnueli and R. Rosner, Distributed reactive systems are hard to synthesize, Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science, pp.746-757, 1990.
DOI : 10.1109/FSCS.1990.89597

J. [. Papadimitriou and . Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research, vol.12, issue.3, pp.441-450, 1987.
DOI : 10.1287/moor.12.3.441

A. Puri, Dynamical properties of timed automata. Discrete Event Dynamic Systems, pp.87-113, 2000.

O. Michael and . Rabin, Probabilistic automata, Information and Control, vol.6, issue.3, pp.230-245, 1963.

A. Rabinovich, Quantitative Analysis of Probabilistic Lossy Channel Systems, Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP'03), pp.1008-1021, 2003.
DOI : 10.1007/3-540-45061-0_78

J. H. Reif, The complexity of two-player games of incomplete information, Journal of Computer and System Sciences, vol.29, issue.2, pp.274-301, 1984.
DOI : 10.1016/0022-0000(84)90034-5

J. Renault, The Value of Repeated Games with an Informed Controller, Mathematics of Operations Research, vol.37, issue.1, 2007.
DOI : 10.1287/moor.1110.0518
URL : https://hal.archives-ouvertes.fr/hal-00266378

N. Markus, S. Rabe, and . Schewe, Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games, Acta Informatica, vol.48, pp.5-6291, 2011.

J. Raskin and O. Sankur, Multiple-environment Markov decision processes, Proceedings of the 34th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS'14), volume 29 of Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.531-543, 2014.

[. Rosenberg, E. Solan, and N. Vieille, Stochastic Games with Imperfect Monitoring, 2003.
DOI : 10.1007/0-8176-4501-2_1
URL : https://hal.archives-ouvertes.fr/hal-00464949

J. Peter, W. M. Ramadge, and . Wonham, Supervisory control of a class of discreteevent processes, SIAM Journal of Control and Optimization, vol.25, issue.1, pp.206-230, 1987.

S. Safra, On the complexity of omega -automata, [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pp.319-327, 1988.
DOI : 10.1109/SFCS.1988.21948

O. Sankur, P. Bouyer, N. Markey, and P. Reynier, Robust Controller Synthesis in Timed Automata, Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13), pp.546-560, 2013.
DOI : 10.1007/978-3-642-40184-8_38

P. Schnoebelen, Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters, vol.83, issue.5, pp.251-261, 2002.
DOI : 10.1016/S0020-0190(01)00337-4

C. Shannon, A Mathematical Theory of Communication, Bell System Technical Journal, vol.27, issue.3, pp.379-423, 1948.
DOI : 10.1002/j.1538-7305.1948.tb01338.x

J. Sun, Y. Liu, J. S. Dong, and J. Pang, PAT: Towards Flexible Verification under Fairness, 21st International Conference on Computer Aided Verification (CAV'09)SLT98] Meera Sampath, Stéphane Lafortune, and Demosthenis Teneketzis, pp.709-714908, 1971.
DOI : 10.1007/978-3-642-02658-4_59
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.151.806

S. Sorin, A first course on zero-sum repeated games, 2002.

[. Suman, P. K. Pandya, L. Shankara-narayanan-krishna, and . Manasa, Timed Automata with Integer Resets: Language Inclusion and Expressiveness, Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'08), pp.78-92, 2008.
DOI : 10.1007/978-3-540-85778-5_7

S. Schmitz and P. Schnoebelen, Algorithmic aspects of WQO theory, Lecture Notes, 2012.
URL : https://hal.archives-ouvertes.fr/cel-00727025

R. Sampath and . Sengupta, Diagnosability of discrete-event systems, IEEE Transactions on Automatic Control, vol.40, issue.9, pp.1555-1575, 1995.
DOI : 10.1109/9.412626

J. Schmaltz and J. Tretmans, On Conformance Testing for Timed Systems, Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'08), pp.250-264, 2008.
DOI : 10.1007/978-3-540-85778-5_18

A. Stainer, Frequencies in Forgetful Timed Automata, Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FOR- MATS'12), pp.236-251, 2012.
DOI : 10.1007/978-3-642-33365-1_17
URL : https://hal.archives-ouvertes.fr/hal-00744081

M. Stoelinga, Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.328-337, 2003.
DOI : 10.1007/s001650300009

M. Y. Safra and . Vardi, On ??-automata and temporal logic, Proceedings of the twenty-first annual ACM symposium on Theory of computing , STOC '89, pp.127-137, 1989.
DOI : 10.1145/73007.73019

M. Tracol, Recurrence and transcience for finite probabilistic tables, Theoretical Computer Science, vol.412, pp.12-141154, 2011.
DOI : 10.1016/j.tcs.2010.12.038
URL : http://doi.org/10.1016/j.tcs.2010.12.038

J. Tretmans, Test generation with inputs, outputs, and quiescence, Proc. of the second International workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'96), pp.127-146, 1996.
DOI : 10.1007/3-540-61042-1_42
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.475.9528

[. Tripakis, Folk theorems on the determinization and minimization of timed automata, Information Processing Letters, vol.99, issue.6, pp.222-226, 2006.
DOI : 10.1016/j.ipl.2006.04.015

D. Thorsley and D. Teneketzis, Diagnosability of stochastic discrete-event systems, IEEE Transactions on Automatic Control, vol.50, issue.4, pp.476-492, 2005.
DOI : 10.1109/TAC.2005.844722

[. Wolovick and S. Johr, A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes, Proceedings of the 4th International Conference Formal Modeling and Analysis of Timed Systems, pp.352-367, 2006.
DOI : 10.1007/11867340_25

T. Wang, J. Sun, Y. Liu, X. Wang, and S. Li, Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata, Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), pp.310-325, 2014.
DOI : 10.1007/978-3-642-54862-8_21

L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns, Automata-Based CSL Model Checking, Proceedings of the 38th International Colloquium on Automata, Languages and Programming, pp.271-282, 2011.
DOI : 10.1016/j.peva.2010.04.001