PRISM benchmark suite - Models. http://www.prismmodelchecker.org/benchmarks/models.php#mdps.
H. Aljazzar, F. Leitner-Fischer, S. Leue & D. Simeonov (2011):
DiPro - A Tool for Probabilistic Counterexample Generation.
In: Proceedings of the 18th International SPIN Workshop,
LNCS 6823.
Springer, Berlin, Heidelberg,
pp. 183–187,
doi:10.1007/978-3-642-22306-8_13.
H. Aljazzar & S. Leue (2009):
Generation of counterexamples for model checking of Markov decision processes.
In: Proceedings of the International Conference on Quantitative Evaluation of Systems (QEST),
pp. 197–206,
doi:10.1109/QEST.2009.10.
H. Aljazzar & S. Leue (2010):
Directed explicit state-space search in the generation of counterexamples for stochastic model checking.
IEEE Trans. on Software Engineering 36(1),
pp. 37–60,
doi:10.1109/TSE.2009.57.
Husain Aljazzar & Stefan Leue (2011):
K*: A heuristic search algorithm for finding the k shortest paths.
Artificial Intelligence 175(18),
pp. 2129 – 2154,
doi:10.1016/j.artint.2011.07.003.
A. Aziz, K. Sanwal, V. Singhal & R. Brayton (2000):
Model-checking continuous-time Markov chains.
ACM Transactions on Computational Logic 1(1),
pp. 162–170,
doi:10.1145/343369.343402.
C. Baier, B. Haverkort, H. Hermanns & J.-P Katoen (2003):
Model checking algorithms for continuous-time Markov chains.
IEEE Transactions on Software Engineering 29(7),
pp. 524–541,
doi:10.1109/TSE.2003.1205180.
T. Ball, M. Naik & S.K. Rajamani (2003):
From symptom to cause: Localizing errors in counterexample traces.
In: Proceedings of ACM Symposium on the Principles of Programming Languages,
pp. 97–105,
doi:10.1145/640128.604140.
A. Beer, S. Heidinger, U. Kuhne, F. Leitner-Fischer & S. Leue (2015):
Symbolic Causality Checking Using Bounded Model Checking.
In: Proceedings of SPIN 2015,
LNCS 9232.
Springer-Verlag, Berlin, Heidelberg,
pp. 203–221,
doi:10.1007/978-3-319-23404-5_14.
H. Chockler & J. Y. Halpern (2004):
Responsibility and blame: a structural model approach.
Journal of Artificial Intelligence Research (JAIR) 22(1),
pp. 93–115,
doi:10.1613/jair.1391.
H. Debbi (2014):
Diagnosis of Probabilistic Models using Causality and Regression.
In: Proceedings of the 8th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2014),
pp. 33–44.
H. Debbi & M. Bourahla (2013):
Causal Analysis of Probabilistic Counterexamples.
In: Proceedings of the Eleventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (Memocode),
pp. 77–86.
T. Eiter & T. Lukasiewicz (2002):
Complexity results for structure-based causality.
Artificial Intelligence 142(1),
pp. 53,
doi:10.1016/S0004-3702(02)00271-0.
T. Eiter & T. Lukasiewicz (2006):
Causes and explanations in the structural-model approach: Tractable cases.
Artificial Intelligence 170(6–7),
pp. 542–580,
doi:10.1016/j.artint.2005.12.003.
F. Fischer & S. Leue (2013):
Causality Checking for Complex System Models.
In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI),
LNCS 7737.
Springer, Berlin, Heidelberg,
pp. 248–276,
doi:10.1007/978-3-642-35873-9_16.
A. Groce (2004):
Error explanation with distance metrics.
In: Proceedings of Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS),
pp. 108–122,
doi:10.1007/s10009-005-0202-0.
J. Halpern & J. Pearl (2001):
Causes and explanations: A structural-model approach part I: Causes.
In: Proceedings of the 17th UAI,
pp. 194–202,
doi:10.1093/bjps/axi147.
T. Han & J.P. Katoen (2009):
Counterexamples Generation in probabilistic model checking.
IEEE Trans. on Software Engineering 35(2),
pp. 72–86,
doi:10.1109/TSE.2009.5.
H. Hansson & B. Jonsson (1994):
Logic for reasoning about time and reliability.
Formal aspects of Computing 6(5),
pp. 512–535,
doi:10.1007/BF01211866.
A. Hinton, M. Kwiatkowska, G. Norman & D. Parker (2006):
PRISM: A tool for automatic verification of probabilistic systems.
In: Proceedings of TACAS,
LNCS 3920.
Springer, Berlin, Heidelberg,
pp. 441–444,
doi:10.1007/11691372_29.
I.Beer, S. Ben-David, H. Chockler, A. Orni & R. Treer (2012):
Explaining counterexamples using causality.
Formal Methods Systems Design 40(1),
pp. 20–40,
doi:10.1007/s10703-011-0132-2.
N. Jansen, E. Abraham, M. Volk, R. Wilmer, J.P Katoen & B. Becker (2012):
Proceedings of The COMICS Tool - Computing Minimal Counterexamples for DTMCs.
In: Proceedings of ATVA,
LNCS 7561.
Springer, Berlin, Heidelberg,
pp. 249–253,
doi:10.1007/978-3-642-33386-6_27.
J.-P. Katoen, M. Khattri & I. S. Zapreev (2005):
A Markov Reward Model Checker.
In: Proceedings of QEST,
pp. 243–244,
doi:10.1109/QEST.2005.2.
F. Leitner-Fischer & S. Leue (2013):
On the Synergy of Probabilistic Causality Computation and Causality Checking.
In: Proceedings of SPIN 2013,
LNCS 7976.
Springer-Verlag, Berlin, Heidelberg,
pp. 246–263,
doi:10.1007/978-3-642-39176-7_16.
F. Leitner-Fischer & S. Leue (2013):
Probabilistic fault tree synthesis using causality computation.
International Journal of Critical Computer-Based Systems 4(2),
pp. 119–143,
doi:10.1504/IJCCBS.2013.056492.
R. Wimmer, N. Jansen, E. Abraham, B. Becker & J.P. Katoen (2012):
Minimal Critical Subsystems for Discrete-Time Markov Models.
In: Proceedings of TACAS,
LNCS 7214.
Springer, Berlin, Heidelberg,
pp. 299–314,
doi:10.1007/978-3-642-28756-5_21.
R. Wimmer, N. Jansen & A. Vorpahl (2013):
High-Level Counterexamples for Probabilistic Automata.
In: Proceedings of Quantitative Evaluation of Systems (QEST),
LNCS 8054.
Springer, Berlin, Heidelberg,
pp. 39–54,
doi:10.1007/978-3-642-40196-1_4.
eptcs@eptcs.org