Verification of Harware and Software

Final Exam

Expressive Completeness

  • My Survey on Expressive Completeness. Expressive Power of Temporal Logics
  • A note by I. Hodkinson with a short proof of Kamp's theorem. Notes on games in temporal logic
  • A paper by T. Wilke with a short proof of Kamp's theorem for discrete orders. Classifying discrete temporal properties. In Christoph Meinel, editor, STACS'99, volume 1563 of Lecture Notes in Computer Science, pages 32-46, Trier, Germany, 1999. Springer.

    Slides for the talk on 4/1/04

    Slides for the talk on 18/1/04

    References

    E. Allen Emerson.
    Automated Temporal Reasoning about Reactive Systems.
    Logics for Concurrency: Structure versus Automata, F. Moller and G. Birtwistle (eds.), Springer LNCS no. 1043, Pages 111-120

    E. Allen Emerson.     Temporal and Modal Logic.
    Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics 1990, J. van Leeuwen, ed., North-Holland Pub. Co./MIT Press, Pages 995-1072.

    A. Rabinovich
    Expressive Power of Temporal Logics
    In Proc. 13th Int. Conf. on Concurrency Theory. Brno, Czech Republic Aug. 2002}, volume 2421 of Lecture Notes in Computer Science, pages 57--75. Springer, 2002.

    Ph. Schnoebelen.
    The complexity of temporal logic model checking.
    In Advances in Modal Logic, papers from 4th Int. Workshop on Advances in Modal Logic (AiML'2002), Sep.-Oct. 2002, Toulouse, France. World Scientific, 2003. To appear.

    W. Thomas.
     Languages, automata and logic.
    Technical Report 9607, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, May 1996.