Temporal logics for trace systems : on automated verification

W. Penczek

    Research output: Contribution to journalArticleAcademicpeer-review

    Abstract

    We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTLP, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to CTLP. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.
    Original languageEnglish
    Pages (from-to)31-67
    JournalInternational Journal of Foundations of Computer Science
    Volume4
    Issue number1
    DOIs
    Publication statusPublished - 1993

    Fingerprint

    Temporal logic
    Model checking
    Specifications

    Cite this

    @article{d827dfb6ac5b4558b9efcfa425097f06,
    title = "Temporal logics for trace systems : on automated verification",
    abstract = "We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTLP, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to CTLP. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.",
    author = "W. Penczek",
    year = "1993",
    doi = "10.1142/S0129054193000043",
    language = "English",
    volume = "4",
    pages = "31--67",
    journal = "International Journal of Foundations of Computer Science",
    issn = "0129-0541",
    publisher = "World Scientific",
    number = "1",

    }

    Temporal logics for trace systems : on automated verification. / Penczek, W.

    In: International Journal of Foundations of Computer Science, Vol. 4, No. 1, 1993, p. 31-67.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Temporal logics for trace systems : on automated verification

    AU - Penczek, W.

    PY - 1993

    Y1 - 1993

    N2 - We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTLP, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to CTLP. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.

    AB - We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTLP, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to CTLP. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.

    U2 - 10.1142/S0129054193000043

    DO - 10.1142/S0129054193000043

    M3 - Article

    VL - 4

    SP - 31

    EP - 67

    JO - International Journal of Foundations of Computer Science

    JF - International Journal of Foundations of Computer Science

    SN - 0129-0541

    IS - 1

    ER -