A partial order approach to branching time logic model checking

R.T. Gerth, R. Kuiper, D. Peled, W. Penczek

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

51 Citaten (Scopus)


Partial order techniques enable reducing the size of the state graph used for model checking, thus alleviating the 'state space explosion' problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods have been studied, implemented and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the logic LTL (linear temporal logic). The paper shows, for the first time, how this approach can be applied to languages that model the behavior of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL* (all logics with the next-time operator removed) and process algebras such as CCS. Conditions on the subset of successors from each node to guarantee reduction that preserves CTL properties are given. Provided experimental results show that the reduction is substantial.
Originele taal-2Engels
TitelProceedings of the Third Israel Symposium on Theory of Computation and Systems (Tel Aviv, Israel, January 4-6, 1995)
UitgeverijInstitute of Electrical and Electronics Engineers
Aantal pagina's10
ISBN van geprinte versie0-8186-6915-2
StatusGepubliceerd - 1995

Vingerafdruk Duik in de onderzoeksthema's van 'A partial order approach to branching time logic model checking'. Samen vormen ze een unieke vingerafdruk.

Citeer dit