The Library
Efficient model checking for LTL with partial order snapshots
Tools
Niebert, Peter and Peled, Doron (2009) Efficient model checking for LTL with partial order snapshots. Theoretical Computer Science, Vol.410 (No.42). pp. 4180-4189. doi:10.1016/j.tcs.2009.03.002 ISSN 0304-3975.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1016/j.tcs.2009.03.002
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. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. 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 appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one.
Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. in this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution. (C) 2009 Elsevier B.V. All rights reserved.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Journal or Publication Title: | Theoretical Computer Science | ||||
Publisher: | Elsevier Science BV | ||||
ISSN: | 0304-3975 | ||||
Official Date: | 28 September 2009 | ||||
Dates: |
|
||||
Volume: | Vol.410 | ||||
Number: | No.42 | ||||
Number of Pages: | 10 | ||||
Page Range: | pp. 4180-4189 | ||||
DOI: | 10.1016/j.tcs.2009.03.002 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |