6 results
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 […]
Published on February 28, 2007
Joel Ouaknine ; Hristina Palikareva ; A. W. Roscoe ; James Worrell.
In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free […]
Published on September 23, 2013
Stefan Kiefer ; Andrzej Murawski ; Joel Ouaknine ; Bjoern Wachter ; James Worrell.
This paper is concerned with the computational complexity of equivalence and minimisation for automata with transition weights in the field Q of rational numbers. We use polynomial identity testing and the Isolation Lemma to obtain complexity bounds, focussing on the class NC of problems within P […]
Published on March 4, 2013
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 […]
Published on May 10, 2019
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 […]
Published on December 7, 2018
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 […]
Published on March 3, 2022