CiteULike is a free online bibliography manager. Register and you can start organising your references online.
Tags

Quantitative Timed Analysis of Interactive Markov Chains

by: Dennis Guck, Tingting Han, Joost-Pieter Katoen, MartinR Neuhäußer

edited by: AlwynE Goodloe, Suzette Person

In NASA Formal Methods, Vol. 7226 (2012), pp. 8-23, doi:10.1007/978-3-642-28891-3_4  Key: citeulike:12017153

Formatted Citation


Show HTML

Likes (beta)

This copy of the article hasn't been liked by anyone yet.

View FullText article


Abstract

This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed $1\frac12$ -player game in which delays are exponentially distributed. IMCs are compositional and act as semantic model for engineering formalisms such as AADL and dynamic fault trees. We provide algorithms for determining the extremal expected time of reaching a set of states, and the long-run average of time spent in a set of states. The prototypical tool Imca supports these algorithms as well as the synthesis of ε-optimal piecewise constant timed policies for timed reachability objectives. Two case studies show the feasibility and scalability of the algorithms.


pnpo's tags for this article

Citations (CiTO)

No CiTO relationships defined

X There are no reviews yet

X Find related articles with these CiteULike tags

X Posting History


X Export records

Privacy Statement | Terms & Conditions
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.