40 citations · 92 across the 18 of their papers we have counts for
26 papers
Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory
Luca Aceto, Antonis Achilleos, Duncan Paul Attard +4
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its executio…
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as pr…
Mostowski Index via extended register games
Olivier Idir, Karoliina Lehtinen
The parity index problem of tree automata asks, given a regular tree language L, what is the least number of priorities of a nondeterministic parity tree automaton that recognises…
History-Determinism vs Fair Simulation
Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen +1
An automaton is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracte…
From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History) Determinism
Antonio Casares, Thomas Colcombet, Nathanaël Fijalkow +1
We study transformations of automata and games using Muller conditions into equivalent ones using parity or Rabin conditions. We present two transformations, one that turns a deter…
History-deterministic Timed Automata
Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen +2
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…
History-deterministic Parikh Automata
Enzo Erlich, Mario Grobler, Shibashis Guha +3
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable…
Parikh Automata over Infinite Words
Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen +1
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable alg…
On the size of good-for-games Rabin automata and its link with the memory in Muller games
Antonio Casares, Thomas Colcombet, Karoliina Lehtinen
In this paper, we look at good-for-games Rabin automata that recognise a Muller language (a language that is entirely characterised by the set of letters that appear infinitely oft…
On the Translation of Automata to Linear Temporal Logic
Udi Boker, Karoliina Lehtinen, Salomon Sickert
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LT…
History Determinism vs. Good for Gameness in Quantitative Automata
Udi Boker, Karoliina Lehtinen
Automata models between determinism and nondeterminism/alternations can retain some of the algorithmic properties of deterministic automata while enjoying some of the expressivenes…
Token Games and History-Deterministic Quantitative-Automata
Udi Boker, Karoliina Lehtinen
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional…
A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct
Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen +1
We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved…
A Recursive Approach to Solving Parity Games in Quasipolynomial Time
Karoliina Lehtinen, Paweł Parys, Sven Schewe +1
Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, whil…
On the Succinctness of Alternating Parity Good-for-Games Automata
Udi Boker, Denis Kuperberg, Karoliina Lehtinen +1
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, wit…
On Succinctness and Recognisability of Alternating Good-for-Games Automata
Udi Boker, Denis Kuperberg, Karoliina Lehtinen +1
We study alternating good-for-games (GFG) automata, i.e., alternating automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge…
Good-for-games -Pushdown Automata
Karoliina Lehtinen, Martin Zimmermann
We introduce good-for-games -pushdown automata (-GFG-PDA). These are automata whose nondeterminism can be resolved based on the input processed so far. Good-for-gameness enab…
Good for Games Automata: From Nondeterminism to Alternation
Udi Boker, Karoliina Lehtinen
A word automaton recognizing a language is good for games (GFG) if its composition with any game with winning condition preserves the game's winner. While all deterministic…
An Operational Guide to Monitorability
Luca Aceto, Antonis Achilleos, Adrian Francalanza +2
Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided…
Improving the complexity of Parys' recursive algorithm
Karoliina Lehtinen, Sven Schewe, Dominik Wojtczak
Parys has recently proposed a quasi-polynomial version of Zielonka's recursive algorithm for solving parity games. In this brief note we suggest a variation of his algorithm that i…
The Cost of Monitoring Alone
Luca Aceto, Antonis Achilleos, Adrian Francalanza +2
We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equ…
Register Games
Karoliina Lehtinen, Udi Boker
The complexity of parity games is a long standing open problem that saw a major breakthrough in 2017 when two quasi-polynomial algorithms were published. This article presents a th…
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza +2
This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal -calculus. It investigat…
The Descriptive Complexity of Modal Model-checking Games
Karoliina Lehtinen
This paper revisits the well-established relationship between the modal mu calculus and parity games to show that it is even more robust than previously known. It addresses the que…