Diagramy decyzyjne i model checking CTL

Zapewne nie wszystkie z poniższych tematów zdążę poruszyć, ale ogólny plan wygląda tak:
  * Diagramy decyzyjne (BDD):
      - Definicje, struktura
      - Operacje
      - Uwagi implementacyjne
      - Warianty
  * Model checking:
      - Definicje: modele, formuły itp.
      - Weryfikacja bezpośrednia
      - Weryfikacja symboliczna:
          - Za pomocą BDD
          - Za pomocą SAT-solvera.
      -  Zastosowania przy weryfikacji oprogramowania