Speaker:Nikolay V. Shilov
Time:2000-06-21 ~ 2000-12
Place:Rm.1215, Industrial Management Bldg. KAIST

Abstract

06-21: Syntax, Semantics and Model and Properties of the Propositional Fixpoint Calculus Variants.

Abstract: A fixpoint calculus is a program logic where formulae are predicate transformers with explicit fixpoints. A propositional fixpoint calculus is a fixpoint calculus with monadic formulae only. There exists 2 basic variants of propositional fixpoint calculus: the FIX-Calculus (FIX) of V.R. Pratt and the Mu-Calculus (MuC) of D. Kozen. Syntax and semantics of both variants were introduced in details, while basic model properties (monotonicity, small model vs. finite model, expressive power) were presented without proofs.

06-24: Algorithmic Problems for the Propositional Mu-Calculus.

Abstract: Model checking is an algorithmic problem of testing a model against a formula, while decidability is another problem of checking whether a formula is a tautology. It is known that model checking problem for MuC in finite models is NP- and co-NP-hard simultaneously, while all known algorithm are exponential where a power depends of formula size only. As far as concern lower and upper bounds for decidability then both are exponential of formula size too. Upper bounds for both algorithmic problems were discussed in details.

07-05: Propositional Modal, Temporal and Dynamic Logics as Fragments of MuC.

Abstract: A classical basic propositional modal logic K can be introduced for computer scientists as a fixpoint-free fragment of MuC with a single program. In contrast, MuC can be introduced for mathematicians as a polymodal variant of K with least fixpoints. In the lecture the first paradigm was exploited for formal introduction of basic propositional modal logic K and branching time logics CTL of E.M. Clarke, the propositional dynamic logic PDL of M.J. Fisher and R.E. Ladner. A survey of basic model and algorithmic properties was presented also.

07-12: More Program Logics.

Abstract: Like in the previous lecture another basic propositional modal logics S5 and the propositional logic of knowledge Kn were introduced as fragments of MuC. A survey of basic model and algorithmic properties was presented too. But in contrast to all program logics which were discussed in the tutorial, a so called the full branching time logic CTL* can not be presented as a fragment of MuC, while MuC can encode state formulae of CTL* with an exponential blow up. Hence it is not surprising that model checking problem for CTL* in finite models is polynomial of model size and exponential of formula size. As far as concern lower and upper bounds for decidability then both are double exponential of formula size.

[ List ]