Temporal logics for trace systems : on automated verification

W. Penczek

    Research output: Contribution to journalArticleAcademicpeer-review


    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
    Issue number1
    Publication statusPublished - 1993


    Dive into the research topics of 'Temporal logics for trace systems : on automated verification'. Together they form a unique fingerprint.

    Cite this