Title: Debugging of probabilistic systems using structural equation modelling

 

Author: 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

 

Journal: Int. J. of Critical Computer-Based Systems, 2016 Vol.6, No.4, pp.250 - 274

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2016.081805

 

Available online 25 Jan 2017

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article