Tatam is a tool for studying transition systems and LTL formulas. It is characterized by :
- its ability to use infinite domains (integer, real),
- the ability to specify different LTL semantics (truncated, infinite, finite traces),
- its ability to prove analysis termination (maximum size in number of transitions),
- the ability to optimize the solution.