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

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.208.4027

E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260

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.1109/TSE.1986.6313045
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.6154

M. E. Andrés, P. D-'argenio, and P. Van-rossum, Significant Diagnostic Counterexamples in Probabilistic Model Checking, Haifa Verification Conference, pp.129-148, 2008.
DOI : 10.1007/978-3-540-24611-4_1

T. Han, J. P. Katoen, and B. Damman, Counterexample generation in probabilistic model checking, IEEE Trans. on Software Engineering, vol.35, issue.2, pp.241-257, 2009.

R. Wimmer, B. Braitling, and B. Becker, Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking, Proc. of VMCAI, pp.366-380, 2009.
DOI : 10.1007/978-3-540-93900-9_29

H. Aljazzar and S. Leue, Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking, IEEE Transactions on Software Engineering, vol.36, issue.1, pp.37-60, 2010.
DOI : 10.1109/TSE.2009.57

´. Abrahám, E. Jansen, N. Wimmer, R. Katoen, J. P. Becker et al., DTMC Model Checking by SCC Reduction, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp.37-46, 2010.
DOI : 10.1109/QEST.2010.13

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828

T. Han and J. P. Katoen, Counterexamples in Probabilistic Model Checking, Proc. of TACAS, pp.72-86, 2007.
DOI : 10.1007/978-3-540-71209-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.320.3197

J. P. Katoen, T. Kemna, I. Zapreev, and D. N. Jansen, Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking, Proc. of TACAS, pp.87-101, 2007.
DOI : 10.1007/978-3-540-71209-1_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.93.3016

S. Derisavi, Signature-based Symbolic Algorithm for Optimal Markov Chain Lumping, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), pp.141-150, 2007.
DOI : 10.1109/QEST.2007.27

R. Wimmer, S. Derisavi, and H. Hermanns, Symbolic partition refinement with automatic balancing of time and space, Performance Evaluation, vol.67, issue.9, pp.815-835, 2010.
DOI : 10.1016/j.peva.2009.12.008

G. S. Tseitin, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic Part, pp.115-125, 1970.

B. Dutertre and L. M. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), Proc. of CAV, pp.81-94, 2006.
DOI : 10.1007/11817963_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.92.705

S. Even, O. Goldreich, and A. Lempel, A randomized protocol for signing contracts, Communications of the ACM, vol.28, issue.6, pp.637-647, 1985.
DOI : 10.1145/3812.3818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.7448

G. Norman and V. Shmatikov, Analysis of Probabilistic Contract Signing, Journal of Computer Security, vol.14, issue.6, pp.561-589, 2006.
DOI : 10.1007/978-3-540-40981-6_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.1816

M. Reiter and A. Rubin, Crowds: anonymity for Web transactions, ACM Transactions on Information and System Security, vol.1, issue.1, pp.66-92, 1998.
DOI : 10.1145/290163.290168
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.864

A. Itai and M. Rodeh, Symmetry breaking in distributed networks, Information and Computation, vol.88, issue.1, pp.60-87, 1990.
DOI : 10.1016/0890-5401(90)90004-2
URL : http://doi.org/10.1016/0890-5401(90)90004-2

Z. Collin and S. Dolev, Self-stabilizing depth-first search, Information Processing Letters, vol.49, issue.6, pp.297-301, 1994.
DOI : 10.1016/0020-0190(94)90103-1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.1100

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, Proc. of TACAS, pp.441-444, 2006.
DOI : 10.1007/11691372_29

M. Günther, J. Schuster, and M. Siegle, Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA, Proceedings of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant Systems, DYADEM-FTS '10, pp.13-18, 2010.
DOI : 10.1145/1772630.1772635