M. Agrawal, S. Akshay, B. Genest, and P. S. Thiagarajan, Approximate verification of the symbolic dynamics of Markov chains, LICS. IEEE Computer Society, pp.55-64, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00920793

R. Alur and D. 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

C. Baier, E. Clarke, V. Hartonas-garmhausen, M. Kwiatkowska, R. et al., Symbolic model checking for probabilistic processes, ICALP'97, pp.430-440, 1997.
DOI : 10.1007/3-540-63165-8_199

C. Baier, B. Haverkort, H. Hermanns, and J. And-katoen, Model checking meets performance evaluation, ACM SIGMETRICS Performance Evaluation Review, vol.32, issue.4, pp.10-15, 2005.
DOI : 10.1145/1059816.1059819

C. Baier, H. Hermanns, J. Katoen, and V. Wolf, Comparative branching-time semantics for Markov chains, CONCUR'03, pp.482-497, 2003.

C. Baier and J. Katoen, Principles of Model Checking, 2008.

D. Beauquier, A. Rabinovich, and A. Slissenko, A Logic of Probability with Decidable Model Checking, CSL'02, pp.306-321, 2002.
DOI : 10.1093/logcom/exl004

M. Benedikt, R. Lenhardt, and J. Worrell, LTL Model Checking of Interval Markov Chains, TACAS, pp.32-46, 2013.
DOI : 10.1007/978-3-642-36742-7_3

J. Büchi, On a Decision Method in Restricted Second Order Arithmetic, Int. Congress for Logic, pp.1-11, 1962.
DOI : 10.1007/978-1-4613-8928-6_23

B. Caillaud, B. Delahaye, K. G. Larsen, A. Legay, M. L. Pedersen et al., Constraint Markov Chains, Theoretical Computer Science, vol.412, issue.34, pp.4373-4404, 2011.
DOI : 10.1016/j.tcs.2011.05.010
URL : https://hal.archives-ouvertes.fr/hal-00654003

H. Calbrix, M. Nivat, and A. Podelski, Ultimately periodic words of rational omega-languages, Int. Conf. on Mathematical Foundations of Programming Semantics, pp.554-566, 1994.

R. Chadha, V. Korthikanti, M. Vishwanathan, G. Agha, and Y. Kwon, Model Checking MDPs with a Unique Compact Invariant Set of Distributions, 2011 Eighth International Conference on Quantitative Evaluation of SysTems, 2011.
DOI : 10.1109/QEST.2011.22

K. Chatterjee, K. Sen, and T. A. Henzinger, Model-checking omega-regular properties of interval Markov chains, FoSSaCS, pp.302-317, 2008.

R. Dedekind, Theory of Algebraic Integers. Cambridge Mathematical Library, 1996.

B. Delahaye, K. G. Larsen, A. Legay, M. L. Pedersen, and A. Wasowski, Decision Problems for Interval Markov Chains, LATA, pp.274-285, 2011.
DOI : 10.1007/978-3-642-21254-3_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.374.9911

V. Forejt, M. Z. Kwiatkowska, G. Norman, P. , and D. , Automated Verification Techniques for Probabilistic Systems, SFM'11, pp.53-113, 2011.
DOI : 10.1007/978-3-642-21455-4_3
URL : https://hal.archives-ouvertes.fr/hal-00648037

S. Haddad and N. Pekergin, Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains, 2009 Sixth International Conference on the Quantitative Evaluation of Systems, pp.177-186, 2009.
DOI : 10.1109/QEST.2009.42
URL : https://hal.archives-ouvertes.fr/hal-00772668

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994.
DOI : 10.1007/BF01211866

G. Hardy and E. Wright, An introduction to the Theory of Numbers 1996. The theory of hybrid automata, LICS. IEEE Computer Society, pp.278-292, 1960.

M. Huth and M. Z. Kwiatkowska, Quantitative analysis and model checking, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.111-122, 1997.
DOI : 10.1109/LICS.1997.614940
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1584

B. Jonsson and K. G. Larsen, Specification and refinement of probabilistic processes, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.266-277, 1991.
DOI : 10.1109/LICS.1991.151651

J. G. Kemeny and J. L. Snell, Finite Markov chains, 1960.

V. A. Korthikanti, M. Viswanathan, G. Agha, and Y. Kwon, Reasoning about MDPs as Transformers of Probability Distributions, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp.199-208, 2010.
DOI : 10.1109/QEST.2010.35

I. O. Kozine, Interval-valued Markov chains, Reliable Computing, vol.8, issue.2, pp.97-113, 2002.
DOI : 10.1023/A:1014745904458

M. Z. Kwiatkowska, G. Norman, P. , and D. , PRISM 4.0: Verification of Probabilistic Real-Time Systems, In CAV. Lecture Notes in Computer Science Series, vol.1, issue.1-2, pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

Y. Kwon and G. Agha, Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains, In ICFEM. Lecture Notes in Computer Science Series, vol.3308, pp.194-208, 2004.
DOI : 10.1007/978-3-540-30482-1_21

Y. Kwon and G. Agha, Verifying the Evolution of Probability Distributions Governed by a DTMC, IEEE Transactions on Software Engineering, vol.37, issue.1, pp.126-141, 2011.
DOI : 10.1109/TSE.2010.80

S. Lalley, Course notes: Basic Markov chain theory. website: http://galton.uchicago, p.312, 2010.

S. Lang, Algebraic Number Theory (Graduate Texts in Mathematics), 1994.

D. Lind and B. Marcus, An Introduction to Symbolic Dynamics and Coding, 1995.
DOI : 10.1017/CBO9780511626302

P. V. Mieghem, Performance Analysis of Communications Networks and Systems, 2006.
DOI : 10.1017/CBO9780511616488

M. Morse and G. A. Hedlund, Symbolic Dynamics, American Journal of Mathematics, vol.60, issue.4, pp.815-866, 1938.
DOI : 10.2307/2371264

J. R. Norris, Markov chains. Cambridge series on statistical and probabilistic mathematics Series, 1997.

J. Ouaknine and J. Worrell, Decision problems for linear recurrence sequences, RP, pp.21-28, 2012.

H. Schneider, Wielandt's proof of the exponent inequality for primitive nonnegative matrices, Linear Algebra and its Applications, vol.353, issue.1-3, pp.5-10, 2002.
DOI : 10.1016/S0024-3795(02)00414-7

E. Seneta, Non-negative Matrices and Markov Chains. Springer series in Statistics, 1981.
DOI : 10.1007/0-387-32792-4

D. Skulj, Discrete time Markov chains with interval probabilities, International Journal of Approximate Reasoning, vol.50, issue.8, pp.1314-1329, 2009.
DOI : 10.1016/j.ijar.2009.06.007

A. Tarski, A Decision Method for Elementary Algebra and Geometry. Univ. of California Press. Turakainen, P. 1968, On Stochastic Languagaes. Information and Control, vol.12, pp.304-313, 1951.

M. Y. Vardi, Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach, ARTS. Lecture Notes in Computer Science Series, pp.265-276, 1999.
DOI : 10.1007/3-540-48778-6_16

K. Weichselberger, The theory of interval-probability as a unifying concept for uncertainty, International Journal of Approximate Reasoning, vol.24, issue.2-3, pp.2-3, 2000.
DOI : 10.1016/S0888-613X(00)00032-3

V. Wolf, R. Goel, M. Mateescu, and T. H. , Solving the chemical master equation using sliding windows, BMC Systems Biology, vol.4, issue.1, p.42, 2010.
DOI : 10.1186/1752-0509-4-42