Catálogo de publicaciones - libros

The model checking problem for finite-state open systems () has been extensively studied in the literature, both in the context of environments with perfect and imperfect information about the system. Recently, the perfect information case has been extended to infinite-state systems (). In this paper, we extend pushdown module checking to the imperfect information setting; i.e., the environment has only a partial view of the system’s control states and pushdown store content. We study the complexity of this problem with respect to the branching-time temporal logic , and show that pushdown module checking, which is by itself harder than pushdown model checking, becomes undecidable when the environment has imperfect information. We also show that undecidability relies on hiding information about the pushdown store. Indeed, we prove that with imperfect information about the control states, but a visible pushdown store, the problem is decidable and its complexity is the same as that of (perfect information) pushdown module checking.

We investigate various classes of alternating automata for visibly pushdown languages () over infinite words. First, we show that alternating visibly pushdown automata () are exactly as expressive as their nondeterministic counterpart () but basic decision problems for are -complete. Due to this high complexity, we introduce a new class of alternating automata called (). extend classical alternating automata over infinite words by also allowing moves. A non-local forward move leads a copy of the automaton from a call input position to the matching-return position. We also allow local and non-local backward moves. We show that one-way and two-way have the same expressiveness and capture exactly the class of . Moreover, boolean operations for are easy and basic decision problems such as emptiness, universality, and pushdown model-checking for parity two-way are -complete. Finally, we consider a linear-time fixpoint calculus which subsumes the full linear-time -calculus (with both forward and backward modalities) and the logic and captures exactly the class of . We show that formulas of this logic can be translated into parity two-way , and vice versa. As a consequence satisfiability and pushdown model checking for this logic are -complete.

We re-examine vacuity in temporal logic model checking. We note two disturbing phenomena in recent results in this area. The first indicates that not all vacuities detected in practical applications are considered a problem by the system verifier. The second shows that vacuity detection for certain logics can be very complex and time consuming. This brings vacuity detection into an undesirable situation where the user of the model checking tool may find herself waiting a long time for results that are of no interest for her.

In this paper we define , an extension of antecedent failure to temporal logic, which refines the notion of vacuity. According to our experience, this type of vacuity indicates a problem in the model, environment or formula. On top, detection of this vacuity is extremely easy to achieve. We base our definition and algorithm on regular expressions, that have become the major temporal logic specification in practical applications.