Ayrat Khalimov

Highlights Conference 2025 Conference Abstract

Translation from LTL to COCOA without Detours

• Ayrat Khalimov

Highlights Conference 2023 Conference Abstract

Fully Generalized Reactivity (1) Synthesis

• Ayrat Khalimov

Recently Ehlers&Schewe proposed a canonical minimal representation foromega-regular languages [1]. The representation consists of a canonical chainof co-Büchi languages (COCOA): A1 ⊃ A2 ⊃. .. ⊃ An, where each Ai is expressibleby a good-for-games co-Büchi automaton, canonical and minimal by the work ofAbu Radi and Kupferman [2]. This work presents a first application of the newrepresentation, to the problem of reactive synthesis. In reactive synthesis wewant to automatically construct a transducer from a specification in e. g. linear temporal logic. The flow of our construction is: translate a given LTLinto a parity automaton and into COCOA using [1, 2], then we construct amu-calculus fixpoint formula which is evaluated on a game graph of thesynthesis problem. The resulting procedure generalizes the widely knownGeneralized Reactivity (1) synthesis approach to full LTL while inheriting itsefficiency advantages on the original specification class. This is a joint work with Rüdiger Ehlers (main contributor). [1]: Natural Colors of Infinite Words, by Rüdiger Ehlers and Sven Schewe[2]: Minimization and Canonization of GFG Transition-Based Automata, by Bader {Abu Radi} and Orna Kupferman Contributed talk given by Ayrat Khalimov

Highlights Conference 2021 Conference Abstract

Transducer Synthesis from Universal Register Automata in (N, ≤)

• Ayrat Khalimov

This presentation concerns the problem of reactive synthesis of systems interacting with its environment via letters from an infinite data domain. Register automata and transducers are popular formalisms for specifying and modeling such systems. They extend finite-state automata by introducing registers that are used to store data and to test incoming data against the stored one. Unlike the standard automata, the expressive power of register automata depends on whether they are deterministic, non-deterministic, or universal. Among these, universal register automata suit synthesis best as they can specify request-grant properties and allow for succinct conjunction. Because the synthesis problem from universal register automata is undecidable, researchers studied a decidable variant, called register-bounded synthesis, where additionally a bound on the number of registers in a sought transducer is given. In those synthesis works, however, automata can only compare data for equality, which limits synthesis applications. In this paper, we extend register-bounded synthesis to domains with the linear order ≤ in a nondense domain. To this end, we prove a key Pumping Lemma for so-called constraint sequences—those finitely abstract behaviours of register automata. The Pumping Lemma allows us to reduce synthesis of register transducers to synthesis of classical (register-less) transducers. As a result, we show that register-bounded synthesis from universal register automata over domain (N, ≤) is decidable in 2ExpTime as in the equality-only case, giving the order for free.

Highlights Conference 2020 Conference Abstract

Register Games on Infinite Ordered Data Domains

• Ayrat Khalimov

We introduce two-player turn-based zero-sum register games on an infinite linearly ordered data domain. Register games have a finite set of registers intended to store data values. At each round, Adam picks some data in the domain, which is tested against the data contained in the registers, using the linear order. Depending on which test holds (exactly one is required), Eve decides to assign the data to some of her registers, and the game deterministically evolves to a successor vertex depending on her assignment choice. Eve wins the game if she has a strategy, which depends only on the tests and not on the concrete data values, such that whichever values Adam provides, the sequence of visited game vertices satisfies a given parity condition. We show the decidability of register games over data domains N and Q. In both data domains, they can be solved in ExpTime and finite-memory strategies suffice to win. We apply these results to solve the synthesis problem of strategies resolving non-determinism in (non-deterministic) register transducers on data words.