Search

• < Previous
• 1
• Next >

---

On the decidability and complexity of Metric Temporal Logic over finite words

Joel Ouaknine ; James Worrell.

Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all&nbsp;[&hellip;]

---

Model Checking Flat Freeze LTL on One-Counter Automata

Antonia Lechner ; Richard Mayr ; Joël Ouaknine ; Amaury Pouly ; James Worrell.

Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of&nbsp;[&hellip;]

---

On the Expressiveness and Monitoring of Metric Temporal Logic

Hsi-Ming Ho ; Joël Ouaknine ; James Worrell.

It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of MTL with the same&nbsp;[&hellip;]

---

Sequential Relational Decomposition

Dror Fried ; Axel Legay ; Joël Ouaknine ; Moshe Y. Vardi.

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in&nbsp;[&hellip;]

---