We study 2-player concurrent stochastic Büchi games
on countable graphs. Two players, Max and Min, seek
respectively to maximize and minimize the probability of
visiting a set of target states infinitely often. We show
that there always exist \(\varepsilon\)-optimal Max
strategies that use just a step counter plus 1 bit of
public memory. This upper bound holds for all countable
graphs, but it is a new result even for the special case of
finite graphs. The upper bound is tight in the sense that
Max strategies that use just a step counter, or just finite
memory, are not sufficient even on finite game graphs.
The upper bound is a consequence of a slightly stronger
new result: \varepsilon-optimal Max strategies for the
combined Büchi and Transience objective require just 1
bit of public memory (but cannot be memoryless). Our proof
techniques also yield a closely related result, that
\varepsilon-optimal Max strategies for the Transience
objective alone (which is only meaningful in infinite
graphs) can be memoryless.
@article{kmst2026a,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={Strategy Complexity of B\"{u}chi and Transience Objectives
in Concurrent Stochastic Games},year={2026},month=sep,journal={Mathematics of Operations Research (MOR)},publisher={Institute for Operations Research and the Management
Sciences (INFORMS)},issn={0364-765X},eissn={1526-5471}}
No good Markov strategies for Büchi objectives in
countable MDPs
We study countably infinite Markov decision processes with
Büchi objectives, which ask to visit a given subset
of states infinitely often. A question left open by T.P.
Hill (1979) is whether there always exist
\(\varepsilon\)-optimal Markov strategies, i.e., strategies
that base decisions only on the current state and on the
clock (the number of steps taken so far). We provide a
negative answer to this question by constructing a
non-trivial counterexample.
@article{kmst2026,title={No good {Markov} strategies for {B{\"u}chi} objectives in
countable {MDPs}},author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},journal={Annals of Operations Research},year={2026},month=may,doi={10.1007/s10479-026-07226-6},url={https://doi.org/10.1007/s10479-026-07226-6},issn={1572-9338},}
We provide a new algebraic technique to solve the
sequential flow problem in polynomial space. The task is to
maximize the flow through a graph where edge capacities can
be changed over time by choosing a sequence of capacity
labelings from a given finite set.
Our method is
based on a novel factorization theorem for finite
semigroups that, applied to a suitable flow semigroup,
allows to derive small witnesses. This generalizes to
multiple in/output vertices, as well as regular
constraints.
@inproceedings{gmt2026a,title={Optimal Sequential Flows},author={Gimbert, Hugo and Mascle, Corto and Totzke, Patrick},year={2026},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},doi={10.4230/LIPIcs.ICALP.2026.98}}
The random population control decision problem asks for
the existence of a controller capable of gathering
almost-surely a whole population of identical finite-state
agents simultaneously in a final state. The controller must
be able to satisfy this requirement however large the
population, provided that it is finite. The problem was
previously known to be decidable and EXPTIME-hard. This
paper tackles the exact complexity: the problem is
EXPTIME-complete.
@inproceedings{gmt2026b,title={Optimally Controlling a Random Population},author={Gimbert, Hugo and Mascle, Corto and Totzke, Patrick},year={2026},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},doi={10.4230/LIPIcs.ICALP.2026.180}}
We study verification problems for history-constrained
systems (HCS), a model of guarded computation that uses
nested systems. An outer system describes the process
architecture in which a sequence of actions represents the
communication between sub-systems through a global bus.
Actions are either permitted or blocked locally by guards;
these guards read and decide based on the sequence of
actions so far in the global bus.
When HCS have
both the outer systems and the local guard controllers
modelled by finite automata, we show they have the same
expressive power as regular languages and finite automata,
but they are exponentially more succinct. We also analyse
games on this model, representing the interaction between
environment and controller, and show that solving such
games is EXPTIME-complete, where the lower bound already
holds for reachability/safety games and the upper bound
holds for any \(ω\)-regular winning condition.
Finally, we consider HCS with guards of greater expressive
power, Vector Addition Systems with States (VASS). We show
that with deterministic coverability-VASS guards the
reachability problem is EXPSPACE-complete, while with
reachability-VASS the problem is undecidable.
@inproceedings{kpst2026,title={History-Constrained Systems},author={Kuijer, Louwe B. and Purser, David and Sinclair-Banks, Henry and Totzke, Patrick},booktitle={Formal Methods},year={2026},}
2025
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL*
is Even Harder
Temporal logics for the specification of
information-flow properties are able to express relations
between multiple executions of a system. The two most
important such logics are HyperLTL and HyperCTL*, which
generalise LTL and CTL* by trace quantification. It is
known that this expressiveness comes at a price, i.e.
satisfiability is undecidable for both logics.
In
this paper we settle the exact complexity of these
problems, showing that both are in fact highly undecidable:
we prove that HyperLTL satisfiability is
\(\Sigma_1^1\)-complete and HyperCTL* satisfiability is
\(\Sigma_1^2\)-complete. These are significant increases
over the previously known lower bounds and the first upper
bounds. To prove \(\Sigma_1^2\)-membership for HyperCTL*,
we prove that every satisfiable HyperCTL* sentence has a
model that is equinumerous to the continuum, the first
upper bound of this kind. We also prove this bound to be
tight. Furthermore, we prove that both countable and
finitely-branching satisfiability for HyperCTL* are as hard
as truth in second-order arithmetic, i.e., still highly
undecidable.
Finally, we show that the membership
problem for every level of the HyperLTL quantifier
alternation hierarchy is \(\Pi_1^1\)-complete.
@article{fktz2025,title={HyperLTL Satisfiability Is Highly Undecidable, HyperCTL*
is Even Harder},author={Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},url={https://lmcs.episciences.org/11608},doi={10.46298/lmcs-21(1:3)2025},journal={Logical Methods in Computer Science },issn={1860-5974},volume={Volume 21, Issue 1},eid={3},year={2025},month=jan,}
History-deterministic automata are those in which
nondeterministic choices can be correctly resolved
stepwise: there is a strategy to select a continuation of a
run given the next input letter so that if the overall
input word admits some accepting run, then the constructed
run is also accepting.
Motivated by checking
qualitative properties in probabilistic verification, we
consider the setting where the resolver strategy can
randomize and only needs to succeed with lower-bounded
probability. We study the expressiveness of such
stochastically-resolvable automata as well as consider the
decision questions of whether a given automaton has this
property. In particular, we show that it is undecidable to
check if a given NFA is \(λ\)-stochastically
resolvable. This problem is decidable for
finitely-ambiguous automata. We also present complexity
upper and lower bounds for several well-studied classes of
automata for which this problem remains decidable.
@inproceedings{ppstty2025,title={{Resolving Nondeterminism by Chance}},author={Paul, Soumyajit and Purser, David and Schewe, Sven and Tang, Qiyi and Totzke, Patrick and Yen, Di-De},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={32:1--32:22},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-389-8},issn={1868-8969},year={2025},volume={348},editor={Bouyer, Patricia and van de Pol, Jaco},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.32},urn={urn:nbn:de:0030-drops-239822},doi={10.4230/LIPIcs.CONCUR.2025.32},month=aug,}
Temporal graphs extend ordinary graphs with discrete
time that affects the availability of edges. We consider
solving games played on temporal graphs where one player
aims to explore the graph, i.e., visit all vertices. The
complexity depends majorly on two factors: the presence of
an adversary and how edge availability is specified.
We demonstrate that on static graphs, where edges are
always available, solving explorability games is just as
hard as solving reachability games. In contrast, on
temporal graphs, the complexity of explorability coincides
with generalized reachability (NP-complete for one-player
and PSPACE- complete for two player games). We further show
that if temporal graphs are given symbolically, even
one-player reachability and thus explorability and
generalized reachability games are PSPACE-hard. For one
player, all these are also solvable in PSPACE and for two
players, they are in PSPACE, EXP and EXP, respectively.
@inproceedings{abt2025,title={{Temporal Explorability Games}},author={Austin, Pete and Bose, Sougata and Mazzocchi, Nicolas and Totzke, Patrick},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={7:1--7:17},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-389-8},issn={1868-8969},year={2025},volume={348},editor={Bouyer, Patricia and van de Pol, Jaco},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.7},urn={urn:nbn:de:0030-drops-239575},doi={10.4230/LIPIcs.CONCUR.2025.7},month=aug,}
Strategy Complexity of Büchi and Transience Objectives
in Concurrent Stochastic Games
We study 2-player concurrent stochastic Büchi games
on countable graphs. Two players, Max and Min, seek
respectively to maximize and minimize the probability of
visiting a set of target states infinitely often. We show
that there always exist \(\varepsilon\)-optimal Max
strategies that use just a step counter plus 1 bit of
public memory. This upper bound holds for all countable
graphs, but it is a new result even for the special case of
finite graphs. The upper bound is tight in the sense that
Max strategies that use just a step counter, or just finite
memory, are not sufficient even on finite game graphs.
The upper bound is a consequence of a slightly stronger
new result: \varepsilon-optimal Max strategies for the
combined Büchi and Transience objective require just 1
bit of public memory (but cannot be memoryless). Our proof
techniques also yield a closely related result, that
\varepsilon-optimal Max strategies for the Transience
objective alone (which is only meaningful in infinite
graphs) can be memoryless.
@inproceedings{kmst2025a,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={Strategy Complexity of B\"{u}chi and Transience Objectives
in Concurrent Stochastic Games},year={2025},month=jul,isbn={9798400719431},publisher={Association for Computing Machinery},address={New York, NY, USA},url={https://doi.org/10.1145/3736252.3742560},doi={10.1145/3736252.3742560},booktitle={ACM Conference on Economics and Computation},pages={390–409},numpages={20},location={Stanford University, Stanford, CA, USA}}
We explore the notion of history-determinism in the
context of timed automata (TA) over infinite timed words.
History-deterministic (HD) automata are those in which
nondeterminism can be resolved on the fly, based on the run
constructed thus far. History-determinism is a robust
property that admits different game-based
characterisations, and HD specifications allow for
game-based verification without an expensive
determinization step.
We show that the class of
timed \(ω\)-languages recognised by HD timed automata
strictly extends that of deterministic ones, and is
strictly included in those recognised by fully
non-deterministic TA.
For non-deterministic timed
automata it is known that universality is already
undecidable for Büchi TA. For history-deterministic TA
with arbitrary parity acceptance, we show that timed
universality, inclusion, and synthesis all remain decidable
and are -complete.
For the subclass of TA with
safety or reachability acceptance, one can decide (in
EXPTIME) whether such an automaton is
history-deterministic. If so, it can effectively
determinized without introducing new automata states.
@article{bhlst2023,title={History-deterministic Timed Automata},author={Bose, Sougata and Henzinger, Thomas A. and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},url={https://lmcs.episciences.org/14429},doi={10.46298/lmcs-20(4:1)2024},journal={Logical Methods in Computer Science },volume={{Volume 20, Issue 4}},year={2024},month=oct,}
Strategy Complexity of Reachability in Countable
Stochastic 2-Player Games
We study countably infinite stochastic 2-player games with
reachability objectives. Our results provide a complete
picture of the memory requirements of
\(\varepsilon\)-optimal (resp. optimal) strategies. These
results depend on whether the game graph is infinitely
branching and on whether one requires strategies that are
uniform (i.e., independent of the start state). Our main
result is that \(\varepsilon\)-optimal (resp. optimal)
Maximizer strategies in infinitely branching turn-based
reachability games require infinite memory. This holds even
under very strong restrictions. Even if all states have an
almost surely winning Maximizer strategy, strategies with a
step counter plus finite private memory are still useless.
Regarding uniformity, we show that for Maximizer there need
not exist positional uniformly \(\varepsilon\)-optimal
strategies even in finitely branching turn-based games,
whereas there always exists one that uses one bit of public
memory, even in concurrent games with finite action sets.
@article{kmst2022,title={Strategy Complexity of Reachability in Countable
Stochastic 2-Player Games},author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},journal={Dynamic Games and Applications},year={2024},month=sep,doi={10.1007/s13235-024-00575-6},}
We study games of infinite duration played on graphs
and focus on the strategy complexity of quantitative
objectives. Such games are known to admit optimal
memoryless strategies over finite graphs, but require
infinite-memory strategies in general over infinite graphs.
We provide new lower and upper bounds for the
strategy complexity of mean-payoff and total-payoff
objectives over infinite graphs, focusing on whether
step-counter strategies (sometimes called Markov
strategies) suffice to implement winning strategies. In
particular, we show that over finitely branching arenas,
three variants of \(\limsup\) mean-payoff and total-payoff
objectives admit winning strategies that are based either
on a step counter or on a step counter and an additional
bit of memory. Conversely, we show that for certain
\(\liminf\) total-payoff objectives, strategies resorting
to a step counter and finite memory are not sufficient. For
step-counter strategies, this settles the case of all
classical quantitative objectives up to the second level of
the Borel hierarchy.
@inproceedings{biptv2024,author={Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},title={{The Power of Counting Steps in Quantitative Games}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={13:1--13:18},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-339-3},issn={1868-8969},year={2024},month=aug,volume={311},editor={Majumdar, Rupak and Silva, Alexandra},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13},urn={urn:nbn:de:0030-drops-207852},doi={10.4230/LIPIcs.CONCUR.2024.13},}
Bounded-Memory Strategies in Partial-Information Games
Sougata
Bose, Rasmus
Ibsen-Jensen, and Patrick
Totzke
In ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2024
We study the computational complexity of solving
stochastic games with mean-payoff objectives. Instead of
identifying special classes in which simple strategies are
sufficient to play \(\varepsilon\)-optimally, or form
\(\varepsilon\)-Nash equilibria, we consider general
partial-information, multiplayer games and ask what can be
achieved with (and against) finite-memory strategies up to
a given bound on the memory.
We show NP-hardness
for approximating zero-sum values, already with respect to
memoryless strategies and for 1-player reachability
games. On the other hand, we provide upper bounds for
solving games of any fixed number of players k. We show
that one can decide in polynomial space if, for a given
k-player game, \(\varepsilon\ge 0 \) and bound b,
there exists an \(\varepsilon\)-Nash equilibrium in which
all strategies use at most b memory modes. For given
\(\varepsilon > 0\), finding an \(\varepsilon\)-Nash
equilibrium with respect to b-bounded strategies can be
done in \(\text{FNP}^{\text{NP}}\). Similarly, for
zero-sum games finding a b-bounded strategy that, against
all b-bounded opponent strategies, guarantees an outcome
within \(\varepsilon\)of a given value, can be done in
\(\text{FNP}^{\text{NP}}\). Our constructions apply
to parity objectiveswith minimal simplifications.
Our results improve the status quo in several well-known
special cases of games. In particular, for 2-player
zero-sum concurrent mean-payoff games, our results imply
that one can approximate ordinary zero-sum values (without
restricting admissible strategies) in \(\text{FNP}^{\text{NP}}\).
@inproceedings{bit2024,title={Bounded-Memory Strategies in Partial-Information Games},author={Bose, Sougata and Ibsen{-}Jensen, Rasmus and Totzke, Patrick},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},doi={10.1145/3661814.3662096},year={2024},month=jul,}
Memoryless Strategies in Stochastic Reachability Games
We study concurrent stochastic reachability games played
on finite graphs. Two players, Max and Min, seek
respectively to maximize and minimize the probability of
reaching a set of target states. We prove that Max has a
memoryless strategy that is optimal from all states that
have an optimal strategy. Our construction provides an
alternative proof of this result by Bordais, Bouyer and Le
Roux, and strengthens it, as we allow Max’s action sets to
be countably infinite.
@inbook{kmst2024,title={Memoryless Strategies in Stochastic Reachability Games},author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},year={2024},month=mar,doi={10.1007/978-3-031-56222-8_13},editor={Kiefer, Stefan and K{\v{r}}et{\'i}nsk{\'y}, Jan and Ku{\v{c}}era, Anton{\'i}n},booktitle={Taming the Infinities of Concurrency},journal={Lecture Notes in Computer Science},publisher={Springer Nature Switzerland},address={Cham},pages={225--242},isbn={978-3-031-56222-8},url={https://doi.org/10.1007/978-3-031-56222-8_13},}
Temporal graphs are a popular modelling mechanism for
dynamic complex systems that extend ordinary graphs with
discrete time. Simply put, time progresses one unit per
step and the availability of edges can change with time.
We consider the complexity of solving
\(ω\)-regular games played on temporal graphs where
the edge availability is ultimately periodic and fixed a
priori.
We show that solving parity games on
temporal graphs is decidable in PSPACE, only assuming the
edge predicate itself is in PSPACE. A matching lower bound
already holds for what we call punctual reachability games
on static graphs, where one player wants to reach the
target at a given, binary encoded, point in time. We
further study syntactic restrictions that imply more
efficient procedures. In particular, if the edge predicate
is in \(P\ \)and is monotonically increasing for one
player and decreasing for the other, then the complexity of
solving games is only polynomially increased compared to
static graphs.
@inproceedings{abt2024,title={Parity Games on Temporal Graphs},author={Austin, Pete and Bose, Sougata and Totzke, Patrick},editor={Kobayashi, Naoki and Worrell, James},booktitle={International Conference on Foundations of Software
Science and Computational Structures (FoSSaCS)},series={Lecture Notes in Computer Science},volume={14574},pages={79--98},publisher={Springer},year={2024},month=apr,url={https://doi.org/10.1007/978-3-031-57228-9\_5},doi={10.1007/978-3-031-57228-9\_5},}
We consider history-determinism, a restricted form of
non-determinism, for Vector Addition Systems with States
(VASS) when used as acceptors to recognise languages of
finite words, both with coverability and reachability
acceptance. History-determinism requires that the
non-deterministic choices can be resolved on-the-fly; based
on the past and without jeopardising acceptance of any
possible continuation of the input word.
Our
results show that the history-deterministic (HD) VASS sit
strictly between deterministic and non-deterministic VASS
regardless of the number of counters. We compare the
relative expressiveness of HD systems, and
closure-properties of the induced language classes, with
coverability and reachability semantics, with and without
silent (\(\varepsilon\)-labelled) transitions.
Whereas in dimension 1, inclusion and regularity remain
decidable, from dimension two onwards, HD-VASS with
suitable resolver strategies, are essentially able to
simulate 2-counter Minsky machines, leading to several
undecidability results: It is undecidable whether an VASS
is history-deterministic, or if a language equivalent
history-deterministic VASS exists. Checking language
inclusion between history-deterministic 2-VASS is also
undecidable.
@inproceedings{bpt2023,title={{History-Deterministic Vector Addition Systems}},author={Bose, Sougata and Purser, David and Totzke, Patrick},booktitle={International Conference on Concurrency Theory (CONCUR)},year={2023},pages={18:1--18:17},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-299-0},issn={1868-8969},volume={279},editor={P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2023/19012},urn={urn:nbn:de:0030-drops-190120},doi={10.4230/LIPIcs.CONCUR.2023.18},}
Writing temporal logic formulae for properties that
combine instantaneous events with overlapping temporal
phenomena of some duration is difficult in classical
temporal logics. To address this issue, in previous work we
introduced a new temporal logic with intuitive temporal
modalities specifically tailored for the representation of
both instantaneous and durative phenomena. We also provided
an implementation of a complex event processing system,
Phenesthe, based on this logic, that has been applied and
tested on a real maritime surveillance scenario.
In this work, we extend our temporal logic with two extra
modalities to increase its expressive power for handling
future formulae. We compare the expressive power of
different fragments of our logic with Linear Temporal Logic
and dyadic first-order logic. Furthermore, we define
correctness criteria for stream processors that use our
language. Last but not least, we evaluate empirically the
performance of Phenesthe+, our extended implementation, and
show that the increased expressive power does not affect
efficiency significantly.
@inproceedings{plt2023,author={Pitsikalis, Manolis and Lisitsa, Alexei and Totzke, Patrick and Lee, Simon},booktitle={International Symposium on Games, Automata, Logics, and
Formal Verification (GandALF)},title={Handling of Past and Future with Phenesthe+},year={2023},}
2022
History-deterministic Timed Automata are Not
Determinizable
An automaton is history-deterministic (HD) if one can
safely resolve its non-deterministic choices on the fly. In
a recent paper, Henzinger, Lehtinen and Totzke studied this
in the context of Timed Automata, where it was conjectured
that the class of timed ω-languages recognised by
HD-timed automata strictly extends that of deterministic
ones.
We provide a proof for this fact.
@inproceedings{bhlst2022,title={History-deterministic Timed Automata are Not
Determinizable},author={Bose, Sougata and Henzinger, Thomas A. and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},year={2022},booktitle={International Workshop on Reachability Problems (RP)},}
We explore the notion of history-determinism in the
context of timed automata (TA). History-deterministic
automata are those in which nondeterminism can be resolved
on the fly, based on the run constructed thus far.
History-determinism is a robust property that admits
different game-based characterisations, and
history-deterministic specifications allow for game-based
verification without an expensive determinization step.
We show yet another characterisation of
history-determinism in terms of fair simulation, at the
general level of labelled transition systems: a system is
history-deterministic precisely if and only if it fairly
simulates all language smaller systems.
For timed
automata over infinite timed words it is known that
universality is undecidable for Büchi TA. We show that
for history-deterministic TA with arbitrary parity
acceptance, timed universality, inclusion, and synthesis
all remain decidable and are EXPTIME-complete.
For
the subclass of TA with safety or reachability acceptance,
we show that checking whether such an automaton is
history-deterministic is decidable (in EXPTIME), and
history-deterministic TA with safety acceptance are
effectively determinizable without introducing new states.
@inproceedings{hlt2022,booktitle={International Conference on Concurrency Theory (CONCUR)},title={History-deterministic Timed Automata},author={Henzinger, Thomas A. and Lehtinen, Karoliina and Totzke, Patrick},year={2022},}
While an abundance of real-time maritime information
exists and is readily available to monitoring authorities,
there are still many instances in which ships are found to
be engaged in dangerous or illegal activities. In order to
prevent such activities, authorities employ Vessel Traffic
Services systems since they promote safety at sea while
also assisting in management of ports. In this paper we
report on research done in cooperation with Denbridge
Marine Ltd., a global provider of maritime solutions, and
present an application integrated in a Vessel Tracking
Services system that allows the detection of normal vessel
activity as well as dangerous or illegal situations in
real-time, using information from the Automatic
Identification System, a radar sensor and other
information.
We use a set of phenomena
representing maritime activities of interest in the
language of Phenesthe, our Complex Event Processing engine,
and detect them on real maritime data streams from the area
of Liverpool, United Kingdom. We evaluate our application
and show that our system is capable of detecting and
visualising maritime activities on the map in real time.
Finally, we study and demonstrate the significance of using
data from the Automatic Identification System along with
radar data for maritime monitoring.
@inproceedings{plt2022,author={Pitsikalis, Manolis and Lisitsa, Alexei and Totzke, Patrick and Lee, Simon},booktitle={International Conference on Mobile Data Management (MDM)},title={Making Sense of Heterogeneous Maritime Data},year={2022},volume={},number={},pages={401-406},doi={10.1109/MDM55031.2022.00089},}
2021
The Reachability Problem for Two-Dimensional Vector
Addition Systems with States
We prove that the reachability problem for two-dimensional
vector addition systems with states is NL-complete or
PSPACE-complete, depending on whether the numbers in the
input are encoded in unary or binary. As a key underlying
technical result, we show that, if a configuration is
reachable, then there exists a witnessing path whose
sequence of transitions is contained in a bounded language
defined by a regular expression of pseudo-polynomially
bounded length. This, in turn, enables us to prove that the
lengths of minimal reachability witnesses are
pseudo-polynomially bounded.
@article{befghlmt2021,author={Blondin, Michael and Englert, Matthias and Finkel, Alain and Göller, Stefan and Haase, Christoph and Lazi\'{c}, Ranko and Mckenzie, Pierre and Totzke, Patrick},title={The Reachability Problem for Two-Dimensional Vector
Addition Systems with States},year={2021},issue_date={October 2021},publisher={Association for Computing Machinery},address={New York, NY, USA},volume={68},number={5},issn={0004-5411},url={https://doi.org/10.1145/3464794},doi={10.1145/3464794},journal={Journal of the {ACM}},month=aug,articleno={34},numpages={43},}
The Transient objective is not to visit any state
infinitely often. While this is not possible in any finite
Markov Decision Process (MDP), it can be satisfied in
countably infinite ones, e.g., if the transition graph is
acyclic.
We prove the following fundamental properties of
Transient in countably infinite MDPs.
There exist uniformly \(\varepsilon\)-optimal MD
strategies (memoryless deterministic) for Transient, even
in infinitely branching MDPs.
Optimal strategies
for Transient need not exist, even if the MDP is finitely
branching. However, if an optimal strategy exists then
there is also an optimal MD strategy.
If an MDP is
universally transient (i.e., almost surely transient under
all strategies) then many other objectives have a lower
strategy complexity than in general MDPs. E.g.,
\(\varepsilon\)-optimal strategies for Safety and
co-Büchi and optimal strategies for
\(\{0,1,2\}\)-Parity (where they exist) can be chosen MD,
even if the MDP is infinitely branching.
@inproceedings{kmst2021,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={{Transience in Countable MDPs}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={11:1--11:15},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-203-7},issn={1868-8969},year={2021},volume={203},editor={Haddad, Serge and Varacca, Daniele},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2021/14388},urn={urn:nbn:de:0030-drops-143881},doi={10.4230/LIPIcs.CONCUR.2021.11},teaser={https://stream.liv.ac.uk/xrvdpjs5},}
HyperLTL Satisfiability is \(\Sigma_1^1\)-complete,
HyperCTL* Satisfiability is \(\Sigma_1^2\)-complete
Temporal logics for the specification of information-flow
properties are able to express relations between multiple
executions of a system. The two most important such logics
are HyperLTL and HyperCTL*, which generalise LTL and CTL*
by trace quantification. It is known that this
expressiveness comes at a price, i.e. satisfiability is
undecidable for both logics.
In this paper we settle the exact complexity of these
problems, showing that both are in fact highly undecidable:
we prove that HyperLTL satisfiability is
\(\Sigma_1^1\)-complete and HyperCTL* satisfiability is
\(\Sigma_1^2\)-complete. These are significant increases
over the previously known lower bounds and the first upper
bounds. To prove \(\Sigma_1^2\)-membership for HyperCTL*,
we prove that every satisfiable HyperCTL* sentence has a
model that is equinumerous to the continuum, the first
upper bound of this kind. We prove this bound to be tight.
Finally, we show that the membership problem for every
level of the HyperLTL quantifier alternation hierarchy is
\(\Pi_1^1\)-complete.
@inproceedings{fktz2021,author={Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},title={{HyperLTL Satisfiability is \(\Sigma_1^1\)-complete,
HyperCTL* Satisfiability is \(\Sigma_1^2\)-complete}},booktitle={International Symposium on Mathematical Foundations of
Computer Science (MFCS)},pages={47:1--47:19},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-201-3},issn={1868-8969},year={2021},volume={202},editor={Bonchi, Filippo and Puglisi, Simon J.},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2021/14487},urn={urn:nbn:de:0030-drops-144870},doi={10.4230/LIPIcs.MFCS.2021.47},}
Simple Stochastic Games with Almost Sure Energy-Parity
Objectives
We study stochastic games with energy-parity objectives,
which combine quantitative rewards with a qualitative
ω-regular condition: The maximizer aims to avoid running
out of energy while simultaneously satisfying a parity
condition. We show that the corresponding almost-sure
problem, i.e., checking whether there exists a maximizer
strategy that achieves the energy-parity objective with
probability 1 when starting at a given energy level k, is
decidable and in NP∩coNP. The same holds for checking if
such a k exists and if a given k is minimal.
@inproceedings{mstw2021,author={Mayr, Richard and Schewe, Sven and Totzke, Patrick and Wojtczak, Dominik},title={{Simple Stochastic Games with Almost Sure Energy-Parity
Objectives}},booktitle={International Conference on Foundations of Software
Science and Computational Structures (FoSSaCS)},year={2021},}
2020
Optimally Resilient Strategies in Pushdown Safety
Games
@inproceedings{ntz2020,author={Neider, Daniel and Totzke, Patrick and Zimmermann, Martin},title={{Optimally Resilient Strategies in Pushdown Safety
Games}},booktitle={International Symposium on Mathematical Foundations of
Computer Science (MFCS)},pages={74:1--74:15},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-159-7},issn={1868-8969},year={2020},volume={170},editor={Esparza, Javier and Kr{\'a}ľ, Daniel},publisher={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2020/12743},doi={10.4230/LIPIcs.MFCS.2020.74},}
@inproceedings{kmst2020,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick and Wojtczak, Dominik},title={{How to Play in Infinite MDPs (Invited)}},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},pages={3:1--3:18},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-138-2},issn={1868-8969},year={2020},volume={168},editor={Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},publisher={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2020/12410},doi={10.4230/LIPIcs.ICALP.2020.3},}
Strategy Complexity of Parity Objectives in Countable
MDPs
@inproceedings{kmst2020a,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={{Strategy Complexity of Parity Objectives in Countable
MDPs}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={39:1--39:17},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-160-3},issn={1868-8969},year={2020},volume={171},editor={Konnov, Igor and Kov{\'a}cs, Laura},publisher={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2020/12851},doi={10.4230/LIPIcs.CONCUR.2020.39},}
Parametrized Universality Problems for One-Counter
Nets
We study the language universality problem for
One-Counter Nets, also known as 1-dimensional Vector
Addition Systems with States (1-VASS), parameterized either
with an initial counter value, or with an upper bound on
the allowed counter value during runs. The language
accepted by an OCN (defined by reaching a final control
state) is monotone in both parameters. This yields two
natural questions: 1) does there exist an initial counter
value that makes the language universal? 2) does there
exist a sufficiently high ceiling so that the bounded
language is universal?
Although the ordinary
universality problem is decidable (and Ackermann-complete)
and these parameterized variants seem to reduce to checking
basic structural properties of the underlying automaton, we
show that in fact both problems are undecidable. We also
look into the complexities of the problems for several
decidable subclasses, namely for unambiguous, and
deterministic systems, and for those over a single-letter
alphabet.
@inproceedings{abht2020,author={Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},title={{Parametrized Universality Problems for One-Counter
Nets}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={47:1--47:16},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-160-3},issn={1868-8969},year={2020},volume={171},editor={Konnov, Igor and Kov{\'a}cs, Laura},publisher={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/opus/volltexte/2020/12859},doi={10.4230/LIPIcs.CONCUR.2020.47},teaser={ https://www.youtube.com/watch?v=ZIU0Ocdb7vs},}
Bertrand et al. (LMCS 2019) describe two-player
zero-sum games in which one player tries to achieve a
reachability objective in n games (on the same finite
arena) simultaneously by broadcasting actions, and where
the opponent has full control of resolving
non-deterministic choices. They show EXPTIME completeness
for the question if such games can be won for every number
n of games.
We consider the almost-sure variant in
which the opponent randomizes their actions, and where the
player tries to achieve the reachability objective
eventually with probability one. The lower bound
construction in [1] does not directly carry over to this
randomized setting. In this note we show EXPTIME hardness
for the almost-sure problem by reduction from Countdown
Games.
@misc{mst2019,title={Controlling a Random Population is EXPTIME-hard},author={Mascle, Corto and Shirmohammadi, Mahsa and Totzke, Patrick},year={2019},}
@inproceedings{cht2019,author={Clemente, Lorenzo and Hofman, Piotr and Totzke, Patrick},title={Timed Basic Parallel Processes},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={15:1--15:16},year={2019},url={https://doi.org/10.4230/LIPIcs.CONCUR.2019.15},doi={10.4230/LIPIcs.CONCUR.2019.15},}
@inproceedings{kmst2019,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={B{\"{u}}chi Objectives in Countable MDPs},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},year={2019},pages={119:1--119:14},publisher={Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH,
Wadern/Saarbruecken, Germany},copyright={Creative Commons Attribution 3.0 Unported license (CC-BY
3.0)},doi={10.4230/LIPIcs.ICALP.2019.119},language={en},url={https://drops.dagstuhl.de/opus/volltexte/2019/10695/pdf/LIPIcs-ICALP-2019-119.pdf},}
2018
Universal Safety for Timed Petri Nets is
PSPACE-complete
@inproceedings{aacmt2018,author={Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Ciobanu, Radu and Mayr, Richard and Totzke, Patrick},title={{Universal Safety for Timed Petri Nets is
PSPACE-complete}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={6:1--6:15},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-087-3},issn={1868-8969},year={2018},volume={118},url={http://drops.dagstuhl.de/opus/volltexte/2018/9544},doi={10.4230/LIPIcs.CONCUR.2018.6},}
2017
What Makes Petri Nets Harder to Verify: Stack or Data?
@inbook{lt2017,author={Lazi{\'c}, Ranko and Totzke, Patrick},title={{What Makes Petri Nets Harder to Verify: Stack or Data?}},editor={Gibson-Robinson, Thomas and Hopcroft, Philippa and Lazi{\'{c}}, Ranko},booktitle={Concurrency, Security, and Puzzles},publisher={Springer International Publishing},address={Cham},journal={Lecture Notes in Computer Science},volume={10160},number={1},pages={144--161},year={2017},doi={10.1007/978-3-319-51046-0_8},}
@article{ht2017,title={Trace inclusion for one-counter nets revisited },journal={Theoretical Computer Science},volume={11174},year={2017},issn={0304-3975},doi={10.1016/j.tcs.2017.05.009},url={http://www.sciencedirect.com/science/article/pii/S0304397517303961},author={Hofman, Piotr and Totzke, Patrick},}
@inproceedings{mstw2017,author={Mayr, Richard and Schewe, Sven and Totzke, Patrick and Wojtczak, Dominik},title={{MDPs with Energy-Parity Objectives}},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},doi={10.1109/LICS.2017.8005131},year={2017},}
@inproceedings{hlt2017,author={Hofman, Piotr and Leroux, J{\'e}r{\o}me and Totzke, Patrick},title={ Linear Combinations of Unordered Data Vectors },booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},year={2017},}
2016
Branching-Time Model Checking Gap-Order Constraint
Systems
@article{mt2016,author={Mayr, Richard and Totzke, Patrick},title={Branching-Time Model Checking Gap-Order Constraint
Systems},journal={Fundamenta Informaticae},volume={143},number={3-4},pages={339--353},year={2016},doi={10.3233/FI-2016-1317},}
@article{hlmt2016,author={Hofman, Piotr and Lasota, Slawomir and Mayr, Richard and Totzke, Patrick},title={Simulation Problems Over One-Counter Nets},journal={Logical Methods in Computer Science },volume={12},number={1},year={2016},doi={10.2168/LMCS-12(1:6)2016},}
Reachability in Two-Dimensional Unary Vector Addition
Systems with States is NL-Complete
@inproceedings{elt2016,author={Englert, Matthias and Lazi{\'c}, Ranko and Totzke, Patrick},title={Reachability in Two-Dimensional Unary Vector Addition
Systems with States is NL-Complete},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},year={2016},}
Coverability Trees for Petri Nets with Unordered Data
@inproceedings{hlllst2016,title={{Coverability Trees for Petri Nets with Unordered Data}},author={Hofman, Piotr and Lasota, Slawomir and Lazi{\'c}, Ranko and Leroux, J{\'e}r{\o}me and Schmitz, Sylvain and Totzke, Patrick},url={https://hal.inria.fr/hal-01252674},booktitle={International Conference on Foundations of Software
Science and Computational Structures (FoSSaCS)},year={2016},}
A Polynomial-Time Algorithm for Reachability in Branching
VASS in Dimension One
@inproceedings{ghlt2016,author={G{\"{o}}ller, Stefan and Haase, Christoph and Lazi{\'c}, Ranko and Totzke, Patrick},title={A Polynomial-Time Algorithm for Reachability in Branching
{VASS} in Dimension One},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},year={2016},doi={10.4230/LIPIcs.ICALP.2016.105},}
2015
On the Coverability Problem for Pushdown Vector Addition
Systems in One Dimension
@inproceedings{lst2015,author={Leroux, J{\'{e}}r{\{o}}me and Sutre, Gr{\'{e}}goire and Totzke, Patrick},title={On the Coverability Problem for Pushdown Vector Addition
Systems in One Dimension},booktitle={International Colloquium on Automata, Languages and
Programming (ICALP)},year={2015},url={http://dx.doi.org/10.1007/978-3-662-47666-6_26},series={Lecture Notes in Computer Science},volume={9135},pages={324--336},publisher={Springer},doi={10.1007/978-3-662-47666-6_26},}
On Boundedness Problems for Pushdown Vector Addition
Systems
@inproceedings{lst2015a,author={Leroux, J{\'{e}}r{\{o}}me and Sutre, Gr{\'{e}}goire and Totzke, Patrick},title={On Boundedness Problems for Pushdown Vector Addition
Systems},year={2015},booktitle={International Workshop on Reachability Problems (RP)},editor={Bojanczyk, Mikolaj and Lasota, Slawomir and Potapov, Igor},series={Lecture Notes in Computer Science},volume={9328},pages={101--113},publisher={Springer},url={https://doi.org/10.1007/978-3-319-24537-9\_10},doi={10.1007/978-3-319-24537-9\_10},}
@inproceedings{ht2014,author={Hofman, Piotr and Totzke, Patrick},title={Trace Inclusion for One-Counter Nets Revisited},year={2014},booktitle={International Workshop on Reachability Problems (RP)},}
@inproceedings{aahmkt2014,title={Infinite-State Energy Games},author={Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Hofman, Piotr and Mayr, Richard and Kumar, K.~Narayan and Totzke, Patrick},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},year={2014},doi={10.1145/2603088.2603100},}
@phdthesis{t2014,author={Totzke, Patrick},school={University of Edinburgh},title={{Inclusion Problems for One-Counter Systems}},month=apr,year={2014},}
2013
Simulation Over One-Counter Nets is PSPACE-Complete
@inproceedings{hlmt2013,title={Simulation Over One-Counter Nets is {PSPACE}-Complete},author={Hofman, Piotr and Lasota, S{\l}awomir and Mayr, Richard and Totzke, Patrick},booktitle={IARCS Annual Conference on Foundations of Software
Technology and Theoretical Computer Science (FSTTCS)},year={2013},month=dec,}
Branching-Time Model Checking Gap-Order Constraint
Systems
@inproceedings{mt2013,title={Branching-Time Model Checking Gap-Order Constraint
Systems},author={Mayr, Richard and Totzke, Patrick},booktitle={International Workshop on Reachability Problems (RP)},year={2013},month=nov,}
Decidability of Weak Simulation on One-Counter Nets
@inproceedings{hmt2013,title={Decidability of Weak Simulation on One-Counter Nets},author={Hofman, Piotr and Mayr, Richard and Totzke, Patrick},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},year={2013},month=feb,doi={10.1109/LICS.2013.26},}
2012
Approximating Weak Bisimilarity of Basic Parallel
Processes
@inproceedings{ht2012,title={Approximating Weak Bisimilarity of Basic Parallel
Processes},author={Hofman, Piotr and Totzke, Patrick},booktitle={International Workshop on Expressiveness in Concurrency
(EXPRESS)},year={2012},month=sep,doi={10.4204/EPTCS.89.8},}
2009
Properties of Multiset Language Classes Defined by
Multiset Pushdown Automata
@article{ktz09a,author={Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},title={Properties of Multiset Language Classes Defined by
Multiset Pushdown Automata},journal={Fundamenta Informaticae},volume={93},number={(1-3)},pages={235--244},year={2009},}
@article{ktz2009,author={Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},title={Multiset Pushdown Automata},journal={Fundamenta Informaticae},year={2009},volume={93},number={(1-3)},pages={221--233},}
Multiset Rewriting – A Formal Language Theoretic
Perspective on Concurrent Systems
@mastersthesis{t2009,author={Totzke, Patrick},school={Universit{\"a}t Hamburg},title={{Multiset Rewriting -- A Formal Language Theoretic
Perspective on Concurrent Systems}},month=oct,year={2009},}