Информационная система "Конференции"

Abstracts

Applications of logic in computer science

Paper examines when a model checker for a state-based propositional program logic can be used (in principle) for checking another state-based propositional program logic in spite of lack of expressive power of the first logic. In particular we study (1) a branching time Computation Tree Logic CTL, (2) the propositional mu-Calculus of D. Kozen MuC,and (3) the second-order propositional program logic 2M of C. Stirling. It is known that CTL<MuC<2M in terms of expressive power. We demonstrate that all these logics enjoy the equal model checking power in the following sense: every listed logic has a formula such that every checker for this particular formula for models in any class closed w.r.t. finite models, Cartesian products and power-sets can be used for checking all formulae of these logics in all models in this class. These particular formulae are existential reachability formula EF of CTL and winning strategies formula WIN of MuC. Thus informally speaking, we prove that a reachability checker or finite game solver can be used (in principle) for model checking very expressive state-base propositional program logics like MuC and 2M.

The driving forces of our proofs is Hitika-like game-theoretic semantics for a state-based second-order propositional program logic Second-Order Elementary Propositional Dynamic logic SOEPDL. We demonstrate that 2M<SOEPDL in expressive power, and prove that SOEPDL is as expressive as a fragment with single free first order variable of the Second order Logic of several Successors SnS of M. Rabin. We refer this fragment as the strict monodic Second order Logic of several Successors SnS(mo) due to similarity with Monodic First-Order Temporal Logic. We also demonstrate how to interpret SnS in SnS(mo). It implies that SOEPDL and SnS(mo) in general are undecidable, while both logics are decidable with a non-elementary lower bound in infinite n-branching tree. In spite of expressive power and complexity, SOEPDL still enjoys equal model checking power with CTL, MuC and 2M (in the same settings as above).

Mail to Webmaster alc9@math.nsc.ru

|Home Page| |English Part|

Go to Home