CSL model checking of deterministic and stochastic Petri nets

J.M. Martinez Verdugo, Boudewijn R.H.M. Haverkort

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

    22 Downloads (Pure)

    Abstract

    Deterministic and Stochastic Petri Nets (DSPNs) are a widely used high-level formalism for modeling discrete-event systems where events may occur either without consuming time, after a deterministic time, or after an exponentially distributed time. The underlying process dened by DSPNs, under certain restrictions, corresponds to a class of Markov Regenerative Stochastic Processes (MRGP). In this paper, we investigate the use of CSL (Continuous Stochastic Logic) to express probabilistic properties, such a time-bounded until and time-bounded next, at the DSPN level. The verification of such properties requires the solution of the steady-state and transient probabilities of the underlying MRGP. We also address a number of semantic issues regarding the application of CSL on MRGP and provide numerical model checking algorithms for this logic. A prototype model checker, based on SPNica, is also described.
    Original languageUndefined
    Title of host publicationProceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems
    EditorsR. German, A. Heindl
    Place of PublicationBerlin
    PublisherVDE Verlag
    Pages265-282
    Number of pages18
    ISBN (Print)978-3-8007-2945-6
    Publication statusPublished - 2006
    EventProceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems - Nuernberg, Germany
    Duration: 27 Mar 200629 Mar 2006

    Publication series

    Name
    PublisherSpringer Verlag
    NumberPaper PMD-

    Conference

    ConferenceProceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems
    Period27/03/0629/03/06
    OtherMarch 27-29, 2006

    Keywords

    • EWI-8992
    • METIS-237894
    • IR-66852

    Cite this