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.
model checking - temporal logics - partial order logics - concurrency
A preliminary version of this paper appears in Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP
98), LNCS 1443, pp. 41–52, 1998.