Drafts/Misc

1. Strategy Complexity of Reachability in Countable Stochastic 2-Player Games
2. Controlling a Random Population is EXPTIME-hard

2022

1. History-deterministic Timed Automata are Not Determinizable
In International Workshop on Reachability Problems (RP), 2022
2. History-deterministic Timed Automata
In International Conference on Concurrency Theory (CONCUR), 2022

2021

1. Transience in Countable MDPs
In International Conference on Concurrency Theory (CONCUR), 2021
2. HyperLTL Satisfiability is $$\Sigma_1^1$$-complete, HyperCTL* Satisfiability is $$\Sigma_1^2$$-complete
In International Symposium on Mathematical Foundations of Computer Science (MFCS), 2021
3. Simple Stochastic Games with Almost Sure Energy-Parity Objectives
In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2021

2020

1. Optimally Resilient Strategies in Pushdown Safety Games
In International Symposium on Mathematical Foundations of Computer Science (MFCS), 2020
2. How to Play in Infinite MDPs (Invited)
In International Colloquium on Automata, Languages and Programming (ICALP), 2020
3. Strategy Complexity of Parity Objectives in Countable MDPs
In International Conference on Concurrency Theory (CONCUR), 2020
4. Parametrized Universality Problems for One-Counter Nets
In International Conference on Concurrency Theory (CONCUR), 2020

2019

1. Timed Basic Parallel Processes
In International Conference on Concurrency Theory (CONCUR), 2019
2. Büchi Objectives in Countable MDPs
In International Colloquium on Automata, Languages and Programming (ICALP), 2019

2018

1. Universal Safety for Timed Petri Nets is PSPACE-complete
In International Conference on Concurrency Theory (CONCUR), 2018

2017

1. MDPs with Energy-Parity Objectives
In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017
2. Linear Combinations of Unordered Data Vectors
In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017

2016

1. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016
2. Coverability Trees for Petri Nets with Unordered Data
In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2016
3. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
In International Colloquium on Automata, Languages and Programming (ICALP), 2016

2015

1. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
In International Colloquium on Automata, Languages and Programming (ICALP), 2015
2. On Boundedness Problems for Pushdown Vector Addition Systems
In International Workshop on Reachability Problems (RP), 2015

2014

1. Trace Inclusion for One-Counter Nets Revisited
In International Workshop on Reachability Problems (RP), 2014
2. Infinite-State Energy Games
In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

1. Simulation Over One-Counter Nets is PSPACE-Complete
In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2013
2. Branching-Time Model Checking Gap-Order Constraint Systems
In International Workshop on Reachability Problems (RP), 2013
3. Decidability of Weak Simulation on One-Counter Nets
In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2013

2012

1. Approximating Weak Bisimilarity of Basic Parallel Processes
In International Workshop on Expressiveness in Concurrency (EXPRESS), 2012

Journal articles

1. The Reachability Problem for Two-Dimensional Vector Addition Systems with States
Journal of the ACM, 2021
2. What Makes Petri Nets Harder to Verify: Stack or Data?
Lecture Notes in Computer Science, 2017
3. Branching-Time Model Checking Gap-Order Constraint Systems
Fundamenta Informaticae, 2016
4. Simulation Problems Over One-Counter Nets
Logical Methods in Computer Science, 2016
5. Trace inclusion for one-counter nets revisited
Theoretical Computer Science, 2017
6. Properties of Multiset Language Classes Defined by Multiset Pushdown Automata
Fundamenta Informaticae, 2009
7. Multiset Pushdown Automata
Fundamenta Informaticae, 2009

Theses

1. Inclusion Problems for One-Counter Systems
University of Edinburgh, 2014
2. Multiset Rewriting – A Formal Language Theoretic Perspective on Concurrent Systems
Universität Hamburg, 2009

Software

All my software tools are accessible through my Github profile. See here for a recent attempt at solving Energy Games. I am the main developer and maintainer of alot, a terminal MUA for the notmuch mail indexer. I also wrote LaTeX beamer themes designed after the websites of the Universities of Edinburgh and Warwick, which I used for some of my talks.