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.
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:
Call the modified version of PRISM on a timed automaton given as argument.
Read the resulting split reachability graph.
Compute volume and distribution.
Output a stochastic Petri net encoding the reachability graph
annotated with distributions.
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.
