Authors: Hichem Debbi; Aimad Debbi; Mustapha Bourahla
Addresses: Departement of Computer Science, University of M'sila, BP 166 Ichebilia, 28000 M'sila, Algeria ' Departement of Computer Science, University of M'sila, BP 166 Ichebilia, 28000 M'sila, Algeria ' Departement of Computer Science, University of M'sila, BP 166 Ichebilia, 28000 M'sila, Algeria
Abstract: The counterexample in probabilistic model checking (PMC) is a set of paths in which a path formula holds, and their accumulated probability violates the probability bound. However, understanding the counterexample is not an easy task. In this paper we address the complementary task of counterexample generation, which is the counterexample analysis. We propose an aided-diagnostic method for probabilistic counterexamples based on the notions of causality and regression analysis. Given a counterexample for a probabilistic CTL (PCTL)/continuous stochastic logic (CSL) formula that does not hold over probabilistic models [discrete time Markov chain (DTMC), Markov decision process (MDP) and continuous time Markov Chain (CTMC)], this method generates the causes of the violation, and describes their contribution to the error in the form of a regression model using structural equation modelling (SEM). The interpretation of the regression model generated helps the designer to get better insight on the behaviour of the model, and thus helps him to understand how the error has emerged.
Keywords: probabilistic model checking; PMC; probabilistic computation tree logic; PCTL; probabilistic counterexample; causality; structural equation modelling; SEM; regression analysis; debugging.
International Journal of Critical Computer-Based Systems, 2016 Vol.6 No.4, pp.250 - 274
Published online: 25 Jan 2017 *Full-text access for editors Access for subscribers Purchase this article Comment on this article