# Seminars on Program Logicx and Applications Seminars/Workshops

Speaker: | Nikolay Shilov |
---|---|

Time: | 1999-10-21 15:00:001999-10-22 15:00:001999-10-23 10:00:00 |

Place: | Rm.1403, CS Bldg., Rm.3208, IM Bldg., KAIST |

### Abstract

**Seminar 1. Algorithmic Problems for Propositional Dynamic Logic Variants.
**

This is a general survey (without proofs and technical details) of known
results on expressive power and algorithmic complexity of model checking,
decidability and axiomatizability for several variants of Propositional
Dynamic Logic (PDL) including the Mu-Calculus and the Second-Order
extension of the PDL.

**Seminar 2. Model Checking Problem for the Mu-Calculus.**

This is a detailed survey (with proof sketches) of known and new
original results on algorithmic complexity of model checking for so called
Mu-Calculus, - a propositional polymodal program logic with fixed points.
It can encode basic temporal logics as well as several variants of the
Propositional Dynamic Logic (PDL). Unfortunately, the best known model
checking algorithms for the Mu-Calculus and finite systems are exponential.
It is known also that the model checking problem for the Mu-Calculus and finite
systems is in NP and co-NP. Several fragments of the Mu-Calculus with
polynomial model checking for finite systems have been identified. A
new fragment will be considered in more details.

Prerequisites: basic notions of mathematical logic and theory of
algorithmic complexity.

**Seminar 3. Model Checking of Knowledge and Time in Systems with
perfect Recall. **

This is presentation (with technical details and proof sketches) of new
results developed in collaboration with Dr. Ron van der Meyden for the modal
logic of knowledge and linear time in distributed systems with perfect recall.
It is shown that the model checking problem (1) is undecidable for a
language with operators for "until" and "common knowledge", (2) is PSPACE-
complete for a language with "common knowledge" but without "until",
(3) has non-elementary upper and lower bounds for a language with "until"
but without "common knowledge".

Prerequisites: basic notions of mathematical logic,
theory of algorithmic complexity and
theory of automata on infinite objects.

**Seminar 4. Verification and Specification with REAL.**

To design distributed systems the standard formal description techniques
(FDT), such as Specification and Description Language (SDL), Extended
State Transition Language (ESTELLE), Language of Temporal Ordering
Specification (LOTOS) are used. The verification of FDT specifications
(proving their safety, progress, and other properties) is still an open
problem. The logical approach to the problem consists in the development
of mathematical semantics for FDT, in a choice of a logical language for
property presentation, and in the development of a corresponding proving
methodology.

The approach adopted in the REAL project to verification of SDL
specifications uses two-level scheme which combines the translation of SDL
to a model high-level language with a verification method for the models.
The project uses a especially designed Basic-REAL (bREAL) specification
language. This language with rigorous mathematical semantics is based on
SDL, real-time temporal and dynamic logics.

Syntax and semantics of bREAL can be given in both formal and informal
levels. Some semantical properties of bREAL specifications (including
invariance under stuttering and the interleaving property of concurrency)
can be proved. A specification and verification example (``Good Passenger
and Slot-Machine'') can be given also.

Prerequisite: basic notions of program logics,
of formal description technique and program verification.

[ List ]