UNSPECIFIED (2006) Efficient model checking for LTL with partial order snapshots. In: 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Vienna, AUSTRIA, MAR 25-APR 02, 2006. Published in: TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 3920 pp. 272-286.

Full text not available from this repository.

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.

Item Type:	Conference Item (UNSPECIFIED)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name:	LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title:	TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS
Publisher:	SPRINGER-VERLAG BERLIN
ISBN:	3-540-33056-9
ISSN:	0302-9743
Editor:	Hermanns, H and Palsberg, J
Date:	2006
Volume:	3920
Number of Pages:	15
Page Range:	pp. 272-286
Publication Status:	Published
Title of Event:	12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Location of Event:	Vienna, AUSTRIA
Date(s) of Event:	MAR 25-APR 02, 2006
URI:	http://wrap.warwick.ac.uk/id/eprint/33525

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item