Consistency and refinement for Interval Markov Chains

Abate, 2008, Markov set-chains as abstractions of stochastic hybrid sytems, vol. 4981 Andova, 1999, Process algebra with probabilistic choice, 111 Antonik, 2010, Modal and mixed specifications: key decision problems and their complexities, MSCS, 20, 75 A. Antonik, M. Huth, K.G. Larsen, U. Nyman, A. Wa¸sowski, 20 years of modal and mixed specifications, BEATCS 95, 2008. Available from: <http://processalgebra.blogspot.com/2008/05/concurrency-column-for-beatcs-june-2008.html>. Benes, 2009, Checking thorough refinement on modal transition systems is EXPTIME-complete, ICTAC, 112 Caillaud, 2010, Compositional design methodology with constraint markov chains Chatterjee, 2008, Model-checking omega-regular properties of interval Markov chains, vol. 4962, 302 Clarke, 1994, Model checking and abstraction, ACM Trans. Program. Lang. Systems, 16, 1512, 10.1145/186025.186051 Clarke, 2000, Counterexample-guided abstraction refinement, vol. 1855, 154 Clarke, 2003, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 752, 10.1145/876638.876643 D. Dams, Abstract interpretation and partition refinement for model checking, Ph.D. Thesis, Eindhoven University of Technology, July 1996. B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wa¸sowski, New results for constraint markov chains, PEVA, 2011, in press. Fecher, 2006, Don’t know in probabilistic systems, vol. 3925, 71 Haddad, 2009, Using stochastic comparison for efficient model checking of uncertain Markov chains, 177 Hansson, 1994, A logic for reasoning about time and reliability, Formal Asp. Comput., 6, 512, 10.1007/BF01211866 Hartfield, 1998, Markov Set-Chains, vol. 1695 M.R. Henzinger, T.A. Henzinger, P.W. Kopke, Computing simulations on finite and infinite graphs, in: Proc. FOCS’95, 1995, pp. 453–462. Jonsson, 1991, Specification and refinement of probabilistic processes, 266 Jonsson, 2001, Probabilistic extensions of process algebras, 685 Katoen, 2007, Three-valued abstraction for continuous-time Markov chains, vol. 4590, 311 Katoen, 2009, Compositional abstraction for stochastic systems, vol. 5813, 195 K.G. Larsen, Modal specifications, in: AVMS, LNCS, vol. 407, 1989, pp. 232–246. Larsen, 1988, A modal process logic, 203 López, 2004, An overview of probabilistic process algebras and their equivalences, vol. 2925, 89 Rabin, 1963, Probabilistic automata, Inform. and Control, 6, 230, 10.1016/S0019-9958(63)90290-0 Segala, 1994, Probabilistic simulations for probabilistic processes, vol. 836, 481 Sen, 2006, Model-checking Markov chains in the presence of uncertainties, vol. 3920, 394