Paper Info
Title
Efficient model checking for LTL with partial order snapshots
Abstract
Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Examples of such properties are serializability of a database or snapshots. Recently, a modest extension for LTL by an operator that expresses snapshots has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot (also called a slice or a cut) was passed, perhaps not in the observed (interleaved) execution sequence, but possibly in a (trace) equivalent one. A model checking algorithm was suggested for a subset of this logic, with PSPACE complexity in the size of the system and the checked formula. For the whole logic, a solution that is in EXSPACE in the size of the system (PSPACE in the number of its global states) was given. In this paper, we provide a model checking algorithm in PSPACE in the size of a system of communicating sequential processes when restricting snapshots to boolean combinations of local properties of each process. Concerning size of the formula, it is PSPACE for the case of snapshot properties expressed in DNF, and EXPSPACE where a translation to DNF is necessary.
Year
DOI
Venue
2009
10.1016/j.tcs.2009.03.002
Theor. Comput. Sci.
Keywords
Field
DocType
partial order snapshot,concurrent system,observed execution sequence,model checking,concurrent history,efficient model checking,partial order,global snapshot,partial order semantics,polynomial space,model checking algorithm,useful partial order concept,snapshots,temporal logics,concurrency,exponential space,interleaving semantics,distributed system
Discrete mathematics,Model checking,Concurrency,Computer science,Algorithm,Disjunctive normal form,Theoretical computer science,EXPSPACE,PSPACE,Boolean algebra,Linear logic,Temporal logic
Journal
Volume
Issue
ISSN
410
42
Theoretical Computer Science
ISBN
Citations 
PageRank 
3-540-33056-9
1
0.35
References 
Authors
13
2
Name
Order
Citations
PageRank
Peter Niebert135725.28
Doron Peled23357273.18