M

• Model checkers (17 P)

T

• Temporal logic (17 P)
• Transition systems (5 P)

• Model checking

*

• Region (model checking)
• Signal (model checking)
• Timed word

A

• Abstract model checking
• Alternating timed automaton

B

• Binary decision diagram
• Büchi automaton

C

• Clock (model checking)
• Counterexample-guided abstraction refinement

G

• Generalized Büchi automaton

K

• Kripke structure (model checking)

L

• Linear temporal logic to Büchi automaton
• Linear time property

M

• Metric interval temporal logic
• Metric temporal logic
• Modal μ-calculus
• Muller automaton
• Murφ

P

• Partial order reduction

R

• Reo Coordination Language

S

• Safety and liveness properties
• Symbolic trajectory evaluation

T

• Timed propositional temporal logic