The Library
Deciding global partial-order properties
Tools
UNSPECIFIED (2005) Deciding global partial-order properties. FORMAL METHODS IN SYSTEM DESIGN, 26 (1). pp. 7-25. doi:10.1007/s10703-005-4592-0 ISSN 0925-9856.
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.1007/s10703-005-4592-0
Abstract
Model checking of asynchronous systems is traditionally based on the interleaving model, where an execution is modeled by a total order between atomic events. Recently, the use of partial order semantics, representing the causal order between events, is becoming popular. This paper considers the model checking problem for partial-order temporal logics. Solutions to this problem exist for partial order logics over local states. For the more general global logics that are interpreted over global states, only undecidability results have been proved. In this paper, we present a decision procedure for a partial order temporal logic over global states. We also sharpen the undecidability results by showing that a single until operator is sufficient for undecidability.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Journal or Publication Title: | FORMAL METHODS IN SYSTEM DESIGN | ||||
Publisher: | SPRINGER | ||||
ISSN: | 0925-9856 | ||||
Official Date: | January 2005 | ||||
Dates: |
|
||||
Volume: | 26 | ||||
Number: | 1 | ||||
Number of Pages: | 19 | ||||
Page Range: | pp. 7-25 | ||||
DOI: | 10.1007/s10703-005-4592-0 | ||||
Publication Status: | Published |
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 |