arXiv subjects

Shibashis Guha

Publications and source records attributed to Shibashis Guha.

At least 19 recordsLinked to original sources

arXiv2026

Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes

Given rationals $\alpha$ and $\beta$, the sure-almost-sure problem for a threshold Boolean objective $\varphi$ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have $\varphi$-value at least $\alpha$ (i.e. sure $\alpha$ satisfaction) and with probability $1$ the outcome has $\varphi$-value at least $\beta$ (i.e. almost-sure $\beta$ satisfaction). The sure-limit-sure problem asks if for all $\varepsilon > 0$ one can simultaneously ensure that all outcomes have $\varphi$-value at least $\alpha$ and with probability at least $1 - \varepsilon$ the outcome has $\varphi$-value at least $\beta$. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this. In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that eventually, from every point in the infinite run, the average payoff becomes greater than a given threshold within a finite window length. We study two variants of window mean payoff: in the fixed variant, the window length $\ell$ is given, while in the bounded variant, the length is not given but is required to be bounded throughout the run. We show that the sure-almost-sure problem and the sure-limit-sure problem are both in P for the fixed variant (if $\ell$ is given in unary) and are both in NP $\cap$ coNP for the bounded variant, matching the computational complexity of sure satisfaction and almost-sure satisfaction when considered separately for these objectives. We also give bounds for the memory requirement of winning strategies for all considered problems.

cs.GT↗

arXiv2026

Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

We extend the two-variable logic on data words with guarded regular binary predicates of the form $\widetilde{L}(x,y)$ that is true if positions $x$ and $y$ are in the same class and the factor strictly between $x$ and $y$ is in the regular language $L$. We characterise the class of monoids for which the extension of the two-variable logic with guarded predicates recognised by the monoid is decidable, namely the class of idempotent monoids whose two-sided ideals are linearly ordered. For this, we introduce an automata formalism, set automata, that is equivalent to the class automata of Boja\'nczyk and Lasota and thus has an undecidable emptiness problem. We identify a subclass of set automata called ordered quasi-normal set automata that has a decidable emptiness problem by reduction to the emptiness problem of ordered multicounter automata. We show that the two-variable logic extended with guarded regular predicates recognised by a semigroup $S$ is expressively equivalent to a quasi-normal set automaton with the semigroup of transformations $S$. In particular, if $S$ is a linear band monoid then the resulting automaton is ordered, and the decidability result follows.

cs.LO↗

arXiv2026

Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games

We consider turn-based stochastic two-player games with a combination of a parity condition that must hold surely, that is in all possible outcomes, and of a parity condition that must hold almost-surely, that is with probability 1. The problem of deciding the existence of a winning strategy in such games is central in the framework of synthesis beyond worst-case where a hard requirement that must hold surely is combined with a softer requirement. Recent works showed that the problem is coNP-complete, and infinite-memory strategies are necessary in general, even in one-player games (i.e., Markov decision processes). However, memoryless strategies are sufficient for the opponent player. Despite these comprehensive results, the known algorithmic solution enumerates all memoryless strategies of the opponent, which is exponential in all cases, and does not construct a winning strategy when one exists. We present a recursive algorithm, based on a characterisation of the winning region, that gives a deeper insight into the problem. In particular, we show how to construct a winning strategy to achieve the combination of sure and almost-sure parity, and we derive new complexity and memory bounds for special classes of the problem, defined by fixing the index of either of the two parity conditions.

cs.GT↗

arXiv2025

Scalable Learning of One-Counter Automata via State-Merging Algorithms

We propose One-counter Positive Negative Inference (OPNI), a passive learning algorithm for deterministic real-time one-counter automata (DROCA). Inspired by the RPNI algorithm for regular languages, OPNI constructs a DROCA consistent with any given valid sample set. We further present a method for combining OPNI with active learning of DROCA, and provide an implementation of the approach. Our experimental results demonstrate that this approach scales more effectively than existing state-of-the-art algorithms. We also evaluate the performance of the proposed approach for learning visibly one-counter automata.

cs.FL↗

arXiv2025

Optimising expectation with guarantees for window mean payoff in Markov decision processes

The window mean-payoff objective strengthens the classical mean-payoff objective by computing the mean-payoff over a finite window that slides along an infinite path. Two variants have been considered: in one variant, the maximum window length is fixed and given, while in the other, it is not fixed but is required to be bounded. In this paper, we look at the problem of synthesising strategies in Markov decision processes that maximise the window mean-payoff value in expectation, while also simultaneously guaranteeing that the value is above a certain threshold. We solve the synthesis problem for three different kinds of guarantees: sure (that needs to be satisfied in the worst-case, that is, for an adversarial environment), almost-sure (that needs to be satisfied with probability one), and probabilistic (that needs to be satisfied with at least some given probability $p$). We show that for fixed window mean-payoff objective, all the three problems are in $\mathsf{PTIME}$, while for bounded window mean-payoff objective, they are in $\mathsf{NP} \cap \mathsf{coNP}$, and thus have the same complexity as for maximising the expected performance without any guarantee. Moreover, we show that pure finite-memory strategies suffice for maximising the expectation with sure and almost-sure guarantees, whereas, for maximising expectation with a probabilistic guarantee, randomised strategies are necessary in general.

cs.GT↗

arXiv2024

Expectation in Stochastic Games with Prefix-independent Objectives

Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective. We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP $\cap$ coUP when the window length is given in unary.

cs.GT↗

arXiv2023

Set Augmented Finite Automata over Infinite Alphabets

A data language is a set of finite words defined on an infinite alphabet. Data languages are used to express properties associated with data values (domain defined over a countably infinite set). In this paper, we introduce set augmented finite automata (SAFA), a new class of automata for expressing data languages. We investigate the decision problems, closure properties, and expressiveness of SAFA. We also study the deterministic variant of these automata.

cs.FL↗

arXiv2023

A Game of Pawns

We introduce and study pawn games, a class of two-player zero-sum turn-based graph games. A turn-based graph game proceeds by placing a token on an initial vertex, and whoever controls the vertex on which the token is located, chooses its next location. This leads to a path in the graph, which determines the winner. Traditionally, the control of vertices is predetermined and fixed. The novelty of pawn games is that control of vertices changes dynamically throughout the game as follows. Each vertex of a pawn game is owned by a pawn. In each turn, the pawns are partitioned between the two players, and the player who controls the pawn that owns the vertex on which the token is located, chooses the next location of the token. Control of pawns changes dynamically throughout the game according to a fixed mechanism. Specifically, we define several grabbing-based mechanisms in which control of at most one pawn transfers at the end of each turn. We study the complexity of solving pawn games, where we focus on reachability objectives and parameterize the problem by the mechanism that is being used and by restrictions on pawn ownership of vertices. On the positive side, even though pawn games are exponentially-succinct turn-based games, we identify several natural classes that can be solved in PTIME. On the negative side, we identify several EXPTIME-complete classes, where our hardness proofs are based on a new class of games called Lock & Key games, which may be of independent interest.

cs.GT↗

arXiv2023

Stochastic Window Mean-Payoff Games

Stochastic two-player games model systems with an environment that is both adversarial and stochastic. The adversarial part of the environment is modeled by a player (Player 2) who tries to prevent the system (Player 1) from achieving its objective. We consider finitary versions of the traditional mean-payoff objective, replacing the long-run average of the payoffs by payoff average computed over a finite sliding window. Two variants have been considered: in one variant, the maximum window length is fixed and given, while in the other, it is not fixed but is required to be bounded. For both variants, we present complexity bounds and algorithmic solutions for computing strategies for Player 1 to ensure that the objective is satisfied with positive probability, with probability 1, or with probability at least $p$, regardless of the strategy of Player 2. The solution crucially relies on a reduction to the special case of non-stochastic two-player games. We give a general characterization of prefix-independent objectives for which this reduction holds. The memory requirement for both players in stochastic games is also the same as in non-stochastic games by our reduction. Moreover, for non-stochastic games, we improve upon the upper bound for the memory requirement of Player 1 and upon the lower bound for the memory requirement of Player 2.

cs.GT↗

arXiv2023

Reinforcement Learning for Omega-Regular Specifications on Continuous-Time MDP

Continuous-time Markov decision processes (CTMDPs) are canonical models to express sequential decision-making under dense-time and stochastic environments. When the stochastic evolution of the environment is only available via sampling, model-free reinforcement learning (RL) is the algorithm-of-choice to compute optimal decision sequence. RL, on the other hand, requires the learning objective to be encoded as scalar reward signals. Since doing such translations manually is both tedious and error-prone, a number of techniques have been proposed to translate high-level objectives (expressed in logic or automata formalism) to scalar rewards for discrete-time Markov decision processes (MDPs). Unfortunately, no automatic translation exists for CTMDPs. We consider CTMDP environments against the learning objectives expressed as omega-regular languages. Omega-regular languages generalize regular languages to infinite-horizon specifications and can express properties given in popular linear-time logic LTL. To accommodate the dense-time nature of CTMDPs, we consider two different semantics of omega-regular objectives: 1) satisfaction semantics where the goal of the learner is to maximize the probability of spending positive time in the good states, and 2) expectation semantics where the goal of the learner is to optimize the long-run expected average time spent in the ``good states" of the automaton. We present an approach enabling correct translation to scalar reward signals that can be readily used by off-the-shelf RL algorithms for CTMDPs. We demonstrate the effectiveness of the proposed algorithms by evaluating it on some popular CTMDP benchmarks with omega-regular objectives.

cs.LG↗

arXiv2022

Parikh Automata over Infinite Words

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the $ω$-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types.

cs.FL↗

arXiv2022

History-deterministic Parikh Automata

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure properties of deterministic automata. Finally, we investigate the complexity of resolving nondeterminism in history-deterministic Parikh automata.

cs.FL↗

arXiv2022

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the fundamental models for non-deterministic systems with probabilistic uncertainty. Mean payoff (a.k.a. long-run average reward) is one of the most classic objectives considered in their context. We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP; further, we extend it to unknown CTMDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability, which has been advocated in literature. In addition to providing probably approximately correct (PAC) bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks.

eess.SY↗

arXiv2022

Strategy Synthesis for Global Window PCTL

Given a Markov decision process (MDP) $M$ and a formula $Φ$, the strategy synthesis problem asks if there exists a strategy $σ$ s.t. the resulting Markov chain $M[σ]$ satisfies $Φ$. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.

cs.LO↗

arXiv2021

Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games

Two-player mean-payoff Stackelberg games are nonzero-sum infinite duration games played on a bi-weighted graph by Leader (Player 0) and Follower (Player 1). Such games are played sequentially: first, Leader announces her strategy, second, Follower chooses his best-response. If we cannot impose which best-response is chosen by Follower, we say that Follower, though strategic, is adversarial towards Leader. The maximal value that Leader can get in this nonzero-sum game is called the adversarial Stackelberg value (ASV) of the game. We study the robustness of strategies for Leader in these games against two types of deviations: (i) Modeling imprecision - the weights on the edges of the game arena may not be exactly correct, they may be delta-away from the right one. (ii) Sub-optimal response - Follower may play epsilon-optimal best-responses instead of perfect best-responses. First, we show that if the game is zero-sum then robustness is guaranteed while in the nonzero-sum case, optimal strategies for ASV are fragile. Second, we provide a solution concept to obtain strategies for Leader that are robust to both modeling imprecision, and as well as to the epsilon-optimal responses of Follower, and study several properties and algorithmic problems related to this solution concept.

math.OC↗

arXiv2021

Safe Learning for Near Optimal Scheduling

In this paper, we investigate the combination of synthesis, model-based learning, and online sampling techniques to obtain safe and near-optimal schedulers for a preemptible task scheduling problem. Our algorithms can handle Markov decision processes (MDPs) that have 1020 states and beyond which cannot be handled with state-of-the art probabilistic model-checkers. We provide probably approximately correct (PAC) guarantees for learning the model. Additionally, we extend Monte-Carlo tree search with advice, computed using safety games or obtained using the earliest-deadline-first scheduler, to safely explore the learned model online. Finally, we implemented and compared our algorithms empirically against shielded deep Q-learning on large task systems.

cs.AI↗

arXiv2021

A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct

We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. These are also known as good-for-games pushdown automata. We prove that HD-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that HD-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than HD-PDA. We also study HDness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show that deciding HDness is ExpTime-complete. HD-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than HD-VPA. Both of these lower bounds are tight. We then compare HD-PDA with PDA for which composition with games is well-behaved, i.e. good-for-games automata. We show that these two notions coincide, but only if we consider potentially infinitely branching games. Finally, we study the complexity of resolving nondeterminism in HD-PDA. Every HDPDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of HD-VPA, but not those of HD-PDA. HD-PDA with finite-state resolvers are determinisable.

cs.FL↗

arXiv2020

Alternating Tree Automata with Qualitative Semantics

We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier, and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.

cs.FL↗