Skip to main content

A Manual for a ModelChecker for Stochastic Automata

Akehurst, David H. and Bowman, Howard and Bryans, Jeremy W. and Derrick, John (2000) A Manual for a ModelChecker for Stochastic Automata. Technical report. n/a (KAR id:21927)

Abstract

This technical report describes a modelchecker for Stochastic Automata, which was built based on the theory described in [BBD00]. The tool is available from: http://www.cs.ukc.ac.uk/people/staff/dha/index.html 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.

Item Type: Reports and Papers (Technical report)
Additional information: Technical Report 9-00
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 27 Oct 2009 14:57 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21927 (The current URI for this page, for reference purposes)

University of Kent Author Information

Akehurst, David H..

Creator's ORCID:
CReDIT Contributor Roles:

Bowman, Howard.

Creator's ORCID: https://orcid.org/0000-0003-4736-1869
CReDIT Contributor Roles:

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.