Algorithmic Verification for Epistemic Logic  

Outline (tentative): 

 Lecture 1:  
    Motivation 
    Syntax and Semantics of Logics of Knowledge and Time
    Classes of systems: perfect recall, clocks, asynchrony
    Overview of Axiomatic properties of these logics
    Definition of the model checking problem 

 Lecture 2: 
    Model Checking the Logic of Knowledge (basic algorithms and complexity) 
    Review of Buchi automata 
    Model Checking the Logic of Knowledge and Time (basic algorithms and complexity) 

 Lecture 3: 
  Use of a model checker for the logic of knowledge 
  Applications: 
     Security Protocols 
     Knowledge Based Programs 

 Lecture 4: 
  Optimizations of model checking algorithms: 
     BDD techniques 
     Bisimulation techniques 
     techniques for special classes of environments

 Lecture 5: 
   Synthesis from Epistemic Specifications 
   Complexity of Knowledge-Based Programs