Search

• < Previous
• 1
• Next >

---

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;]

---

A Static Analysis Framework for Livelock Freedom in CSP

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&nbsp;[&hellip;]

---

On the Complexity of Equivalence and Minimisation for Q-weighted Automata

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&nbsp;[&hellip;]

---