A partial order approach to branching time logic model checking

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

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

53 Citaten (Scopus)

Samenvatting

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
Originele taal-2Engels
Pagina's (van-tot)132-152
TijdschriftInformation and Computation
Volume150
Nummer van het tijdschrift2
DOI's
StatusGepubliceerd - 1999

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