Paritosh K. Pandya

(January-May 1999)

Each lecture denotes a double lecture spanning 2:00 Hours.

** denotes advance topics. I don't promise to cover these!

Monadic second-order logic over finite and infinite words, trees and graphs.

Model checker MONA.

Decidability of MSO over omega-words. Complexity.

Reductions between between Buchi, Muller, Rabin, Streett automata

and their complexities.

Safra's determinisation construction.

Linear propositional temporal logic

Embedding PTL in MSO

Embedding CTL* in MSO over infinite trees.

Modelchecking algorithm for CTL* formulae and its complexity

Tense logics over arbitrary linear order (PTnL). Monadic theories of various linean orders.

Logic PTnL with strict until and since operators, variety of operators their and expressiveness

Quantification (QPTnL),

Fixed point operators (muPTnL)

Embedding and expressive power of temporal logics for discrete and dense Time.

Statement of Kamps Theorem.

First order Temporal Logic (FOLTL).

Quantified Discrete Duration Calculus (Zhou, Moskowski) QDDC

Embedding QDDC in MSO

Verification of Esterel programs using DCEST (Bus Arbiter Example)

Some examples of verification using SPIN

(Dining philosophers, Dekker's Mutual Exclusion)

Symbolic model checking of modal mu calculus.

Symbolic model checking of CTL formulae.

Model checker SMV

Timed automata. Closure properties.

Regions construction and decidability of emptiness.

Symbolic representation of convex time regions using DBM and its manipulation.

Symbolic modelchecking of Timed systems using Uppaal, Hytech.

(generalised Buchi and Streett acceptance sets). Fair paths.

Fair strongly connected components. Modelchecking algorithm.

Fischer's mutual exclusion algorithm in Uppaal.

Retrospecitve Operators, Nets ...

Characterisation of First-order definable finite and omega-languages

Characterisation of Languages definable in PTL: statement of Kamp's theorem

Decidability MSO over infinite trees. Variations (SnS, SwS).

Decidability of various logics based on MSO over infinite trees.

Monadic Theory of various linear orders (a la Shelah) and their decidability.

- Clarke and Wing survey for strategic directions.
- Thomas handbook of TCS article
- Thomas handbook of formal langauges article.
- Madhavan Tutorial on omega automata
- Madhavan Tutorial on LTL model checking
- Narayan Kumar Tutorial on CTL* and CTL model checking
- Vardi papers on alternating automata and modelchecking
- McMillan book on symbolic model checking
- Alur-Dill paper on "Theory of timed automata" TCS 126
- Uppaal papers on convex region representation