Linear time temporal logics over mazurkiewicz traces

Abstract

Temporal logics are a well-established tool for specifying and reasoning about the computations performed by distributed systems. Although temporal logics are interpreted over sequences, it is often the case that such sequences can be gathered together into equivalence classes where all members of an equivalence class represent the same partially ordered stretch of behaviour of the system. This appears to have important imphcations for improving the practical efficiency of automated verification methods based on temporal logics. With this as motivation, we study logics that are directly interpreted over partial orders. We survey a number of linear time temporal logics whose underlying frames are Mazurkiewicz traces. We describe automata theoretic methods for solving the satisfiability and model checking problems for these logics. It turns out that we still do not know what the “canonical” hnear time temporal logic over Mazurkiewicz traces looks hke. We identify here the criteria that should be met by this elusive logic.