Efficient Modelling and Generation of Markov Automata (extended version)

    Research output: Book/ReportReportAcademic

    21 Downloads (Pure)

    Abstract

    This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models. Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL's linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages35
    Publication statusPublished - 11 Jun 2012

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-12-16
    ISSN (Print)1381-3625

    Keywords

    • IR-80536
    • METIS-287881
    • EWI-21932

    Cite this

    Timmer, M., Katoen, J. P., van de Pol, J. C., & Stoelinga, M. I. A. (2012). Efficient Modelling and Generation of Markov Automata (extended version). (CTIT Technical Report Series; No. TR-CTIT-12-16). Enschede: Centre for Telematics and Information Technology (CTIT).
    Timmer, Mark ; Katoen, Joost P. ; van de Pol, Jan Cornelis ; Stoelinga, Mariëlle Ida Antoinette. / Efficient Modelling and Generation of Markov Automata (extended version). Enschede : Centre for Telematics and Information Technology (CTIT), 2012. 35 p. (CTIT Technical Report Series; TR-CTIT-12-16).
    @book{1b3a69cbc9c44de8aa11f08a041cde9e,
    title = "Efficient Modelling and Generation of Markov Automata (extended version)",
    abstract = "This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models. Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL's linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.",
    keywords = "IR-80536, METIS-287881, EWI-21932",
    author = "Mark Timmer and Katoen, {Joost P.} and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
    year = "2012",
    month = "6",
    day = "11",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-12-16",
    address = "Netherlands",

    }

    Timmer, M, Katoen, JP, van de Pol, JC & Stoelinga, MIA 2012, Efficient Modelling and Generation of Markov Automata (extended version). CTIT Technical Report Series, no. TR-CTIT-12-16, Centre for Telematics and Information Technology (CTIT), Enschede.

    Efficient Modelling and Generation of Markov Automata (extended version). / Timmer, Mark; Katoen, Joost P.; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2012. 35 p. (CTIT Technical Report Series; No. TR-CTIT-12-16).

    Research output: Book/ReportReportAcademic

    TY - BOOK

    T1 - Efficient Modelling and Generation of Markov Automata (extended version)

    AU - Timmer, Mark

    AU - Katoen, Joost P.

    AU - van de Pol, Jan Cornelis

    AU - Stoelinga, Mariëlle Ida Antoinette

    PY - 2012/6/11

    Y1 - 2012/6/11

    N2 - This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models. Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL's linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.

    AB - This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models. Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL's linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.

    KW - IR-80536

    KW - METIS-287881

    KW - EWI-21932

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Efficient Modelling and Generation of Markov Automata (extended version)

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Timmer M, Katoen JP, van de Pol JC, Stoelinga MIA. Efficient Modelling and Generation of Markov Automata (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2012. 35 p. (CTIT Technical Report Series; TR-CTIT-12-16).