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 and P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing , STOC '04, pp.202-211, 2004.
DOI : 10.1145/1007352.1007390

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

S. Andova, Process Algebra with Probabilistic Choice, ARTS, pp.111-129, 1999.
DOI : 10.1007/3-540-48778-6_7

C. Baier, F. Ciesinski, and M. Größer, ProbMela and verification of Markov decision processes, ACM SIGMETRICS Performance Evaluation Review, vol.32, issue.4, pp.22-27, 2005.
DOI : 10.1145/1059816.1059821

A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone et al., Multiple Viewpoint Contract-Based Specification and Design, FMCO'07, pp.200-225, 2008.
DOI : 10.1109/43.736561

J. R. Büchi, Weak Second-Order Arithmetic and Finite Automata, Zeitschrift f??r Mathematische Logik und Grundlagen der Mathematik, vol.9, issue.1-6, pp.66-92, 1960.
DOI : 10.1002/malq.19600060105

K. Chatterjee, L. De-alfaro, M. Faella, T. A. Henzinger, R. Majumdar et al., Compositional quantitative reasoning, QEST, pp.179-188, 2006.

F. Ciesinski and C. Baier, Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems, In QEST, pp.131-132, 2006.

F. Ciesinski and M. Größer, On Probabilistic Computation Tree Logic, Validation of Stochastic Systems, pp.147-188, 2004.
DOI : 10.1007/978-3-540-24611-4_5

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs, pp.52-71, 1981.
DOI : 10.1007/BFb0025774

L. De-alfaro, Formal Verification of Probabilistic Systems, 1997.

L. De-alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, Model checking discounted temporal properties, TACAS, volume 2988 of Lecture Notes in Computer Science, pp.77-92, 2004.

B. Delahaye, B. Caillaud, and A. Legay, Compositional reasoning on (probabilistic) contracts (long version)

C. Eisner and D. Fisman, A Practical Introduction to PSL, 2006.

A. Finkel, B. Willems, and P. Wolper, A direct symbolic approach to model checking pushdown systems, Electr. Notes Theor. Comput. Sci, vol.9, 1997.

Y. Glouche, P. L. Guernic, J. Talpin, and T. Gautier, A boolean algebra of contracts for logical assume-guarantee reasoning, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00292870

A. Høyland and M. Rausand, System Reliability Theory: Models and Statistical Methods, 1994.

N. López and M. Núñez, An Overview of Probabilistic Process Algebras and Their Equivalences, Validation of Stochastic Systems, pp.89-123, 2004.
DOI : 10.1007/978-3-540-24611-4_3

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

M. Rabin and D. Scott, Finite Automata and Their Decision Problems, IBM Journal of Research and Development, vol.3, issue.2, pp.115-125, 1959.
DOI : 10.1147/rd.32.0114

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

R. Sinnamon and J. Andrews, Fault tree analysis and binary decision diagrams, Proceedings of 1996 Annual Reliability and Maintainability Symposium, pp.215-222, 1996.
DOI : 10.1109/RAMS.1996.500665

M. Y. Vardi, Automatic verification of probabilistic concurrent finite state programs, 26th Annual Symposium on Foundations of Computer Science (sfcs 1985), pp.327-338, 1985.
DOI : 10.1109/SFCS.1985.12

M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification (preliminary report), LICS, pp.332-344, 1986.

M. Y. Vardi and P. Wolper, Reasoning about Infinite Computations, Information and Computation, vol.115, issue.1, pp.1-37, 1994.
DOI : 10.1006/inco.1994.1092

P. Wolper, Temporal logic can be more expressive, 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pp.72-99, 1983.
DOI : 10.1109/SFCS.1981.44