Browsing by Author "Lehaut, Mathieu"

Now showing 1 - 4 of 4

Adding Reconfiguration to Zielonka’s Asynchronous Automata
(Electronic Proceedings in Theoretical Computer Science, EPTCS, 88-102, 2024) Lehaut, Mathieu; Piterman, Nir
We study an extension of Zielonka’s (fixed) asynchronous automata called reconfigurable asynchronous automata where processes can dynamically change who they communicate with. We show that reconfigurable asynchronous automata are not more expressive than fixed asynchronous automata by giving translations from one to the other. However, going from reconfigurable to fixed comes at the cost of disseminating communication (and knowledge) to all processes in the system. We then show that this is unavoidable by describing a language accepted by a reconfigurable automaton such that in every equivalent fixed automaton, every process must either be aware of all communication or be irrelevant.
Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology
(2024) Hausmann, Daniel; Lehaut, Mathieu; Piterman, Nir
We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures.
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
(2024) Hausmann, Daniel; Lehaut, Mathieu; Piterman, Nir
Emerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition naturally gives rise to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as B\"uchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results. We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations.
Synthesis for prefix first-order logic on data words
(2024) Grange, J.; Lehaut, Mathieu
We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.