On the connection of partial order logics and partial order reduction methods
Peter Niebert, Wojciech Penczek · TU/e Research Portal · 1995
. We examine the connection between "equivalence robust" subsets of propositional temporal logics (LTL and CTL*), for which partial order reduction methods can be applied in model checking, and partial order logics and equivalences. For the linear case we show how to naturally translate "equivalence robust" LTL properties into Thiagarajan's linear time temporal logic for traces (TrPTL), substantiating the claim that partial order logics have the right syntax for equivalence robust properties. For the branching case we define a parametrised dependency relation (D; V ) yielding an (D; V )-equivalence notion for trees that generalizes Mazurkiewicz's trace equivalence. Then, we show that under some condition (D;V )-equivalent trees are stuttering equivalent and therefore cannnot be distinguished by any CTL-X formulas. We prove that partial order reductions for CTL-X give (D; V )-equivalent trees. Our approach can be used as a semantic basis for branching time partial order logic...