## 1 Introduction and Motivation  
Linear time [1] and branching time [2] temporal logics are used for specifying and verifying concurrent and distributed systems: partial order models (trace systems are an example) are mostly used to give semantics to linear time logics, while interleaving models (such as transition systems) are widely used for branching time logics. To express properties inherent in concurrency, _i.e._, properties distinguishing concurrency from nondeterminism, a partial order interpretation for the logic fits better. This interpretation allows also a good definition of fairness properties as, for example, inevitability under the fairness assumption [3, 4]: \"in all computations the event \(a\) eventually occurs\". Model checking is one of the main methods for the automated verification of concurrent systems [5]; it consists in checking whether a structure representing the system is a model for a logic formula. Modelchecking very large concurrent systems may cause the so-called \"state explosion problem\" and lead to a too big number of states of the structure. A variety of methods for reducing the state explosion problem have been developed [6; 7; 8; 9; 10]; in the context of branching time logics, in [11; 12], the authors and others proposed a logic, called selective mu-calculus, equi-expressive to mu-calculus [13], but, such that each formula directly characterizes an abstraction of the system that maintains the truth value of the formula itself. Different action logics, such as [14], whose operators could be also used in a linear fashion to concisely express fairness properties, are not suitable to individuate system abstractions preserving the truth values of formulae. A further problem is the model checking of infinite representation of systems: for example, in trace systems, recursive behaviors are usually represented by means of an infinite set of finite traces (see [15], solutions for branching time logic are in [16]). Finally, it is known that, while a lot of interesting correctness properties, such as mutual exclusion and the absence of starvation, can be elegantly expressed by linear time formulae, the model checking of a linear time logic and that of a branching time logic [5; 17; 18] have different complexity. For example, given a transition system of size \(n\) and an alternation-free temporal logic formula of size \(m\), model checking algorithms for the branching time logic (CTL)run in time \(\mathcal{O}(nm)\), while those for the linear time logics (LTL) run in time \(\mathcal{O}(n2^{m})\). This result holds also in the case of generalized model checking [19]. In this work, we give a non-interleaving interpretation of selective mu-calculus formulae using the simplest and best known partial order model for computations, that is [PERSON]'s trace system [3; 15; 20]. This model allows a compact representation of the system computations using only an element, called trace, to represent an equivalence class of sequences of events with respect to a dependence relation. A similar approach has been carried on with the logic CTL in [21]. More precisely, the author defines an extension of CTL by past modalities, called \(CTL_{P}\), and interpreted over [PERSON]'s trace systems. The author's aim is to obtain the model checking of properties described in this logic with a linear complexity, as is that of CTL on transition systems: on the contrary, he proved that model checking for \(CTL_{P}\) on traces is NP-hard, even if past modalities cannot be nested. Differently from [21], the aim of this article is to check the satisfaction of our formulae directly on traces, _i.e._, we suppose using a sequential memory representation for traces and no graph representation of the system, but only a representation of dependencies. Moreover, we employ a trace abstraction, induced by the selective formulae, and we simplify the traces by discarding, at each verification step, the events that are no more of interest for the successive verification.