SPDL Model Checking via Property-Driven State Space Generation

    Research output: Book/ReportReportProfessional

    25 Downloads (Pure)

    Abstract

    In this report 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 languageUndefined
    Place of PublicationEnschede
    PublisherDesign and Analysis of Communication Systems (DACS)
    Number of pages27
    Publication statusPublished - Sep 2007

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.LNCS4549/TR-CTIT-07-59
    ISSN (Print)1381-3625

    Keywords

    • METIS-241884
    • EWI-11009
    • IR-64331

    Cite this

    Kuntz, G. W. M., & Haverkort, B. R. H. M. (2007). SPDL Model Checking via Property-Driven State Space Generation. (CTIT Technical Report Series; No. LNCS4549/TR-CTIT-07-59). Enschede: Design and Analysis of Communication Systems (DACS).