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