Undecidability of Partial Order Logics

Rajeev Alur and Doron Peled

In this paper we prove the undecidability of certain temporal logics over partial orders. The proof we use is generic and can be applied to characterize various termpoal operators that cannot be used for automatic verification (model checking). We propose that these results partially explain why the partial order model of concurrency has not gained as much popularity as the interleaving model.

Information Processing Letters 69(3), 1999.