Model checking stochastic automata

J. Bryans, Howard Bowman, John Derrick

    Research output: Contribution to journalArticle

    21 Citations (Scopus)

    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.
    Original languageEnglish
    Pages (from-to)452-492
    Number of pages41
    JournalACM Transactions on Computational Logic
    Volume4
    Issue number4
    DOIs
    Publication statusPublished - 2003

    Fingerprint

    Model checking
    Probability distributions
    Distribution functions

    Cite this

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

    In: ACM Transactions on Computational Logic, Vol. 4, No. 4, 2003, p. 452-492.

    Research output: Contribution to journalArticle

    Bryans, J. ; Bowman, Howard ; Derrick, John. / Model checking stochastic automata. In: ACM Transactions on Computational Logic. 2003 ; Vol. 4, No. 4. pp. 452-492.
    @article{32d18f900cb9418685d3fd580d853933,
    title = "Model checking stochastic automata",
    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.",
    author = "J. Bryans and Howard Bowman and John Derrick",
    year = "2003",
    doi = "10.1145/937555.937558",
    language = "English",
    volume = "4",
    pages = "452--492",
    journal = "ACM Transactions on Computational Logic",
    issn = "1529-3785",
    publisher = "Association for Computing Machinery (ACM)",
    number = "4",

    }

    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 -