### Topics

- Linear Dynamical Systems
- Timed Automata and Metric Temporal Logic
- Infinite-State systems and Automata
- Probabilistic Semantics and Verification
- Category Theory

### Linear Dynamical Systems

*On Termination of Integer Linear Loops.*

(with J. Ouaknine and J. Sousa-Pinto)

Submitted 2014

*Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences.*

(with J. Ouaknine)

Proceedings of ICALP 2014 and Track-B best paper award.

*Effecitve Positivity Problems for Simple Linear Recurrence Sequences.*

(with J. Ouaknine)

Proceedings of ICALP 2014.

*Positivity Problems for Low-Order Linear Recurrence Sequences.*

(with J. Ouaknine)

Proceedings of SODA 2014.

*The Orbit Problem in Higher Dimensions.*

(with V. Chonev and J. Ouaknine)

Proceedings of STOC 2013.

### Timed Automata and Metric Temporal Logic

*Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian .*

(with R. Lazic and J. Ouaknine)

Proceedings of MFCS 2013, LNCS 7966, Springer, 2013.

*Expressive Completeness for Metric Temporal Logic.*

(with P. Hunter and J. Ouaknine)

Proceedings of LICS 2013, IEEE Computer Society Press.

*Alternating Timed Automata over Bounded Time.*

(with M. Jenkins, J. Ouaknine and A. Rabinovich)

Proceedings of LICS 10, IEEE Computer Society Press.

*Time-Bounded Verification.*

(with J. Ouaknine)

Proceedings of CONCUR 09, LNCS 5710, Springer, 2009.

*Some recent results in Metric Temporal Logic.*

(with J. Ouaknine)

Proceedings of FORMATS 08, LNCS 5215, Springer, 2008.

*On expressiveness and complexity in real-time model checking.*

(with P. Bouyer, N. Markey, J. Ouaknine)

Proceedings of ICALP 08, LNCS 5126, Springer, 2008.

*The cost of punctuality.*

(with P. Bouyer, N. Markey, J. Ouaknine)

Proceedings of LICS 2007, IEEE Computer Society Press, 2007.

*Zone-based universality analysis for single-clock timed automata.*

(with P. A. Abdulla, J. Ouaknine, K. Quaas)

*Proceedings of FSEN 07*, LNCS 4767, Springer, 2007.

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

(with J. Ouaknine).

In Logical Methods in Computer Science 3(1).

*On Metric Temporal Logic and faulty Turing machines.*

(with J. Ouaknine).

Proceedings of FOSSACS 06, LNCS 3921, Springer, 2006.

*Safety Metric Temporal Logic is fully decidable .*

(with J. Ouaknine).

Proceedings of TACAS 06, LNCS 3920, Springer, 2006.

*Decidability and complexity results for timed automata via channel systems.*

(with P.A. Abdulla, J. Deneux, J. Ouaknine).

Proceedings of ICALP 05, LNCS 3580, Springer, 2005.

*On the decidability of Metric Temporal Logic.*

(with J. Ouaknine).

Proceedings of LICS 2005, IEEE Computer Society Press, 2005.

*On the language inclusion problem for timed automata: Closing a decidability gap .*

(with J. Ouaknine).

Proceedings of LICS 2004, IEEE Computer Society Press, 2004.

*Timed CSP = closed timed epsilon-automata .*

(with J. Ouaknine).

Nordic Journal of Computing, Volume 10, Number 2, 2003.

*Revisiting digitization, robustness and decidability for timed automata.*

(with J. Ouaknine)

Proceedings of LICS 2003, IEEE Computer Society Press, 2003.

*Universality and Language Inclusion for Open and Closed Timed Automata.*

(with J. Ouaknine)

Proceedings of HSCC 03, LNCS 2623, Springer, 2003.

*Timed CSP = closed timed automata*

(with J. Ouaknine).

Proceedings of EXPRESS 02, ENTCS 68(2), 2002.

### Infinite-State Systems and Automata

*Revisiting the Equivalence Problem for Finite Multitape Automata*

Proceedings of ICALP 2013, LNCS 7966, Springer, 2013.

*On Termination and Invariance for Faulty Channel Machines*

(with P. Bouyer, N. Markey, J. Ouaknine and Ph. Schnoebelen).

Formal Aspects of Compututing 24(4-6): 595-607, 2012.

*Reachability for succinct and parametric one-counter automata*

(with C. Haase, S. Kreutzer, J. Ouaknine).

Proceedings of CONCUR 09, LNCS 5710, Springer, 2009.

*On termination for faulty channel machines*

(with P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen).

Proceedings of STACS 08, 2008.

*Nets with tokens which carry data.*

(with R. Lazic, T. Newcomb, J. Ouaknine, A.W. Roscoe).

Proceedings of ICATPN 07, LNCS 4546, Springer, 2007.

### Probabilistic Semantics and Verification

*LTL model checking of Interval Markov Chains.*

(with M. Benedikt and R. Lenhardt)

Proceedings of TACAS 13, LNCS 7795, Springer 2013.

*Three Tokens in Herman's Algorithm.*

(with S. Kiefer, A. Murawski, J. Ouaknine and B. Wachter)

Formal Aspects of Computing 24(4-6):671--678, 2012.

*On the Complexity of Equivalence and Minimisation for Q-Weighted Automata.*

(with S. Kiefer, A. Murawski, J. Ouaknine and B. Wachter)

LMCS Volume 9, Issue 8, 2013.

*On the Complexity of Computing Probabilistic Bisimilarity.*

(with D. Chen and F. van Breugel)

Proceedings of FOSSACS 2012, LNCS 7213, Springer 2012.

*On automated verification of probabilistic programs.*

(with Axel Legay, Andrzej Murawski and Joel Ouaknine)

Proceedings of TACAS 08, LNCS 4963, Springer 2008.

*Labelled Markov processes as generalised stochastic relations.*

(with Dusko Pavlovic and Michael Mislove)

In

*Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin,*ENTCS 172, 2007.

*Approximating a behavioural pseudometric without discount.*

(with Franck van Breugel and Babita Sharma)

Proceeding of FOSSACS 07, LNCS 4423, Springer, 2007.

*Approximating and computing behavioural distances in probabilistic transition systems.*

(with F. van Breugel)

Theoretical Computer Science 360(1-3):373-385, 2006.

*An accessible approach to behavioural pseudometrics.*

(with Franck van Breugel, Claudio Hermida and Michael Makkai).

Proceeding of ICALP 2005, LNCS 3580, Springer, 2005.

*Domain theory, simulation and testing for labelled Markov processes.*

(with Franck Van Breguel, Michael Mislove and Joel Ouaknine)

Theoretical Computer Science 333(1-2): 171--197, 2005

*A behavioural pseudometric for probabilistic transition systems.*

(with Franck van Breugel)

Theoretical Computer Science 331(1):115--142, 2005.

*Duality for Labelled Markov Processes.*

(with Michael Mislove, Joel Ouaknine and Dusko Pavlovic)

Proceedings of FOSSACS 04, LNCS 2987, Springer, 2004.

*Measuring the probabilistic powerdomain.*

(with Keye Martin and Michael Mislove)

Theoretical Computer Science 312(1):99--119, 2004.

*Axioms for probability and nondeterminism.*

(with Michael Mislove and Joel Ouaknine)

Proceedings of EXPRESS 03, ENTCS 91(3), 2003.

*An intrinsic characterization of approximate probabilistic bisimilarity*

(with Franck van Breugel, Mike Mislove and Joel Ouaknine)

Proceedings of FOSSACS 03, LNCS 2620, Springer, 2003.

*Testing labelled Markov processes*

(with F. van Breugel and Steven Shalit)

Proceedings of ICALP 02, LNCS 2380, Springer, 2002.

*Measuring the probabilistic powerdomain*

(with K. Martin and M. Mislove)

Proceedings ICALP 02, LNCS 2380, Springer, 2002.

*Towards quantitative verification of probabilistic transition systems*

(with F. van Breugel)

Proceedings of ICALP 01, LNCS 2076, Springer, 2001.

*An algorithm for quantitative verification of probabilistic transition systems.*

(with F. van Breugel)

Proceedings CONCUR 01, LNCS 2154, Springer, 2001.

### Category Theory and Coalgebra

*On the final sequence of a finitary set functor.*

Theoretical Computer Science 338(1-3): 184--199, 2005.

*A Note on Coalgebras and Presheaves .*

Mathematical Structures in Computer Science, 15:475--483, 2005.

*On the structure of categories of coalgebras*

(with P.T. Johnstone, J. Power, T. Tujishita, H. Watanabe)

Theoretical Computer Science 260:87--117, 2001.

*Coinduction for recursive data types: partial orders, metric spaces and omega-categories.*

Proceedings of CMCS 00, ENTCS 33, April 2000.

*An axiomatics for categories of coalgebras*

(with P.T. Johnstone, J. Power, T. Tujishita, H. Watanabe)

Proceedings of LICS 98, IEEE Computer Society Press, 1998.

*Toposes of coalgebras and hidden algebras*

Proceedings of CMCS 98, ENTCS 11, 1998.

*Last updated in April, 2005, by jbw@mcomlab.ox.ac.uk*