Temporal logic and model checking

Linear and branching-time temporal logics interpreted over infinite words and transition systems, with automata-theoretic and fixed-point model-checking procedures.

• Computation tree logic
• Linear temporal logic
• Büchi automata for a fragment of linear temporal logic
• CTL*
• Linear-time μ-calculus
• Model checking for computation tree logic
• Model checking for linear temporal logic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.