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 AutomataProceedings 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