Int. J. of Critical Computer-Based Systems   »   2016 Vol.6, No.4

 

 

Title: Debugging of probabilistic systems using structural equation modelling

 

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.

 

DOI: 10.1504/IJCCBS.2016.081805

 

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

 

Available online: 25 Jan 2017

 

 

Editors Full text accessPurchase this articleComment on this article