Efficient Modelling, Generation and Analysis of Markov Automata

Mark Timmer, K. Iwama (Editor)

    Research output: Contribution to journalArticleAcademic

    76 Downloads (Pure)


    Quantitative model checking is concerned with the verification of both quantitative and qualitative properties over models incorporating quantitative information. Increases in expressivity of the models involved allow more types of systems to be analysed, but also raise the difficulty of their efficient analysis. Three years ago, the Markov automaton (MA) was introduced as a generalisation of probabilistic automata and interactive Markov chains, supporting nondeterminism, discrete probabilistic choice as well as stochastic timing (Markovian rates). Later, the tool IMCA was developed to compute time-bounded reachability probabilities, expected times and long-run averages for sets of goal states within an MA. However, an efficient formalism for modelling and generating MAs was still lacking. Additionally, the omnipresent state space explosion also threatened the analysability of these models. This thesis solves the first problem and contributes significantly to the solution of the second.
    Original languageUndefined
    Pages (from-to)139-140
    Number of pages2
    JournalBulletin of the European Association for Theoretical Computer Science
    Publication statusPublished - Feb 2014


    • EWI-24602
    • IR-90553
    • METIS-304036

    Cite this