Temporal logics for trace systems : on automated verification

W. Penczek

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer 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.
    Originele taal-2Engels
    Pagina's (van-tot)31-67
    TijdschriftInternational Journal of Foundations of Computer Science
    Nummer van het tijdschrift1
    StatusGepubliceerd - 1993


    Duik in de onderzoeksthema's van 'Temporal logics for trace systems : on automated verification'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit