## 5 Conclusions and Related Works
However, for certain model checking applications, pushdown automata with two or more stacks are useful. In [43], the model checking problem for specifications given by nondeterministic pushdown tree automata is studied. The author consider both finite-state (regular) and infinite-state (non-regular) systems. It is shown that for finite-state systems, the model checking problem is solvable in time exponential in both the system and the specification. On the other hand, the model checking problem for context-free systems is undecidable; already for a weak type of pushdown tree automata. In [44], the authors consider the sabotage modal logic (SML) [45], which can arbitrarily delete edges of the model; thus, it has the ability to modify the model under evaluation. In [44], it was shown that the sabotage modality already strengthens modal logic in such a way that all nice model-theoretic properties and algorithmic complexities get lost. In fact, from the viewpoint of complexities, SML much more resembles first-order logic than modal logic (with the exception that the formula complexity remains in PTIME). In [46], the authors examine the complexity of the module checking problem (_i.e._, model checking of open systems) for linear and branching temporal logics. They prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2 EXPTIME-complete for specifications in CTL*. In [47], module checking has been extended to a setting where the environment has imperfect information about the state of the system, _i.e._, to the case where the environment has only a partial view of the system's control states (see also [48] for related work regarding imperfect information). Recently, [49; 50] extended model checking of pushdown systems by introducing open pushdown systems (with perfect information) that interact with their environment. It is shown in [49; 50] that CTL pushdown module checking is 2 EXPTIME-complete and, thus, much harder than pushdown model checking. In [51], the authors extend pushdown module checking to the imperfect information setting and pushdown store content. They study the complexity of this problem with respect to the branching-time temporal logics, CTL, CTL* and the propositional \(\mu\)-calculus. They show that pushdown module checking becomes undecidable when the environment has imperfect information. Improved model checking algorithms have been developed also for hierarchical systems [52; 53; 54]. Such systems are exponentially more succinct than standard state transition graphs, as repeated sub-systems are described only once. In conclusion, our method consists of a variety of attacks to the complexity of the verification. 1. We work directly and only on traces to perform model checking, without representing either traces or systems by some sort of graph, so saving memory. 2. We obtain a finite trace system, also when using unbounded iteration. In such a way, we can perform model checking also in the presence of infinite computations. 3. We reduce the dimension of the trace system, in the number of traces and in the number of events in each trace. Beside the use of abstraction to reduce the number of events of the initial traces, we maintain in a trace at each verification step only the events useful for the following steps, so performing a kind of on-the-fly verification. In such way, we save space, but also verification time, since we decrease the number of times a formula has to be checked. 4. We manipulate traces to decide the satisfaction on a single trace with a polynomial complexity depending on the dimension of the formula and of the trace. The precise complexity of the method needs a deeper examination, since, in general, it depends on the level of concurrency of the systems and on the number of the \(rec\) operators and of the possible one-unfoldings of each hole.