Learn · Model Checking

Lecture 47 of 55Algorithms for CTL

Module 3: Final algorithm

Prof. Srivathsan.B · Chennai Mathematical Institute

Credits and licence

From
Model Checking, Chennai Mathematical Institute (at NPTEL)
Licence
CC BY-NC-SA, as NPTEL states it. Non-commercial use only.
Attribution
NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge. Coordinated by IIT Madras.
Who can watch
Tweens profiles and older. How courses are placed

All the lectures

  1. Course Overview Video
  2. Module 1: Modeling code behaviour Video
  3. Module 2: Modeling hardware circuits Video
  4. Module 3: Modeling data-dependent programs Video
  5. Module 4: Modeling concurrent systems Video
  6. Summary Video
  7. Module 1: Model checking tools Video
  8. Module 2: Simple models in NuSMV Video
  9. Module 3: Hardware verification using NuSMV Video
  10. Module 4: Modeling concurrent systems in NuSMV Video
  11. Summary. Video
  12. Module 1: A problem in concurrency Video
  13. Module 2: What is a property? Video
  14. Module 3: Invariants Video
  15. Module 4: Safety properties Video
  16. Module 5: Liveness properties Video
  17. Summary.. Video
  18. Module 1: Road map Video
  19. Module 2: A gentle introduction to automata Video
  20. Module 3: Simple properties of finite automata Video
  21. Module 4: Safety properties described by automata Video
  22. Summary... Video
  23. Module 1: Specifying properties Video
  24. Module 2: Omega-regular expressions Video
  25. Module 3: Bchi automata Video
  26. Module 4: Simple properties of Bchi automata Video
  27. Summary.... Video
  28. Module 1: Overview Video
  29. Module 2: Omega-regular expressions to NBA Video
  30. Module 3: Checking emptiness of NBA Video
  31. Module 4: Generalized NBA Video
  32. Summary..... Video
  33. Module 1: Introduction to LTL Video
  34. Module 2: Semantics of LTL Video
  35. Module 3: A puzzle Video
  36. Summary . Video
  37. Module 1: Automata based LTL model-checking Video
  38. Module 2: LTL to NBA Video
  39. Module 3: Automaton construction Video
  40. Summary .. Video
  41. Module 1: Tree view of a transition system Video
  42. Module 2: CTL* Video
  43. Module 3: CTL Video
  44. summary ... Video
  45. Module 1: Adequate CTL formulae Video
  46. Module 2: EX, EU, EG Video
  47. Module 3: Final algorithm Video
  48. Module 4: State-space explosion Video
  49. Summary .... Video
  50. Module 1: Introduction to BDDs Video
  51. Module 2: Ordered BDDs Video
  52. Module 3: Representing transition systems as OBDDs Video
  53. Summary ..... Video
  54. Timed transition systems Video
  55. Concluding remarks Video