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 μ-Calculus of D. Kozen μ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 < μ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, μC and 2M (in the same settings as above). © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Shilov, N. V., & Yi, K. (2001). On expressive and model checking power of propositional program logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2244 LNCS, pp. 39–46). Springer Verlag. https://doi.org/10.1007/3-540-45575-2_6
Mendeley helps you to discover research relevant for your work.