4 citations · 8 across the 11 of their papers we have counts for
19 papers
Population Protocols over Ordered Agents
Michael Blondin, Michaël Cadilhac, Benjamin Courchesne +3
Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according…
The complexity of downward closures of indexed languages
Richard Mandel, Corto Mascle, Georg Zetzsche
Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precise…
Optimal Sequential Flows
Hugo Gimbert, Corto Mascle, Patrick Totzke
We provide a new algebraic technique to solve the sequential flow problem in polynomial space. The task is to maximise the flow through a graph where edge capacities can be changed…
Reach together: How populations win repeated games
Nathalie Bertrand, Patricia Bouyer, Luc Lapointe +1
In repeated games, players choose actions concurrently at each step. We consider a parameterized setting of repeated games in which the players form a population of an arbitrary si…
Optimally Controlling a Random Population
Hugo Gimbert, Corto Mascle, Patrick Totzke
The population control problem is a parameterised problem where a controller sends messages to a whole population of identical finite-state agents, aiming to eventually move them a…
On the Minimisation of Deterministic and History-Deterministic Generalised (co)Büchi Automata
Antonio Casares, Olivier Idir, Denis Kuperberg +2
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBü…
Verification of Population Protocols with Unordered Data
Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer +3
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they dec…
The Complexity of Simplifying -Automata through the Alternating Cycle Decomposition
Antonio Casares, Corto Mascle
In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller into parity automata and…
Learning temporal formulas from examples is hard
Corto Mascle, Nathanaël Fijalkow, Guillaume Lagarde
We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a w…
Model-checking parametric lock-sharing systems against regular constraints
Corto Mascle, Anca Muscholl, Igor Walukiewicz
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. W…
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
Lucie Guillou, Corto Mascle, Nicolas Waldburger
We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is…
Model-checking lock-sharing systems against regular constraints
Corto Mascle
We study the verification of distributed systems where processes are finite automata with access to a shared pool of locks. We consider objectives that are boolean combinations of…
Distributed controller synthesis for deadlock avoidance
Hugo Gimbert, Corto Mascle, Anca Muscholl +1
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction…
Keyboards as a new model of computation
Yoan Géran, Bastien Laboureix, Corto Mascle +1
We introduce a new formalisation of languages, called keyboards. We consider a set of elementary operations (writing/erasing a letter, going to the right or to the left,...) and we…
Responsibility and verification: Importance value in temporal logics
Corto Mascle, Christel Baier, Florian Funke +2
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley…
Controlling a Random Population is EXPTIME-hard
Corto Mascle, Mahsa Shirmohammadi, Patrick Totzke
Bertrand et al. [1] (LMCS 2019) describe two-player zero-sum games in which one player tries to achieve a reachability objective in games (on the same finite arena) simultaneou…
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
Corto Mascle, Martin Zimmermann
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-cri…
On Nonnegative Integer Matrices and Short Killing Words
Stefan Kiefer, Corto Mascle
Let be a natural number and a set of -matrices over the nonnegative integers such that the joint spectral radius of is at most one. We s…
From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
Corto Mascle, Daniel Neider, Maximilian Schwenger +3
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an…