Parallel CSRL Model Checking: First Results and Pointers to the Future

Matthias Kuntz

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

    Abstract

    The verification of quantitative aspects of a system, like performance and dependability, by means of model checking has become an important and vivid area of research over the past decade. Recently, great progress has been made in the combined analysis of a system's performance and dependability (the so-called performability) by means of model checking. Both the logic CSRL (continuous stochastic reward logic) and a number of model checking algorithms for this logic are tangible outcomes of this research. To evaluate CSRL properties, however, it is necessary to solve large systems of partial differential equations (PDEs). The inherent time complexity of the model checking algorithms makes CSRL model checking for system models with more than 100,000 states practically infeasible. To overcome these difficulties, we have investigated various possibilities to parallelise the CSRL model checking algorithms. First practical experiments with a parallel version of the so-called path-exploration-based algorithm will be reported.
    Original languageEnglish
    Title of host publicationProceedings of the Sixth International Workshop on Parallel and Distributed Methods in Verification
    EditorsI. Černá, B.R. Haverkort
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Pages105-120
    Number of pages16
    Publication statusPublished - Jul 2007
    Event6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007 - Berlin, Germany
    Duration: 8 Jul 20078 Jul 2007
    Conference number: 6
    http://anna.fi.muni.cz/PDMC/PDMC07/

    Workshop

    Workshop6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007
    Abbreviated titlePDMC
    Country/TerritoryGermany
    CityBerlin
    Period8/07/078/07/07
    Internet address

    Fingerprint

    Dive into the research topics of 'Parallel CSRL Model Checking: First Results and Pointers to the Future'. Together they form a unique fingerprint.

    Cite this