Y. Abdedda¨?mabdedda¨?m, A. Kerbaa, and O. Maler, Task graph scheduling using timed automata, IPDPS, p.237, 2003.

L. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba, Reactive Systems: Modeling, Specification and Verification, 2007.
DOI : 10.1017/CBO9780511814105

S. Xavier-allamigeon, E. Gaubert, and . Goubault, Inferring Min and Max Invariants Using Max-Plus Polyhedra, Lecture Notes in Computer Science, vol.5079, pp.189-204, 2008.
DOI : 10.1007/978-3-540-69166-2_13

R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. Ho et al., The algorithmic analysis of hybrid systems, Theoretical Computer Science, vol.138, issue.1, pp.3-34, 1995.
DOI : 10.1016/0304-3975(94)00202-T

R. Alur, Timed automata, Halbwachs and Peled, pp.8-22
DOI : 10.1007/978-3-642-59615-5_12

R. Alur, M. Bernadsky, and P. Madhusudan, Optimal Reachability for Weighted Timed Games, Lecture Notes in Computer Science, vol.3142, pp.122-133, 2004.
DOI : 10.1007/978-3-540-27836-8_13

R. Alur, C. Courcoubetis, and D. L. Dill, Model-checking for realtime systems, LICS, pp.414-425, 1990.

R. Alur and D. L. Dill, Automata for modeling real-time systems, Lecture Notes in Computer Science, vol.443, 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

R. Alur, S. L. Torre, and G. J. Pappas, Optimal paths in weighted timed automata, Benedetto and Sangiovanni-Vincentelli [26], pp.49-62

D. Andersson, Improved combinatorial algorithms for discounted payoff games, 2006.

E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli et al., Data-structures for the verification of timed automata, Lecture Notes in Computer Science, vol.1201, pp.346-360, 1997.
DOI : 10.1007/BFb0014737

E. Asarin, O. Maler, and A. Pnueli, Symbolic controller synthesis for discrete and timed systems, Hybrid Systems, pp.1-20, 1994.
DOI : 10.1007/3-540-60472-3_1

C. Baier, N. Bertrand, P. Bouyer, T. Brihaye, and M. Größer, Probabilistic and Topological Semantics for Timed Automata, FSTTCS, pp.179-191, 2007.
DOI : 10.1007/978-3-540-77050-3_15

URL : https://hal.archives-ouvertes.fr/inria-00424526

B. Barbot, T. Chen, T. Han, J. Katoen, and A. Mereacre, Efficient CTMC Model Checking of Linear Real-Time Objectives, Lecture Notes in Computer Science, vol.4, issue.2, pp.128-142, 2011.
DOI : 10.1007/978-3-642-12002-2_4

G. Behrmann, J. Bengtsson, A. David, K. G. Larsen, P. Pettersson et al., UppaaL Implementation Secrets, Lecture Notes in Computer Science, vol.2469, pp.3-22, 2002.
DOI : 10.1007/3-540-45739-9_1

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.9800

G. Behrmann, P. Bouyer, K. G. Larsen, and R. Pelánek, Lower and upper bounds in zone based abstractions of timed automata, pp.312-326

G. Behrmann, E. Brinksma, M. Hendriks, and A. Mader, Production scheduling by reachability analysis -a case study, IPDPS. IEEE Computer Society, 2005.

G. Behrmann, A. Cougnard, A. David, E. Fleury, K. G. Larsen et al., UPPAAL-Tiga: Time for Playing Games!, Lecture Notes in Computer Science, vol.4590, pp.121-125, 2007.
DOI : 10.1007/978-3-540-73368-3_14

URL : https://hal.archives-ouvertes.fr/hal-00350466

G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, SFM, pp.200-236, 2004.
DOI : 10.1007/978-3-540-30080-9_7

G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson et al., Minimum-Cost Reachability for Priced Timed Automata, Benedetto and Sangiovanni-Vincentelli [26], pp.147-161
DOI : 10.7146/brics.v8i3.20457

G. Behrmann, T. Hune, and F. W. Vaandrager, Distributing Timed Model Checking ??? How the Search Order Matters, Lecture Notes in Computer Science, vol.1855, pp.216-231, 2000.
DOI : 10.1007/10722167_19

G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi, Efficient timed reachability analysis using clock difference diagrams, Halbwachs and Peled, pp.341-353
DOI : 10.7146/brics.v5i47.19492

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4832

G. Behrmann, K. G. Larsen, and R. Pelánek, To Store or Not to Store, Lecture Notes in Computer Science, vol.2725, pp.433-445, 2003.
DOI : 10.1007/978-3-540-45069-6_40

G. Behrmann, K. G. Larsen, and J. Rasmussen, Optimal scheduling using priced timed automata, ACM SIGMETRICS Performance Evaluation Review, vol.32, issue.4, pp.34-40, 2005.
DOI : 10.1145/1059816.1059823

J. Bengtsson and W. Yi, On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata, Lecture Notes in Computer Science, vol.2885, pp.491-503, 2003.
DOI : 10.1007/978-3-540-39893-6_28

J. Bengtsson and W. Yi, Timed Automata: Semantics, Algorithms and Tools, Lectures on Concurrency and Petri Nets, pp.87-124, 2003.
DOI : 10.1007/978-3-540-27755-2_3

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.332.8701

B. Bérard, A. Petit, V. Diekert, and P. Gastin, Characterization of the expressive power of silent transitions in timed automata, Fundam. Inform, vol.36, issue.23, pp.145-182, 1998.

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

H. Bohnenkamp, P. R. D-'argenio, H. Hermanns, and J. Katoen, Modest: A compositional modeling formalism for real-time and stochastic systems, 2004.

P. Bouyer, T. Brihaye, and N. Markey, Improved undecidability results on weighted timed automata, Information Processing Letters, vol.98, issue.5, pp.188-194, 2006.
DOI : 10.1016/j.ipl.2006.01.012

URL : https://hal.archives-ouvertes.fr/hal-01194609

P. Bouyer, E. Brinksma, and K. G. Larsen, Staying Alive as Cheaply as Possible, Lecture Notes in Computer Science, vol.2993, pp.203-218, 2004.
DOI : 10.1007/978-3-540-24743-2_14

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.59

P. Bouyer, F. Cassez, E. Fleury, and K. G. Larsen, Optimal Strategies in Priced Timed Game Automata, Lecture Notes in Computer Science, vol.3328, pp.148-160, 2004.
DOI : 10.1007/978-3-540-30538-5_13

URL : https://hal.archives-ouvertes.fr/hal-00350483

P. Bouyer, U. Fahrenberg, K. G. Larsen, and N. Markey, Timed automata with observers under energy constraints, Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, HSCC '10, pp.61-70, 2010.
DOI : 10.1145/1755952.1755963

P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and J. Srba, Infinite Runs in Weighted Timed Automata with Energy Constraints, Lecture Notes in Computer Science, vol.5215, pp.33-47, 2008.
DOI : 10.1007/978-3-540-85778-5_4

URL : https://hal.archives-ouvertes.fr/hal-01194594

P. Bouyer, K. G. Larsen, and N. Markey, Lower-Bound Constrained Runs in Weighted Timed Automata, 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp.128-137, 2012.
DOI : 10.1109/QEST.2012.28

URL : https://hal.archives-ouvertes.fr/hal-01016100

P. Bouyer, K. G. Larsen, N. Markey, and J. Rasmussen, Almost Optimal Strategies in One Clock Priced Timed Games, Lecture Notes in Computer Science, vol.4337, pp.345-356, 2006.
DOI : 10.1007/11944836_32

M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis et al., Kronos: A model-checking tool for real-time systems, Lecture Notes in Computer Science, vol.1427, pp.546-550, 1998.
DOI : 10.1007/BFb0028779

URL : https://hal.archives-ouvertes.fr/hal-00374788

T. Brihaye, V. Bruyère, and J. Raskin, On Optimal Timed Strategies, pp.49-64
DOI : 10.1007/11603009_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.110.4228

E. Peter, A. Bulychev, K. G. David, A. Larsen, G. Legay et al., Monitor-based statistical model checking for weighted metric temporal logic, Lecture Notes in Computer Science, vol.7180, pp.168-182, 2012.

E. Peter, A. Bulychev, K. G. David, A. Larsen, M. Legay et al., Computing Nash equilibrium in wireless ad hoc networks: A simulation-based approach, EPTCS, vol.78, pp.1-14, 2012.

F. Cassez, A. David, E. Fleury, K. G. Larsen, and D. Lime, Efficient On-the-Fly Algorithms for the Analysis of Timed Games, Lecture Notes in Computer Science, vol.3653, pp.66-80, 2005.
DOI : 10.1007/11539452_9

URL : https://hal.archives-ouvertes.fr/hal-00350475

F. Cassez, A. David, K. G. Larsen, D. Lime, and J. Raskin, Timed Control with Observation Based and Stuttering Invariant Strategies, Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, pp.192-206, 1992.
DOI : 10.1007/978-3-540-75596-8_15

URL : https://hal.archives-ouvertes.fr/hal-00218336

C. Courcoubetis and M. Yannakakis, Minimum and maximum delay problems in real-time systems, Formal Methods in System Design, vol.443, issue.4, pp.399-409
DOI : 10.1007/BF00709157

R. D. Pedro, J. Argenio, T. C. Katoen, J. Ruys, and . Tretmans, The bounded retransmission protocol must be on time!, Lecture Notes in Computer Science, vol.1217, pp.416-431, 1997.

A. David, D. Du, K. G. Larsen, A. Legay, M. Mikucionis et al., Statistical Model Checking for Stochastic Hybrid Systems, Electronic Proceedings in Theoretical Computer Science, vol.92, pp.122-136, 2012.
DOI : 10.4204/EPTCS.92.9

URL : https://hal.archives-ouvertes.fr/hal-01088197

A. David, K. G. Larsen, A. Legay, M. Mikucionis, D. B. Poulsen et al., Runtime Verification of Biological Systems, Lecture Notes in Computer Science, vol.1, issue.7609, pp.388-404, 2012.
DOI : 10.1007/978-3-642-34026-0_29

URL : https://hal.archives-ouvertes.fr/hal-01088165

A. David, K. G. Larsen, A. Legay, M. Mikucionis, D. B. Poulsen et al., Statistical Model Checking for Networks of Priced Timed Automata, Lecture Notes in Computer Science, vol.10, issue.3, pp.80-96, 2011.
DOI : 10.1145/1755952.1755987

A. David, K. G. Larsen, A. Legay, M. Miku?ionis, and Z. Wang, Time for Statistical Model Checking of Real-Time Systems, Computer Aided Verification, pp.349-355, 2011.
DOI : 10.1007/s10009-005-0187-8

L. David and . Dill, Timing assumptions and verification of finite-state concurrent systems Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol.407, pp.197-212, 1989.

M. Duflot, M. Kwiatkowska, G. Norman, and D. Parker, A formal analysis of bluetooth device discovery, International Journal on Software Tools for Technology Transfer, vol.12, issue.3/4, pp.621-632, 2006.
DOI : 10.1007/s10009-006-0014-x

P. Juhan and . Ernits, Memory arbiter synthesis and verification for a radar memory interface card, Nord. J. Comput, vol.12, issue.2, pp.68-88, 2005.

U. Fahrenberg, L. Juhl, K. G. Larsen, and J. Srba, Energy Games in Multiweighted Automata, ICTAC, pp.95-115, 2011.
DOI : 10.1016/0304-3975(95)00188-3

URL : https://hal.archives-ouvertes.fr/hal-01088043

U. Fahrenberg and K. G. Larsen, Discount-Optimal Infinite Runs in Priced Timed Automata, Electronic Notes in Theoretical Computer Science, vol.239, pp.179-191, 2009.
DOI : 10.1016/j.entcs.2009.05.039

U. Fahrenberg and K. G. Larsen, Discounting in Time, Electronic Notes in Theoretical Computer Science, vol.253, issue.3, pp.25-31, 2009.
DOI : 10.1016/j.entcs.2009.10.003

U. Fahrenberg, K. G. Larsen, A. Legay, and C. Thrane, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Proceedings of the NATO Advanced Study Institute on Engineering Methods and Tools for Software Safety and Security Marktoberdorf, 2012.
DOI : 10.1007/3-540-48119-2_15

URL : https://hal.archives-ouvertes.fr/hal-01087921

U. Fahrenberg, K. G. Larsen, and C. Thrane, Verification, Performance Analysis and Controller Synthesis for Real-Time Systems, ASI 08 NATO Science for Peace and Security Series -D: Information and Communication Security, 2008.
DOI : 10.1007/978-3-642-11623-0_2

U. Fahrenberg, K. G. Larsen, and C. Thrane, Verification, Performance Analysis and Controller Synthesis for Real-Time Systems, Lecture Notes in Computer Science, vol.5961, pp.34-61, 2009.
DOI : 10.1007/978-3-642-11623-0_2

U. Fahrenberg, K. G. Larsen, and C. Thrane, Model-based verification and analysis for real-time systems, Software and Systems Safety -Specification and Verification NATO Science for Peace and Security Series -D: Information and Communication Security, pp.231-259, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01088054

A. Fehnker, Scheduling a steel plant with timed automata, Proceedings Sixth International Conference on Real-Time Computing Systems and Applications. RTCSA'99 (Cat. No.PR00306), pp.280-286, 1999.
DOI : 10.1109/RTCSA.1999.811256

R. Michael, J. Hansen, A. Madsen, and . Brekling, Semantics and verification of a language for modelling hardware architectures, Formal Methods and Hybrid Real-Time Systems, pp.300-319, 2007.

M. Hendriks, Model Checking the Time to Reach Agreement, pp.98-111
DOI : 10.1007/11603009_9

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.193-244, 1994.
DOI : 10.1109/LICS.1992.185551

URL : http://doi.org/10.1006/inco.1994.1045

T. Hérault and R. Lassaigne, Frédéric Magniette, and Sylvain Peyronnet Approximate probabilistic model checking, VMCAI, pp.73-84, 2004.

F. Herbreteau, D. Kini, B. Srivathsan, and I. Walukiewicz, Using non-convex approximations for efficient analysis of timed automata, FSTTCS, volume 13 of LIPIcs Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.78-89, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00559902

T. Hune, K. G. Larsen, and P. Pettersson, Guided synthesis of control programs using Uppaal, Nord. J. Comput, vol.8, issue.1, pp.43-64, 2001.

H. Ejersbo-jensen, K. G. Larsen, and A. Skou, Scaling up Uppaal automatic verification of real-time systems using compositionality and abstraction, Lecture Notes in Computer Science, pp.19-30, 1926.

K. Jensen and A. Podelski, Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the Joint European Conferences on Theory and Practice of Software, 10th International Conference Proceedings, volume 2988 of Lecture Notes in Computer Science, 2004.

J. Jakob-jessen, J. Illum-rasmussen, K. G. Larsen, and A. David, Guided Controller Synthesis for Climate Controller Using Uppaal Tiga, Lecture Notes in Computer Science, vol.4763, pp.227-240, 2007.
DOI : 10.1007/978-3-540-75454-1_17

R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics, vol.23, issue.1, pp.309-311, 1978.
DOI : 10.1016/0012-365X(78)90078-X

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM 2.0: a tool for probabilistic model checking, First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings., pp.322-323, 2004.
DOI : 10.1109/QEST.2004.1348048

L. Lamport, Real-Time Model Checking Is Really Simple, Lecture Notes in Computer Science, vol.3725, pp.162-175, 2005.
DOI : 10.1007/11560548_14

K. G. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune et al., As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata, Lecture Notes in Computer Science, vol.2102, pp.493-505, 2001.
DOI : 10.1007/3-540-44585-4_47

K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, Efficient verification of real-time systems: compact data structure and state-space reduction, Proceedings Real-Time Systems Symposium, pp.14-24, 1997.
DOI : 10.1109/REAL.1997.641265

K. G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, Testing realtime embedded software using Uppaal-TRON: an industrial case study, pp.299-306, 2005.

K. G. Larsen, J. Pearson, C. Weise, and W. Yi, Clock Difference Diagrams, BRICS Report Series, vol.5, issue.46, pp.271-298, 1999.
DOI : 10.7146/brics.v5i46.19491

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.1868

K. G. Larsen, P. Pettersson, and W. Yi, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.
DOI : 10.1007/s100090050010

G. Kim, J. Larsen, and . Rasmussen, Optimal conditional reachability for multi-priced timed automata, FoSSaCS, pp.234-249, 2005.

G. Kim, J. Larsen, and . Rasmussen, Optimal reachability for multi-priced timed automata, Theor. Comput. Sci, vol.390, issue.2-3, pp.197-213, 2008.

M. Lindahl, P. Pettersson, and W. Yi, Formal design and analysis of a gear controller, Lecture Notes in Computer Science, vol.1384, pp.281-297, 1998.
DOI : 10.1007/BFb0054178

Q. Lu, M. Madsen, M. Milata, S. Ravn, U. Fahrenberg et al., Reachability analysis for timed automata using max-plus algebra, The Journal of Logic and Algebraic Programming, vol.81, issue.3, pp.298-313, 2012.
DOI : 10.1016/j.jlap.2011.10.004

URL : https://hal.archives-ouvertes.fr/hal-01087998

O. Maler, Timed automata as an underlying model for planning and scheduling, AIPS Workshop on Planning for Temporal Domains, pp.67-70, 2002.

O. Maler, K. G. Larsen, and B. H. Krogh, On Zone-Based Analysis of Duration Probabilistic Automata, INFINITY, pp.33-46, 2010.
DOI : 10.4204/EPTCS.39.3

O. Maler, A. Pnueli, and J. Sifakis, On the synthesis of discrete controllers for timed systems (an extended abstract), STACS, pp.229-242, 1995.

P. Mcdermott-wells, What is Bluetooth? Potentials, IEEE, vol.23, issue.5, pp.33-35, 2004.

B. Jesper, J. Møller, H. R. Lichtenberg, H. Andersen, and . Hulgaard, Difference decision diagrams, Lecture Notes in Computer Science, vol.1683, pp.111-125, 1999.

J. Ouaknine and J. Worrell, Universality and Language Inclusion for Open and Closed Timed Automata, Lecture Notes in Computer Science, vol.2623, pp.375-388, 2003.
DOI : 10.1007/3-540-36580-X_28

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.5.1617

P. Panangaden, Labelled Markov Processes, 2010.
DOI : 10.1142/p595

K. Quaas, On the Interval-Bound Problem for Weighted Timed Automata, Lecture Notes in Computer Science, vol.6638, pp.452-464, 2011.
DOI : 10.1007/978-3-642-21254-3_36

J. Illum-rasmussen, K. G. Larsen, and K. Subramani, Resource-Optimal Scheduling Using Priced Timed Automata, pp.220-235
DOI : 10.1007/978-3-540-24730-2_19

K. Sen, M. Viswanathan, and G. Agha, Statistical Model Checking of Black-Box Probabilistic Systems, CAV, pp.202-215, 2004.
DOI : 10.1007/978-3-540-27813-9_16

C. Stirling, Modal and temporal logics for processes, Proc. Banff Higher Order Workshop, pp.149-237, 1995.
DOI : 10.1007/3-540-60915-6_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.9078

T. Teige, A. Eggers, and M. Fränzle, Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems, 2011.

S. Tripakis and K. Altisen, On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems, World Congress on Formal Methods, pp.233-252, 1999.
DOI : 10.1007/3-540-48119-2_15

F. W. Lodewijk, P. J. Van-hoesel, and . Havinga, A lightweight medium access protocol (LMAC) for wireless sensor networks: Reducing preamble transmissions and transceiver state switches, 1st International Workshop on Networked Sensing Systems Society of Instrument and Control Engineers (SICE), pp.205-208, 2004.

A. Wald, Sequential Analysis, 2004.

W. Yi, P. Pettersson, and M. Daniels, Automatic verification of realtime communicating systems by constraint-solving, of IFIP Conference Proceedings, pp.243-258

L. S. Håkan and . Younes, Verification and Planning for Stochastic Processes with Asynchronous Events, 2005.