Concept
Metric temporal logic
Overview
Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is a linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly monotonic integer-time semantics.
MTL has been described as a prominent specification formalism for real-time systems. Full MTL over infinite timed words is undecidable.
Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).
Related ideas
- Propositional variable
- Logical connective
- Temporal logic
- Modal operator
- De Morgan's laws
- Linear temporal logic
- Metric interval temporal logic
Place in the tradition
Part of Temporal logic.