Automated generation of partial Markov chain from high level descriptions

• We generate Markov chains from a higher level safety modeling language (AltaRica).
• We use a variation on Dijkstra׳s algorithm to generate partial Markov chains.
• Hence we solve two problems: the first problem is the tedious manual construction of Markov chains.
• The second problem is the blow-up of the size of the chains, at the cost of decent approximations.
• The experimental results highlight the efficiency of the method.

We propose an algorithm to generate partial Markov chains from high level implicit descriptions, namely AltaRica models. This algorithm relies on two components. First, a variation on Dijkstra׳s algorithm to compute shortest paths in a graph. Second, the definition of a notion of distance to select which states must be kept and which can be safely discarded.The proposed method solves two problems at once. First, it avoids a manual construction of Markov chains, which is both tedious and error prone. Second, up the price of acceptable approximations, it makes it possible to push back dramatically the exponential blow-up of the size of the resulting chains.We report experimental results that show the efficiency of the proposed approach.