### Abstract

Original language | English |
---|---|

Pages (from-to) | 452-492 |

Number of pages | 41 |

Journal | ACM Transactions on Computational Logic |

Volume | 4 |

Issue number | 4 |

DOIs | |

Publication status | Published - 2003 |

### Fingerprint

### Cite this

*ACM Transactions on Computational Logic*,

*4*(4), 452-492. https://doi.org/10.1145/937555.937558

**Model checking stochastic automata.** / Bryans, J.; Bowman, Howard; Derrick, John.

Research output: Contribution to journal › Article

*ACM Transactions on Computational Logic*, vol. 4, no. 4, pp. 452-492. https://doi.org/10.1145/937555.937558

}

TY - JOUR

T1 - Model checking stochastic automata

AU - Bryans, J.

AU - Bowman, Howard

AU - Derrick, John

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

U2 - 10.1145/937555.937558

DO - 10.1145/937555.937558

M3 - Article

VL - 4

SP - 452

EP - 492

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 4

ER -