School of Computing

A model checking algorithm for stochastic systems

Jeremy Bryans, Howard Bowman, and John Derrick

Technical Report 4-00, University of Kent at Canterbury, Canterbury, Kent, January 2000.


In this report we present an algorithm for model checking stochastic automata. The algorithm, which is essentially based on discretising time, permits generalised distributions to be used.

Download publication 297 kbytes (PostScript)

Bibtex Record

author = {Jeremy Bryans and Howard Bowman and John Derrick},
title = {A Model Checking Algorithm for Stochastic Systems},
month = {January},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    address = {Canterbury, Kent},
    institution = {University of Kent at Canterbury},
    number = {4-00},
    publication_type = {techreport},
    submission_id = {626_954244857},

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

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

Last Updated: 21/03/2014