## 5 Conclusions and Related Works
For this purpose, we use selective mu-calculus to describe system properties, and trace systems are reduced by eliminating the events that do not alter the truth value of a given formula. Finally, it is worth noting that a lot of interesting properties, such as mutual exclusion and absence of starvation, can be elegantly expressed by linear time formulae that usually use a partial order interpretation; while the interleaving interpretation does not allow an easy expression of fairness properties; nevertheless, the use of the selective mu-calculus allows us to express properties, such as precedence and fairness, in a very compact way; for example, the fairness property \"in all computation, eventually aoccurs\" can be expressed through selective mu-calculus by the formula \(\mu Z.(\langle-\rangle_{\emptyset}\operatorname{\tttt}\wedge[-a]_{\emptyset}Z)\). The works [9, 10, 34, 35] also follow the partial order approach to model checking and consider only a representative among all interleavings of actions generated by a parallel composition. The properties that are well handled by these approaches do not concern precedence relations between actions, while they can be profitably used to prove, for example, deadlock freedom. In our approach, properties concerning precedence relations between actions are, in general, described by formulae that induce a consistent reduction of the trace system. On the contrary, the formula describing deadlock freedom induces no reduction, since it involves all events. Thus, the two approaches can be considered as complementary. Other approaches use symbolic model checking (for a survey on the use of this formal verification technique for linear temporal logic, see [36]), which is particularly suited to the verification of reactive systems or concurrent programs. In these approaches, the focus of the state explosion problem is shifted from the size of the state space to the size of the BDD representation, maintaining all problems of defining an automaton, recognizing the complement of the formula to be verified. Abstraction is another successful technique for fighting the state explosion problem in model checking. In [37], the authors present a novel game-based approach to abstraction-refinement for the full \(\mu\)-calculus, interpreted over three-valued semantics, successively improved in [38]. Pushdown systems are transition systems whose states include a stack of unbounded length; hence, they are strictly more expressive than finite state systems. One can argue that pushdown systems are a natural model for sequential programs with procedures where there is no restriction on the call hierarchy among the procedures. Arbitrary recursion is allowable, since the stack can keep track of active procedure calls. Differently form our approach, the main restriction of this kind of model is that it does not handle parallelism. In fact, in [39], the authors show applications of their model checking algorithm for pushdown systems only in the area of sequential program analysis. The model checking problem of pushdown systems against standard branching temporal logics has been intensively studied in the literature. It has been confirmed that, with pushdown systems, the model checking problem is much harder for branching-time temporal logics than for linear-time temporal logics. In particular, for the modal mu-calculus, the most powerful branching temporal logic used for verification, the problem is known to be EXPTIME-complete (even for a fixed formula) [40]. The problem remains EXPTIME-complete also for the logic, CTL. In [41], the author shows that the complexity of the pushdown model checking problem for CTL* is, in fact, 2 EXPTIME-complete. A natural generalization of pushdown machines is pushdown machines with more than one stack [42]. This generalization, unfortunately, is not smooth in terms of the power of these machines: a pushdown automaton with two or more stacks is known to recognize all recursively enumerable languages. The model in its full generality is, thus, intractable.