Model Checking Stochastic Automata

Bryans, J. and Bowman, H. and Derrick, J. (2003) Model Checking Stochastic Automata. ACM Transactions on Computational Logic, 4 (4). pp. 452-492. ISSN 1529-3785. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://www.cs.kent.ac.uk/pubs/2003/1730

Abstract

Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions; stochastic automata have emerged as a useful technique by which such systems can be specified and verified.However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this article we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.

Item Type: Article
Uncontrolled keywords: Stochastic Automata, Model Checking
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:00
Last Modified: 12 Jun 2012 14:03
Resource URI: http://kar.kent.ac.uk/id/eprint/13898 (The current URI for this page, for reference purposes)
  • Depositors only (login required):