Faster SPDL Model Checking Through Property-Driven State Space Generation

Matthias Kuntz, Boudewijn R. Haverkort

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

    14 Downloads (Pure)

    Abstract

    In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.
    Original languageEnglish
    Title of host publicationFormal Methods and Stochastic Models for Performance Evaluation
    Subtitle of host publicationFourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings
    EditorsKatinka Wolter
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages80-96
    Number of pages17
    ISBN (Print)978-3-540-75210-3
    DOIs
    Publication statusPublished - 14 Sep 2007
    Event4th European Performance Engineering Workshop, EPEW 2007 - Berlin, Germany
    Duration: 27 Sep 200728 Sep 2007
    Conference number: 4

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume4748
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    Workshop4th European Performance Engineering Workshop, EPEW 2007
    Abbreviated titleEPEW
    CountryGermany
    CityBerlin
    Period27/09/0728/09/07

    Keywords

    • Model check
    • Parse tree
    • Kanban system
    • State space generation
    • Propositional dynamic logic

    Fingerprint Dive into the research topics of 'Faster SPDL Model Checking Through Property-Driven State Space Generation'. Together they form a unique fingerprint.

  • Cite this

    Kuntz, M., & Haverkort, B. R. (2007). Faster SPDL Model Checking Through Property-Driven State Space Generation. In K. Wolter (Ed.), Formal Methods and Stochastic Models for Performance Evaluation: Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September 27-28, 2007. Proceedings (pp. 80-96). (Lecture Notes in Computer Science; Vol. 4748). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-540-75211-0_7