Publications
In my field, authors of publications are usually listed in alphabetical order.Peer-reviewed journal articles
-
The Reactive Synthesis Competition (SYNTCOMP): 2018 – 2021.
International Journal on Software Tools for Technology Transfer, Volume 26, pages 551 –
567,
2023.
[DOI]
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018–2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality—that is, the total size in terms of logic and memory elements—of solutions.
Peer-reviewed conference proceedings
-
Active Learning of Mealy Machines with Timers.
Formal Modeling and Analysis of Timed Systems, FORMATS,
2025.
[arXiv]
We present the first algorithm for query learning Mealy machines with timers in a black-box context. Our algorithm is an extension of the L# algorithm of Vaandrager et al. to a timed setting. We rely on symbolic queries which empower us to reason on untimed executions while learning. Similarly to the algorithm for learning timed automata of Waga, these symbolic queries can be realized using finitely many concrete queries. Experiments with a prototype implementation show that our algorithm is able to efficiently learn realistic benchmarks.
-
Automata with Timers.
Formal Modeling and Analysis of Timed Systems, FORMATS, pages 33 – 49,
2023.
[DOI]
[arXiv]
In this work, we study properties of deterministic finite-state automata with timers, a subclass of timed automata proposed by Vaandrager et al. as a candidate for an efficiently learnable timed model. We first study the complexity of the configuration reachability problem for such automata and establish that it is PSPACE-complete. Then, as simultaneous timeouts (we call these, races) can occur in timed runs of such automata, we study the problem of determining whether it is possible to modify the delays between the actions in a run, in a way to avoid such races. The absence of races is important for modelling purposes and to streamline learning of automata with timers. We provide an effective characterization of when an automaton is race-avoiding and establish that the related decision problem is in 3EXP and PSPACE-hard.
-
Validating Streaming JSON Documents with Learned VPAs.
Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 271 –
289,
2023.
[DOI]
[arXiv]
[Implementation]
We present a new streaming algorithm to validate JSON documents against a set of constraints given as a JSON schema. Among the possible values a JSON document can hold, objects are unordered collections of key-value pairs while arrays are ordered collections of values. We prove that there always exists a visibly pushdown automaton (VPA) that accepts the same set of JSON documents as a JSON schema. Leveraging this result, our approach relies on learning a VPA for the provided schema. As the learned VPA assumes a fixed order on the key-value pairs of the objects, we abstract its transitions in a special kind of graph, and propose an efficient streaming algorithm using the VPA and its graph to decide whether a JSON document is valid for the schema. We evaluate the implementation of our algorithm on a number of random JSON documents, and compare it to the classical validation algorithm.
-
Learning Realtime One-Counter Automata.
Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 244 –
262,
2022.
[DOI]
[Implementation]
[arXiv]
We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.
-
Optimization of Answer Set Programs for Consistent Query Answering by Means of First-Order
Rewriting.
Conference on Information and Knowledge Management, CIKM, pages 25 – 34,
2020.
[DOI]
[Implementation]
Consistent Query Answering (CQA) with respect to primary keys is the following problem. Given a database instance that is possibly inconsistent with respect to its primary key constraints, define a repair as an inclusion-maximal consistent subinstance. Given a Boolean query q, the problem CERTAINTY(q) takes a database instance as input, and asks whether q is true in every repair. For every Boolean conjunctive query q, the complement of CERTAINTY(q) can be straightforwardly implemented in Answer Set Programming (ASP) by means of a generate-and-test approach: first generate a repair, and then test whether it falsifies the query. Theoretical research has recently revealed that for every self-join-free Boolean conjunctive query q, the complexity class of CERTAINTY(q) is one of FO, L-complete, or coNP-complete. Faced with this complexity trichotomy, one can hypothesize that in practice, the full power of generate-and-test is a computational overkill when CERTAINTY(q) is in the low complexity classes FO or L. We investigate part of this hypothesis within the context of ASP, by asking the following question: whenever CERTAINTY(q) is in FO, does a dedicated first-order algorithm exhibit significant performance gains compared to a generic generate-and-test implementation? We first elaborate on the construction of such dedicated first-order algorithms in ASP, and then empirically address this question.
Preprints
-
Antichains for Concurrent Parameterized Games.
2025.
[arXiv]
[Implementation]
Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n).
Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a uniform strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE algorithm is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents.
In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented in C++ these two algorithms, as well as the one initially proposed, and report on their relative performances on various benchmarks.