Uniform sampling for Timed Automata

Monte Carlo model checking introduced by Smolka and Grosu is an approach to analyse non-probabilistic models using sampling and draw conclusions with a given confidence interval by applying statistical inference. Though not exhaustive, the method enables verification of complex models, even in cases where the underlying problem is undecidable. This tool chain provides Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, as opposed to isotropic sampling that chooses the next step uniformly at random. The uniformity is defined with respect to volume measure of timed languages. We have developed uniform sampling within a zone-based Monte Carlo model checking framework. We implement our algorithms using tools Prism, SageMath and Cosmos.

This complete work is described in [BBBK16].

Tool-Chain



We implemented the techniques using three tools: PRISM, SageMath and Cosmos. The workflow is depicted in the figure above. We modify the tools to meet our needs. We adapted PRISM's forward reachability algorithm to implement the splitting algorithm described in [BBBK16]. We also export the split zone graph in a file format easy to read for SageMath. We use SageMath to compute distributions and weights of transitions as rational functions of clock valuations, which are exported and read by COSMOS in the form of a Stochastic Petri Net with general distributions. COSMOS then samples trajectories of this model, checks the membership of the language of a given NTA, and returns the probability. We have modified COSMOS to handle distributions given by arbitrary rational functions and to compute the membership of a timed word in an NTA.

All the tools that we used are open source software under the GPL licence.

PRISM

PRISM is a probabilistic model checker that supports a variety of probabilistic models and probabilistic temporal logics, including Probabilistic Timed Automata (PTA). A PTA model is provided in the PRISM modelling language as a synchronised parallel composition of reactive modules.

The modified version PRISM implementing the splitting algorithm on the zone graph is a fork of PRISM 4.1.dev with an additional switch "-exportsplitreach file.sage" exporting the split reachability graph in a format readable by sage. This fork is available for download here.

SageMath

SageMath is a mathematics software system. We use it to manipulate symbolic polynomials for the volume functions and probability distribution.

Sage is a scripting language derived from python. The script we have developed is available here. This script does the following:

To use this script one must first edit the 10th line to set the variable prismpath to the path of the modified prism executable. The path of the input timed automaton is given as first argument, then the output file name, then the receding horizon value and finally the length of word to sample.

Case Study and examples

File ex.prism contains an example TA with a single state and two transitions. To sample paths of length 100 uniformly with receding horizon 10 from this example we use the command
./script_tocosmos.sage ex.prism ex.grml 10 100.
This command produce a file ex.grml containing a stochastic Petri net and a file twoears.grml.data containing the polynomials defining probability distributions. The command
Cosmos ex.grml --loop 100 -i
simulate the trajectory step by step.

We provide here a script that generates and run experiments on the case study described in [BBBK16]. This script is written in the Ocaml language.