Satisfiability and model-checking for a variant of the Computational
Tree Logic of Knowledge (CTLK)
-----------------------------------
          
ABSTRACT
-----------------------------------
We show that CTLK with a semantics based on concrete observability, 
with perfect recall and synchrony, has an undecidable satisfiability 
problem, and a decidable model-checking problem. 
The complexity of the model-checking problem is nonelementary in 
the size of the model.
          
SPEAKER(S)
-----------------------------------
Prof.dr. Catalin DIMA
Universite Paris Est - Creteil
Paris
Franta
-----------------------------------
Prof.dr. Catalin Dima is a member of the Laboratoire d'Algorithmique, 
Complexite et Logique (LACL) of the Universite Paris Est - Creteil 
(formerly Universite Paris 12), in the "Specification et Verification 
de Systemes" team. 
He has a PhD from Universite Joseph Fourier Grenoble (2001), 
while he was at  Verimag, Grenoble, in the "Timed and Hybrid Systems" 
team. Other past positions include a one-year position at ENSEIRB 
and LaBRI (Bordeaux), a one-year position in the BIP team of 
INRIA Rhone Alpes (Grenoble), and a position within the Department 
of Foundations of Computer Science of the University of Bucharest.
He held several visiting professorship positions at the University 
of Insubria (Como) and is a former fellow of UNU/IIST Macau.

Webpage: http://lacl.univ-paris12.fr/dima/
-----------------------------------