Contents

• Preface
• The Engineering Framework
  • From Interfaces to property Sets
  • Deterministic or Probabilistic Property Sets
  • Automata, Properties, Execution Graphs
  • Formal Semantics and Truth Conditions
  • (Classical) Model Theory
  • Logic and Semantics
  • Model Checking
  • Automated Theorem Proving
  
  
• Introduction
  • A Toy Problem
  • Model as Transition Graph
  • Model as Execution Graph
  • Introducing Properties
  • Specification Language CTL
  • Finite Automata
  • Automaton with Output
  • Automaton with Properties
  • Model Checking
  • Symbolic Model Checking
  
  
• Introduction Version 2
  • Properties vs. States
  • Problem $P$
  • System Interface $S^{0}I$
  • Actions
  • Properties Language $L_{PROP}$
  • Minimal Property Sets
  • Minimal Transitions
  • An induced Automaton $A$
  
  
• Automata, Languages, and Graphs
  • Historical Remarks to the concept 'Automaton'
  • Finite Automata and Languages
  • Some Definitions regarding Language
  • Some Definitions regarding Graphs
    • (Ordinary) Graph
    • Directed Graph
    • Tree
    • Graph extended with Input-Output and Labels
    • Execution Graph
  • Formal Definition of Finite Automata
    • (Ordinary) Finite Automata
    • Finite and Infinite Input
    • Deterministic and Non-Deterministic Automaton
    • Automata with Output: Moore, Mealy, finite Transducer
    • Finite Labelled Automaton
    • Example of an Automaton with Graphs
  • Timed Automata
    • Discrete and Continous Time
    • Example extended with Clocks
    • Finite Automata and Clocks
    • Automata Theoretic Semantics of Time
    • Timed CTL: TCTL and tCTL
    • Model Checking
  • Connected Automata
  
  
• Temporal Logics
  • Bits of History
  • The Syntax of $L_{CTL^{*}}$
  • The Syntax of $L_{CTL}$
  • The Semantics of $L_{CTL}$- and $L_{CTL^{*}}$-Expressions
    • Properties and Logical Operators
    • Time and Temporal Operators
    • Quantifier
    • Examples of CTL-Expressions with Interpretations
  
  
• Specifying with Temporal Logic
  • Reachability Property
  • Safety Property
  • (Simple) Liveness Property
  • Deadlock Freeness
  • Fairness Property
  
  
• Verification as Model Checking
  • Bits of History
  • General Idea
  • Symbolic Model Checking
    • Ordered Binary Decision Diagrams
    • Fixpoint Representations
  • The SMV-Model Checker Software
  
  
• Exercises
  • Exercise 1: Engineering Process
  • Exercise 2: Automata and Their Behavior
  • Exercise 3: CTL
  • Exercise 4: Model Checking (Without Time)
  • Exercise 5: Timed Automata
  
  
• Bibliography