Sougata Bose

GandALF Workshop 2025 Workshop Paper

Generalised Reachability Games Revisited

• Sougata Bose
• Daniel Hausmann
• Soumyajit Paul
• Sven Schewe
• Tansholpan Zhanabekova

Classic reachability games on graphs are zero-sum games, where the goal of one player, Eve, is to visit a vertex from a given target set, and that of other player, Adam, is to prevent this. Generalised reachability games, studied by Fijalkow and Horn, are a generalisation of reachability objectives, where instead of a single target set, there is a family of target sets and Eve must visit all of them in any order. In this work, we further study the complexity of solving two-player games on graphs with generalised reachability objectives. Our results are twofold: first, we provide an improved complexity picture for generalised reachability games, expanding the known tractable class from games in which all target sets are singleton to additionally allowing a logarithmic number of target sets of arbitrary size. Second, we study optimisation variants of generalised reachability with a focus on the size of the target sets. For these problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability in the classic variant for singleton target sets, the optimisation problem is NP-hard when Eve tries to maximise the number of singleton target sets that are visited. Tractability can be recovered in the optimisation setting when all target sets are singleton by requiring that Eve pledges a maximum sized subset of target sets that she can guarantee to visit.

Highlights Conference 2025 Conference Abstract

Solving Concurrent Mean-payoff Games using Limited Memory

• Sougata Bose

Highlights Conference 2023 Conference Abstract

History Deterministic Vector Addition Systems

• Sougata Bose

In this talk, we consider History-determinism, a restricted form of non-determinism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words, both with coverability and reachability acceptance. History-determinism requires that the non-deterministic choices can be resolved on-the-fly; based on the past andwithout jeopardising acceptance of any possible continuation of the input word. Our results show that the history-deterministic (HD) VASS sit strictly between deterministic and non-deterministic VASS. We compare the relative expressiveness of HD systems, and closure-properties of the induced language classes, with coverability and reachability semantics, with or without $\epsilon$ labelled transitions. With two or more counters HD-VASS are essentially able to approximate 2-counter Minsky machines, leading to several undecidability results. It is undecidable whether an VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic $2$-VASS is also undecidable. This talk is based on joint work with Patrick Totzke and David Purser. Contributed talk given by Sougata Bose

Highlights Conference 2021 Conference Abstract

One-way Resynchronizability of Word Transducers

• Sougata Bose

The one-way definability problem for word transducers asks whether a given two-way transducer is equivalent to some one-way transducer. This problem is motivated by the fact that a one-way transducer can process the input one letter at a time, whereas a two-way transducer needs to store the entire input. This problem has been studied in the classical semantics and is undecidable in general, but becomes decidable when restricted to functional transducers. In this talk, we consider a variant of the one-way definability problem in the origin semantics. The origin semantics for transducers was proposed in 2014 by Bojanczyk and led to various decidability results for problems that are undecidable in the classical semantics. We show that it is decidable whether a two-way word transducer is “close” to a one-way transducer in the origin semantics up to some distortions of origins defined by a bounded, regular resynchronizers. We call this the one-way resynchronizability problem and we characterize the class of “one-way resynchronizable” transducers using a property of the runs of the transducer, called “inversions”, and a structural property of the origin graphs produced by the transducer, called “cross-width”. Furthermore, a two-way transducer can be checked for absence of inversions, which also shows that the problem is decidable. This is joint work with Krishna S. , Anca Muscholl, and Gabriele Puppis presented at FoSSaCS 2021.

MFCS Conference 2019 Conference Paper

On Synthesis of Resynchronizers for Transducers

• Sougata Bose
• Shankara Narayanan Krishna
• Anca Muscholl
• Vincent Penelle
• Gabriele Puppis

We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T_1, T_2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T_1 is contained in R(T_2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.