A partial order approach to branching time logic model checking

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

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

54 Citations (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.
Original languageEnglish
Title of host publicationProceedings of the Third Israel Symposium on Theory of Computation and Systems (Tel Aviv, Israel, January 4-6, 1995)
PublisherInstitute of Electrical and Electronics Engineers
Number of pages10
ISBN (Print)0-8186-6915-2
Publication statusPublished - 1995


Dive into the research topics of 'A partial order approach to branching time logic model checking'. Together they form a unique fingerprint.

Cite this