A partial order approach to branching time logic model checking

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

Research output: Contribution to journalArticleAcademicpeer-review

46 Citations (Scopus)

Abstract

Partial order techniques enable reducing the size of the state space 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 linear temporal logic. The present 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* (with the next time operator removed) and process algebra logics such as Hennesy–Milner logic (withτactions). Conditions on the selection of subset of successors from each state during the state-space construction, which guarantee reduction that preserves CTL* properties, are given. The experimental results provided show that the reduction is substantial
Original languageEnglish
Pages (from-to)132-152
JournalInformation and Computation
Volume150
Issue number2
DOIs
Publication statusPublished - 1999

Fingerprint

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

Cite this