Name
Abstract | ||
|---|---|---|
Model checking of asynchronous systems is traditionally based on the interleaving model, where an execution is modeled by
a total order between events. Recently, the use of partial order semantics that allows independent events of concurrent processes
to be unordered is becoming popular. Temporal logics that are interpreted over partial orders allow specifications relating
global snapshots, and permit reduction algorithms to generate only one representative linearization of every possible partial-order
execution during state-space search. This paper considers the satisfiability and the model checking problems for temporal
logics interpreted over partially ordered sets of global configurations. For such logics, only undecidability results have
been proved previously. In this paper, we present an Expspace decision procedure for a fragment that contains an eventuality operator and its dual. We also sharpen previous undecidability
results, which used global predicates over configurations. We show that although our logic allows only local propositions
(over events), it becomes undecidable when adding some natural until operator.
|
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/s10703-005-4592-0 | Formal Methods in System Design |
Keywords | Field | DocType |
global partial-order properties,temporal logics,general global logic,total order,partial order logic,causal order,model checking,global state,partial order semantics,undecidability result,concurrency,partial order logics,partial order,interleaving model,state space,temporal logic,partially ordered set,satisfiability,asynchronous system | Discrete mathematics,Model checking,Computer science,Satisfiability,Algorithm,EXPSPACE,Theoretical computer science,Operator (computer programming),Program analysis,Partially ordered set,Linearization,Undecidable problem | Journal |
Volume | Issue | ISSN |
26 | 1 | 0925-9856 |
ISBN | Citations | PageRank |
3-540-64781-3 | 10 | 0.70 |
References | Authors | |
23 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rajeev Alur | 1 | 17253 | 1413.65 |
| Kenneth L. McMillan | 2 | 3332 | 269.05 |
| Doron Peled | 3 | 3357 | 273.18 |