Search

• < Previous
• 1
• Next >

---

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

---

Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems

Franck van Breugel ; Babita Sharma ; James Worrell.

Desharnais, Gupta, Jagadeesan and Panangaden introduced a family of behavioural pseudometrics for probabilistic transition systems. These pseudometrics are a quantitative analogue of probabilistic bisimilarity. Distance zero captures probabilistic bisimilarity. Each pseudometric has a discount&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 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;]

---

Two Variable vs. Linear Temporal Logic in Model Checking and Games

Michael Benedikt ; Rastislav Lenhardt ; James Worrell.

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we consider two such restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO2).&nbsp;[&hellip;]

---

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

---

Minimisation of Multiplicity Tree Automata

Stefan Kiefer ; Ines Marusic ; James Worrell.

We consider the problem of minimising the number of states in a multiplicity tree automaton over the field of rational numbers. We give a minimisation algorithm that runs in polynomial time assuming unit-cost arithmetic. We also show that a polynomial bound in the standard Turing model would require&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;]

---

Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata

Vojtěch Forejt ; Petr Jančar ; Stefan Kiefer ; James Worrell.

We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). We first show a general&nbsp;[&hellip;]

---