School of Computing

A Manual for a ModelChecker for Stochastic Automata

David Akehurst, Howard Bowman, Jeremy Bryans, and John Derrick

Technical Report 9-00, Computing Laboratory, University of Kent, December 2000.


This technical report describes a modelchecker for Stochastic Automata, which was built based on the theory described in [BBD00].

The tool is available from:

It accepts a stochastic automaton, a 'timed probabilistic until' formula pattern and a time step parameter. Note that we do not yet allow adversaries, a clock which guards two or more transitions is considered a (run-time) error. Also, we have not yet implemented the full range of the temporal logic in [BBD00]; only the 'timed probabilistic until' queries are allowed, and propositions must be atomic. The algorithm will return one of three results: true, false or undecided. If it returns true, then the automaton models the formula. If it returns false, then the automaton does not model the formula. If it returns undecided, then the algorithm was unable to determine whether the automaton models the formula.

Download publication 128 kbytes (PDF)

Bibtex Record

author = {David Akehurst and Howard Bowman and Jeremy Bryans and John Derrick},
title = {{A Manual for a ModelChecker for Stochastic Automata}},
month = {December},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    publication_type = {techreport},
    submission_id = {10906_985944658},
    institution = {Computing Laboratory, University of Kent},
    number = {9-00},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014