An incremental modular technique for checking LTL-X properties on Petri nets

K. Klai, L. Petrucci, M.A. Reniers

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

    2 Citations (Scopus)
    50 Downloads (Pure)


    Model-checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. Modular verification is a promising natural approach to tackle this problem. It is based on the "divide and conquer" principle and aims at deducing the properties of the system from those of its components analysed in isolation. Unfortunately, several issues make the use of modular verification techniques difficult in practice. First, deciding how to partition the system into components is not trivial and can have a significant impact on the resources needed for verification. Second, when model-checking a component in isolation, how should the environment of this component be described? In this paper, we address these problems in the framework of model-checking LTL\X action-based properties on Petri nets. We propose an incremental and modular verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account using the linear place invariants of the system.
    Original languageEnglish
    Title of host publicationProceedings of the 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2007) 27-29 June 2007, Tallinn, Estonia
    EditorsJ. Derrick, J. Vain
    Place of PublicationBerlin
    ISBN (Print)978-3-540-73195-5
    Publication statusPublished - 2007
    Eventconference; FORTE 2007, Tallinn, Estonia; 2007-06-27; 2007-06-29 -
    Duration: 27 Jun 200729 Jun 2007

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Conferenceconference; FORTE 2007, Tallinn, Estonia; 2007-06-27; 2007-06-29
    OtherFORTE 2007, Tallinn, Estonia


    Dive into the research topics of 'An incremental modular technique for checking LTL-X properties on Petri nets'. Together they form a unique fingerprint.

    Cite this