Path-Checking for MTL and TPTL over Data Words

Precise complexity results are derived for the model checking problems for MTL (metric temporal logic) and TPTL (timed propositional temporal logic) on (in)finite data words and deterministic one-counter machines. Depending on the number of register variables and the encoding of numbers in constraints (unary or binary), the complexity is either P-complete or PSPACE-complete.

Authors

• Shiguang Feng

Keywords

No keywords are indexed for this paper.