02084327

a

02084327 Shilov, Nikolai V. Yi, Kwang On expressive and model checking power of propositional program logics. 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). 2001 Berlin: Springer EN

http://link.springer.de/link/service/series/0558/bibs/2244/22440039.htm

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).