Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    60 Downloads (Pure)

    Abstract

    The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.
    Original languageUndefined
    Title of host publicationProceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation
    EditorsIvana Černá, Gerald Lüttgen
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages35-50
    Number of pages16
    DOIs
    Publication statusPublished - 3 Dec 2008
    Event7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008 - Budapest, Hungary
    Duration: 29 Mar 200829 Mar 2008
    Conference number: 7
    http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Number2
    Volume220
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Workshop

    Workshop7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008
    Abbreviated titlePDMC
    CountryHungary
    CityBudapest
    Period29/03/0829/03/08
    Internet address

    Keywords

    • FMT-TOOLS
    • FMT-MC: MODEL CHECKING
    • METIS-254871
    • EC Grant Agreement nr.: FP6/043235
    • EWI-12290
    • IR-62249

    Cite this

    Blom, S., Haverkort, B. R. H. M., Kuntz, G. W. M., & van de Pol, J. C. (2008). Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking. In I. Černá, & G. Lüttgen (Eds.), Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (pp. 35-50). [10.1016/j.entcs.2008.11.012] (Electronic Notes in Theoretical Computer Science; Vol. 220, No. 2). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2008.11.012
    Blom, Stefan ; Haverkort, Boudewijn R.H.M. ; Kuntz, G.W.M. ; van de Pol, Jan Cornelis. / Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking. Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation. editor / Ivana Černá ; Gerald Lüttgen. Amsterdam : Elsevier, 2008. pp. 35-50 (Electronic Notes in Theoretical Computer Science; 2).
    @inproceedings{710e087bfd614ee98b177649c4af873b,
    title = "Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking",
    abstract = "The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.",
    keywords = "FMT-TOOLS, FMT-MC: MODEL CHECKING, METIS-254871, EC Grant Agreement nr.: FP6/043235, EWI-12290, IR-62249",
    author = "Stefan Blom and Haverkort, {Boudewijn R.H.M.} and G.W.M. Kuntz and {van de Pol}, {Jan Cornelis}",
    note = "Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)",
    year = "2008",
    month = "12",
    day = "3",
    doi = "10.1016/j.entcs.2008.11.012",
    language = "Undefined",
    series = "Electronic Notes in Theoretical Computer Science",
    publisher = "Elsevier",
    number = "2",
    pages = "35--50",
    editor = "Ivana Čern{\'a} and Gerald L{\"u}ttgen",
    booktitle = "Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation",

    }

    Blom, S, Haverkort, BRHM, Kuntz, GWM & van de Pol, JC 2008, Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking. in I Černá & G Lüttgen (eds), Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation., 10.1016/j.entcs.2008.11.012, Electronic Notes in Theoretical Computer Science, no. 2, vol. 220, Elsevier, Amsterdam, pp. 35-50, 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008, Budapest, Hungary, 29/03/08. https://doi.org/10.1016/j.entcs.2008.11.012

    Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking. / Blom, Stefan; Haverkort, Boudewijn R.H.M.; Kuntz, G.W.M.; van de Pol, Jan Cornelis.

    Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation. ed. / Ivana Černá; Gerald Lüttgen. Amsterdam : Elsevier, 2008. p. 35-50 10.1016/j.entcs.2008.11.012 (Electronic Notes in Theoretical Computer Science; Vol. 220, No. 2).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking

    AU - Blom, Stefan

    AU - Haverkort, Boudewijn R.H.M.

    AU - Kuntz, G.W.M.

    AU - van de Pol, Jan Cornelis

    N1 - Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)

    PY - 2008/12/3

    Y1 - 2008/12/3

    N2 - The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.

    AB - The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.

    KW - FMT-TOOLS

    KW - FMT-MC: MODEL CHECKING

    KW - METIS-254871

    KW - EC Grant Agreement nr.: FP6/043235

    KW - EWI-12290

    KW - IR-62249

    U2 - 10.1016/j.entcs.2008.11.012

    DO - 10.1016/j.entcs.2008.11.012

    M3 - Conference contribution

    T3 - Electronic Notes in Theoretical Computer Science

    SP - 35

    EP - 50

    BT - Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation

    A2 - Černá, Ivana

    A2 - Lüttgen, Gerald

    PB - Elsevier

    CY - Amsterdam

    ER -

    Blom S, Haverkort BRHM, Kuntz GWM, van de Pol JC. Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking. In Černá I, Lüttgen G, editors, Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation. Amsterdam: Elsevier. 2008. p. 35-50. 10.1016/j.entcs.2008.11.012. (Electronic Notes in Theoretical Computer Science; 2). https://doi.org/10.1016/j.entcs.2008.11.012