Seminars on Program Logicx and Applications Seminars/Workshops

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.