\input zb-basic
\input zb-ioport
\iteman{io-port 02084327}
\itemau{Shilov, Nikolai V.; Yi, Kwang}
\itemti{On expressive and model checking power of propositional program logics.}
\itemso{Bj\o rner, Dines (ed.) et al., Perspectives of system informatics. 4th international Andrei Ershov memorial conference, PSI 2001, Akademgorodok, Novosibirsk, Russia, July 2--6, 2001. Revised papers. Berlin: Springer (ISBN 3-540-43075-X). Lect. Notes Comput. Sci. 2244, 39-46 (2001).}
\itemab
Summary: We examine when a model checker for a propositional program logic can be used for checking another propositional program logic in spite of lack of expressive power of the first logic. We prove that (1) a branching time Computation Tree Logic CTL, (2) the propositional $\mu$-Calculus of D. Kozen $\mu$C, and (3) the second-order propositional program logic 2M of C. Stirling enjoy the equal model checking power in spite of difference in their expressive powers CTL $< \mu$ C $<$ 2M: every listed logic has a formula such that every model checker for this particular formula for models in a class closed w.r.t. finite models, Cartesian products and power-sets can be reused for checking all formulae of these logics in all models in this class. We also suggest a new second-order propositional program logic SOEPDL and demonstrate that this logic is more expressive than 2M, is as expressive as the Second-order Logic of monadic Successors of M. Rabin (S(n)S-Logic), but still enjoys equal model checking power with CTL, $\mu$C and 2M (in the same settings as above).
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{http://link.springer.de/link/service/series/0558/bibs/2244/22440039.htm}
\end