## 5 Conclusions and Related Works  
In this work, we define the notion of satisfaction for the formulae of a temporal logic calculus, when interpreted on a trace system, _i.e._, a partial order representation of the concurrent system. The calculus we use is a temporal logic, whose formulae directly characterize possible abstractions of the system preserving their truth values; more precisely, the events relevant for checking a formula are only the ones explicitly mentioned. Different action logics, such as [14], whose operators could be used in a linear fashion to concisely express fairness properties, are not suitable to individuate system abstractions preserving the truth values of formulae. We use a well-known partial order model for computations, that is [PERSON]'s trace system [20]. Recently, Mazurkiewicz traces have been also extended with time in order to capture the concurrency and timing constraints among the services of systems [23]. It is known that model checking has a different complexity when using linear time or branching time logics [5, 17, 18]. 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 ones for the linear time logics (LTL) run in time \(\mathcal{O}(n2^{m})\). The works [24, 25] relate branching and linear model checking. The authors study the problem of deciding whether a linear-time property, specified by either an automaton or an LTL formula, can be translated to a branching time logic formula and describe the translation when this exists. A disadvantage of this method is that a higher complexity of the formula is achieved, since its size must be increased by some prefix; moreover, also fairness requirements must be expressed by a new formula prefixed to the translation of the old one. Other works [26, 27] check linear time formulae on a structure that is the unfolding of the Petri net representing the system, _i.e._, a partial order model. Nevertheless, this method requires the construction of a, possibly infinite, safe net to represent the behavior of the system. Solutions exist to this problem that exploit [PERSON]'s finite prefix [28]. The product automaton is obtained from the finite prefix and the Buchi automaton representing the formula. In [29, 30], for example, the satisfaction of linear time mu-calculus formulae is checked using alternating Buchi automata. Some different approaches (for example, [20, 31, 32]) interpret the logic on the dependence graphs among events, instead of linearizations. Moreover, the state explosion problem is present also for this type of graph. A similar approach is the automata-theoretic one [25], which is based on the product between the finite state automaton representing the system and the one representing the formula. Furthermore, such an approach suffers from the state-explosion problem, due to the interleaving of concurrent events; several methods for the reduction of the state space have been suggested in this case [7, 9, 33, 34]. A different approach could be that of using a partial order interpretation, where it is possible to distinguish concurrency from nondeterminism, trying to keep the advantage of not exploding the state space of the system due to the concurrency using trace systems. Our method exploits the compact notation of equivalence classes of behaviors; moreover, the satisfaction of a formula is decided by an algorithm that works directly on the traces (thus, a sequential memory representation) without constructing any type of graph; so saving space and time. The work pays further attention to the reduction of the state space of the system, since, as argued in [17, 24], this is the greatest part of the complexity of the model checking procedure, provided that interesting properties are generally of a small size.