Helmut Seidl. Model-Checking for L_2. , volume 97-18 of Forschungsbericht, 1997. Universität Trier, Mathematik/Informatik.
We present a model-checking algorithm for fragment L 2 of the propositional modal - calculus [12, 7] based on distributive functions. We illustrate the usefulness of our approach by uniformly deriving fast L 2 -model-checking algorithms both for finite transition systems as well as for infinite-state transition systems like pushdown processes. 1 Introduction The propositional modal -calculus as considered by Kozen in  has been proven to be extremely useful for the verification of finite state systems. Although not being very intuitive for expressing system properties, - calculus has been successfully used as an intermediate formalism for many temporal logics to be compiled into. While the best known algorithms for checking arbitrary closed -formulas on finite transition systems are still exponential in the alternation-depth of the formula [8, 13, 19], it has been observed that, luckily, standard translations of temporal logics like CTL , PDL\Delta and ECTL do not result i..