Showing 1–24 of 24 results for author: Mallik, K

Monitoring of Static Fairness

Authors: Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik

Abstract: Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present a general framework of runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure, with or without full observation of the st… ▽ More Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present a general framework of runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure, with or without full observation of the state space. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. We present two categories of monitoring algorithms, namely ones with a uniform error bound across all time points, and ones with weaker non-uniform, pointwise error bounds at different time points. Our monitoring algorithms use statistical tools that are adapted to suit the dynamic requirements of monitoring and the special needs of the fairness specifications. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. In these experiments, our monitors took less than a millisecond to update their verdicts after each observation. △ Less

Submitted 3 July, 2025; originally announced July 2025.

Comments: arXiv admin note: text overlap with arXiv:2305.15979

Monitoring Robustness and Individual Fairness

Authors: Ashutosh Gupta, Thomas A. Henzinger, Konstantin Kueffner, Kaushik Mallik, David Pape

Abstract: Input-output robustness appears in various different forms in the literature, such as robustness of AI models to adversarial or semantic perturbations and individual fairness of AI models that make decisions about humans. We propose runtime monitoring of input-output robustness of deployed, black-box AI models, where the goal is to design monitors that would observe one long execution sequence o… ▽ More Input-output robustness appears in various different forms in the literature, such as robustness of AI models to adversarial or semantic perturbations and individual fairness of AI models that make decisions about humans. We propose runtime monitoring of input-output robustness of deployed, black-box AI models, where the goal is to design monitors that would observe one long execution sequence of the model, and would raise an alarm whenever it is detected that two similar inputs from the past led to dissimilar outputs. This way, monitoring will complement existing offline ``robustification'' approaches to increase the trustworthiness of AI decision-makers. We show that the monitoring problem can be cast as the fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied, lacks suitable online solutions. We present our tool Clemont, which offers a number of lightweight monitors, some of which use upgraded online variants of existing FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams -- a data-structure commonly used in software and hardware verification. We have also developed an efficient parallelization technique that can substantially cut down the computation time of monitors for which the distance between input-output pairs is measured using the $L_\infty$ norm. Using standard benchmarks from the literature of adversarial and semantic robustness and individual fairness, we perform a comparative study of different monitors in \tool, and demonstrate their effectiveness in correctly detecting robustness violations at runtime. △ Less

Submitted 31 May, 2025; originally announced June 2025.

Efficient Dynamic Shielding for Parametric Safety Specifications

Authors: Davide Corsi, Kaushik Mallik, Andoni Rodriguez, Cesar Sanchez

Abstract: Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety… ▽ More Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower. △ Less

Submitted 28 May, 2025; originally announced May 2025.

Supermartingale Certificates for Quantitative Omega-regular Verification and Control

Authors: Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Đorđe Žikelić

Abstract: We present the first supermartingale certificate for quantitative $ω$-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certif… ▽ More We present the first supermartingale certificate for quantitative $ω$-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) $ω$-regular properties. We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches. △ Less

Submitted 24 May, 2025; originally announced May 2025.

Comments: Accepted at CAV 2025

Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives

Authors: Guy Avni, Martin Kurečka, Kaushik Mallik, Petr Novotný, Suman Sadhukhan

Abstract: Graph games are fundamental in strategic reasoning of multi-agent systems and their environments. We study a new family of graph games which combine stochastic environmental uncertainties and auction-based interactions among the agents, formalized as bidding games on (finite) Markov decision processes (MDP). Normally, on MDPs, a single decision-maker chooses a sequence of actions, producing a prob… ▽ More Graph games are fundamental in strategic reasoning of multi-agent systems and their environments. We study a new family of graph games which combine stochastic environmental uncertainties and auction-based interactions among the agents, formalized as bidding games on (finite) Markov decision processes (MDP). Normally, on MDPs, a single decision-maker chooses a sequence of actions, producing a probability distribution over infinite paths. In bidding games on MDPs, two players -- called the reachability and safety players -- bid for the privilege of choosing the next action at each step. The reachability player's goal is to maximize the probability of reaching a target vertex, whereas the safety player's goal is to minimize it. These games generalize traditional bidding games on graphs, and the existing analysis techniques do not extend. For instance, the central property of traditional bidding games is the existence of a threshold budget, which is a necessary and sufficient budget to guarantee winning for the reachability player. For MDPs, the threshold becomes a relation between the budgets and probabilities of reaching the target. We devise value-iteration algorithms that approximate thresholds and optimal policies for general MDPs, and compute the exact solutions for acyclic MDPs, and show that finding thresholds is at least as hard as solving simple-stochastic games. △ Less

Submitted 27 December, 2024; originally announced December 2024.

Comments: To appear in AAMAS 2025

Predictive Monitoring of Black-Box Dynamical Systems

Authors: Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik, Emily Yu, Đorđe Žikelić

Abstract: We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting… ▽ More We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor's expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques. △ Less

Submitted 21 December, 2024; originally announced December 2024.

Comments: Submitted to L4DC 2025

Fairness Shields: Safeguarding against Biased Decision Makers

Authors: Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, Kaushik Mallik

Abstract: As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions are often unfair or biased with respect to people's sensitive attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on specific instances of short decision seque… ▽ More As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions are often unfair or biased with respect to people's sensitive attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on specific instances of short decision sequences. We introduce fairness shielding, where a symbolic decision-maker -- the fairness shield -- continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes interventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algorithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios. △ Less

Submitted 16 December, 2024; originally announced December 2024.

Comments: To appear in AAAI 2025

Bidding Games with Charging

Authors: Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger, Kaushik Mallik

Abstract: Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules, and the winner is decided based on the infinite path traversed by the token from a given initial position. In bidding games, the players initially… ▽ More Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules, and the winner is decided based on the infinite path traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent charges. Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. We show that the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied? △ Less

Submitted 8 July, 2024; originally announced July 2024.

Extremal minimal bipartite matching covered graphs

Authors: Amit Kumar Mallik, Ajit A. Diwan, Nishad Kothari

Abstract: A connected graph, on four or more vertices, is matching covered if every edge is present in some perfect matching. An ear decomposition theorem (similar to the one for $2$-connected graphs) exists for bipartite matching covered graphs due to Hetyei. From the results and proofs of Lovász and Plummer, that rely on Hetyei's theorem, one may deduce that any minimal bipartite matching covered graph ha… ▽ More A connected graph, on four or more vertices, is matching covered if every edge is present in some perfect matching. An ear decomposition theorem (similar to the one for $2$-connected graphs) exists for bipartite matching covered graphs due to Hetyei. From the results and proofs of Lovász and Plummer, that rely on Hetyei's theorem, one may deduce that any minimal bipartite matching covered graph has at least $2(m-n+2)$ vertices of degree two (where minimal means that deleting any edge results in a graph that is not matching covered); such a graph is said to be extremal if it attains the stated lower bound. In this paper, we provide a complete characterization of the class of extremal minimal bipartite matching covered graphs. In particular, we prove that every such graph $G$ is obtained from two copies of a tree devoid of degree two vertices, say $T$ and $T'$, by adding edges -- each of which joins a leaf of $T$ with the corresponding leaf of $T'$. Apart from the aforementioned bound, there are four other bounds that appear in, or may be deduced from, the work of Lovász and Plummer. Each of these bounds leads to a notion of extremality. In this paper, we obtain a complete characterization of all of these extremal classes and also establish relationships between them. Two of our characterizations are in the same spirit as the one stated above. For the remaining two extremal classes, we reduce each of them to one of the already characterized extremal classes using standard matching theoretic operations. △ Less

Submitted 11 April, 2024; v1 submitted 9 April, 2024; originally announced April 2024.

Comments: Submitted to Innovations in Graph Theory

New Insights Into Achievable Spectral Efficiency With Adaptive Free Space Optical Transmissions

Authors: Himani Verma, Kamal Singh, Ranjan K. Mallik

Abstract: Terrestrial free-space optical (FSO) communication systems, while designed to operate on large unlicensed optical bandwidths, are power-constrained due to strict eye safety regulations. The channel fluctuation inherent in terrestrial FSO links also limits the received optical power. Consequently, the available signal-to-noise ratio (SNR) per Hz could become limited; this holds for future long-haul… ▽ More Terrestrial free-space optical (FSO) communication systems, while designed to operate on large unlicensed optical bandwidths, are power-constrained due to strict eye safety regulations. The channel fluctuation inherent in terrestrial FSO links also limits the received optical power. Consequently, the available signal-to-noise ratio (SNR) per Hz could become limited; this holds for future long-haul terrestrial systems based on coherent optical communications. An efficient and adaptive transmission mechanism is thus crucial at the optical source. However, a critical assessment of the impact of adaptive transmission in terrestrial FSO systems has received less attention in the literature. This work studies terrestrial FSO communication systems employing adaptive beam transmission while detection receivers operate under shot noise-limited conditions. Specifically, we propose a novel exact closed-form expression for the average spectral efficiency of these FSO systems with transmit beam power adaptation over the gamma-gamma turbulence channel with pointing error. More importantly, we provide a detailed assessment of the impact of turbulence and pointing error impairments on the performance of the aforementioned FSO systems, revealing several novel and counterintuitive insights. In particular, the extensive numerical results help elucidate the intricacies of analyzing these terrestrial FSO systems and clarify a few misconceptions alluded to in recent related literature. △ Less

Submitted 12 May, 2025; v1 submitted 17 February, 2024; originally announced February 2024.

A Gale-Shapley View of Unique Stable Marriages

Authors: Kartik Gokhale, Amit Kumar Mallik, Ankit Kumar Misra, Swaprava Nath

Abstract: Stable marriage of a two-sided market with unit demand is a classic problem that arises in many real-world scenarios. In addition, a unique stable marriage in this market simplifies a host of downstream desiderata. In this paper, we explore a new set of sufficient conditions for unique stable matching (USM) under this setup. Unlike other approaches that also address this question using the structu… ▽ More Stable marriage of a two-sided market with unit demand is a classic problem that arises in many real-world scenarios. In addition, a unique stable marriage in this market simplifies a host of downstream desiderata. In this paper, we explore a new set of sufficient conditions for unique stable matching (USM) under this setup. Unlike other approaches that also address this question using the structure of preference profiles, we use an algorithmic viewpoint and investigate if this question can be answered using the lens of the deferred acceptance (DA) algorithm (Gale and Shapley, 1962). Our results yield a set of sufficient conditions for USM (viz., MaxProp and MaxRou) and show that these are disjoint from the previously known sufficiency conditions like sequential preference and no crossing. We also provide a characterization of MaxProp that makes it efficiently verifiable, and shows the gap between MaxProp and the entire USM class. These results give a more detailed view of the sub-structures of the USM class. △ Less

Submitted 2 August, 2024; v1 submitted 28 October, 2023; originally announced October 2023.

Comments: 20 pages, 1 figure, In Proceedings, ECAI 2024

Auction-Based Scheduling

Authors: Guy Avni, Kaushik Mallik, Suman Sadhukhan

Abstract: Many sequential decision-making tasks require satisfaction of multiple, partially contradictory objectives. Existing approaches are monolithic, namely all objectives are fulfilled using a single policy, which is a function that selects a sequence of actions. We present auction-based scheduling, a modular framework for multi-objective decision-making problems. Each objective is fulfilled using a se… ▽ More Many sequential decision-making tasks require satisfaction of multiple, partially contradictory objectives. Existing approaches are monolithic, namely all objectives are fulfilled using a single policy, which is a function that selects a sequence of actions. We present auction-based scheduling, a modular framework for multi-objective decision-making problems. Each objective is fulfilled using a separate policy, and the policies can be independently created, modified, and replaced. Understandably, different policies with conflicting goals may choose conflicting actions at a given time. In order to resolve conflicts, and compose policies, we employ a novel auction-based mechanism. We allocate a bounded budget to each policy, and at each step, the policies simultaneously bid from their available budgets for the privilege of being scheduled and choosing an action. Policies express their scheduling urgency using their bids and the bounded budgets ensure long-run scheduling fairness. We lay the foundations of auction-based scheduling using path planning problems on finite graphs with two temporal objectives. We present decentralized algorithms to synthesize a pair of policies, their initially allocated budgets, and bidding strategies. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other: (a) strong synthesis, with no assumptions and strongest guarantees, (b) assume-admissible synthesis, with weakest rationality assumptions, and (c) assume-guarantee synthesis, with explicit contract-based assumptions. For reachability objectives, we show that, surprisingly, decentralized assume-admissible synthesis is always possible when the out-degrees of all vertices are at most two. △ Less

Submitted 31 January, 2024; v1 submitted 18 October, 2023; originally announced October 2023.

Comments: Full version of a paper accepted at TACAS'24

Monitoring Algorithmic Fairness under Partial Observations

Authors: Thomas A. Henzinger, Konstantin Kueffner, Kaushik Mallik

Abstract: As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of… ▽ More As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the (unknown) monitored system. Moreover, they can monitor only fairness properties that are specified as arithmetic expressions over the probabilities of different events. In this work, we extend fairness monitoring to systems modeled as partially observed Markov chains (POMC), and to specifications containing arithmetic expressions over the expected values of numerical functions on event sequences. The only assumptions we make are that the underlying POMC is aperiodic and starts in the stationary distribution, with a bound on its mixing time being known. These assumptions enable us to estimate a given property for the entire distribution of possible executions of the monitored POMC, by observing only a single execution. Our monitors observe a long run of the system and, after each new observation, output updated PAC-estimates of how fair or biased the system is. The monitors are computationally lightweight and, using a prototype implementation, we demonstrate their effectiveness on several real-world examples. △ Less

Submitted 1 August, 2023; originally announced August 2023.

Comments: The extended version of the paper, with the same title, published in 23rd International Conference on Runtime Verification (RV'23)

Monitoring Algorithmic Fairness

Authors: Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik

Abstract: Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common al… ▽ More Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system's model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation. △ Less

Submitted 25 May, 2023; originally announced May 2023.

Comments: CAV 2023

Runtime Monitoring of Dynamic Fairness Properties

Authors: Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik

Abstract: A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback patterns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring… ▽ More A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback patterns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and deploy a monitor that will continuously observe a long sequence of events generated by the system in the wild, and will output, with each event, a verdict on how fair the system is at the current point in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated at run-time, which is important because unfair behaviors may not be eliminated a priori, at design-time, due to partial knowledge about the system and the environment, as well as uncertainties and dynamic changes in the system and the environment, such as the unpredictability of human behavior. Secondly, monitors are by design oblivious to how the monitored system is constructed, which makes them suitable to be used as trusted third-party fairness watchdogs. They function as computationally lightweight statistical estimators, and their correctness proofs rely on the rigorous analysis of the stochastic process that models the assumptions about the underlying dynamics of the system. We show, both in theory and experiments, how monitors can warn us (1) if a bank's credit policy over time has created an unfair distribution of credit scores among the population, and (2) if a resource allocator's allocation policy over time has made unfair allocations. Our experiments demonstrate that the monitors introduce very low overhead. We believe that runtime monitoring is an important and mathematically rigorous new addition to the fairness toolbox. △ Less

Submitted 8 May, 2023; originally announced May 2023.

Journal ref: 2023 ACM Conference on Fairness, Accountability, and Transparency (FAccT '23), June 12--15, 2023, Chicago, IL, USA

Computing Adequately Permissive Assumptions for Synthesis

Authors: Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak, Anne-Kathrin Schmuck

Abstract: We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' needed from the environment to allow the system player to win. Given an $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every envi… ▽ More We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' needed from the environment to allow the system player to win. Given an $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every environment strategy compliant with $Ψ$ allows the system to fulfill $Φ$ (sufficiency), (ii) $Ψ$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $Ψ$ does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of $ω$-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches -- both theoretically and empirically. To the best of our knowledge, for $ω$-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive. △ Less

Submitted 6 April, 2023; v1 submitted 18 January, 2023; originally announced January 2023.

Comments: TACAS 2023

An Efficient Ratio Detector for Ambient Backscatter Communication

Authors: Wenjing Liu, Shanpu Shen, Danny H. K. Tsang, Ranjan K. Mallik, Ross Murch

Abstract: Ambient backscatter communication (AmBC) leverages the existing ambient radio frequency (RF) environment to implement communication with battery-free devices. One critical challenge of AmBC systems is signal recovery because the transmitted information bits are embedded in the ambient RF signals and these are unknown and uncontrollable. To address this problem, most existing approaches use averagi… ▽ More Ambient backscatter communication (AmBC) leverages the existing ambient radio frequency (RF) environment to implement communication with battery-free devices. One critical challenge of AmBC systems is signal recovery because the transmitted information bits are embedded in the ambient RF signals and these are unknown and uncontrollable. To address this problem, most existing approaches use averaging-based energy detectors and consequently the data rate is low and there is an error floor. Here we propose a new detection strategy based on the ratio between signals received from a multiple-antenna Reader. The advantage of using the ratio is that ambient RF signals are removed directly from the embedded signals without averaging and hence it can increase data rates and avoid the error floor. Different from original ratio detectors that use the magnitude ratio of the signals between two Reader antennas, in our proposed approach, we utilize the complex ratio so that phase information is preserved and propose an accurate linear channel model approximation. This allows the application of existing linear detection techniques from which we can obtain a minimum distance detector and closed-form expressions for bit error rate (BER). In addition, averaging, coding and interleaving can also be included to further enhance the BER. The results are also general, allowing any number of Reader antennas to be utilized in the approach. Numerical results demonstrate that the proposed approach performs better than approaches based on energy detection and original ratio detectors. △ Less

Submitted 18 October, 2022; originally announced October 2022.

Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness

Authors: Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani

Abstract: We consider fixpoint algorithms for two-player games on graphs with $ω$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the source vertex of a live ed… ▽ More We consider fixpoint algorithms for two-player games on graphs with $ω$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the source vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $ω$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic $ω$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude. △ Less

Submitted 23 February, 2023; v1 submitted 15 February, 2022; originally announced February 2022.

Journal ref: TheoretiCS, Volume 2 (February 24, 2023) theoretics:9088

MIMO Terahertz Quantum Key Distribution

Authors: Neel Kanth Kundu, Soumya P. Dash, Matthew R. McKay, Ranjan K. Mallik

Abstract: We propose a multiple-input multiple-output (MIMO) quantum key distribution (QKD) scheme for terahertz (THz) frequency applications operating at room temperature. Motivated by classical MIMO communications, a transmit-receive beamforming scheme is proposed that converts the rank-$r$ MIMO channel between Alice and Bob into $r$ parallel lossy quantum channels. Compared with existing single-antenna Q… ▽ More We propose a multiple-input multiple-output (MIMO) quantum key distribution (QKD) scheme for terahertz (THz) frequency applications operating at room temperature. Motivated by classical MIMO communications, a transmit-receive beamforming scheme is proposed that converts the rank-$r$ MIMO channel between Alice and Bob into $r$ parallel lossy quantum channels. Compared with existing single-antenna QKD schemes, we demonstrate that the MIMO QKD scheme leads to performance improvements by increasing the secret key rate and extending the transmission distance. Our simulation results show that multiple antennas are necessary to overcome the high free-space path loss at THz frequencies. We demonstrate a non-monotonic relation between performance and frequency, and reveal that positive key rates are achievable in the $10-30$ THz frequency range. The proposed scheme can be used for both indoor and outdoor QKD applications for beyond fifth-generation ultra-secure wireless communications systems. △ Less

Submitted 10 July, 2021; v1 submitted 8 May, 2021; originally announced May 2021.

Comments: Revisions submitted to IEEE Communications Letters

Symbolic Control for Stochastic Systems via Finite Parity Games

Authors: Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani

Abstract: We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we s… ▽ More We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region. The heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a 2.5-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract 2.5-player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve 2.5-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability. We have implemented the abstraction-based algorithm in Mascot-SDS (Majumdar et al., 2020), where we combined the outlined abstraction step with our recent tool FairSyn. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We outperform a recently proposed tool for solving this problem by a large margin. △ Less

Submitted 29 September, 2022; v1 submitted 4 January, 2021; originally announced January 2021.

Comments: 54 pages, under review in the Elsevier journal of Nonlinear Analysis: Hybrid Systems

ACM Class: G.3; I.1.2; I.1.4

Resilient Abstraction-Based Controller Design

Authors: Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider

Abstract: We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofol… ▽ More We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via so called disturbance edges. (II) We show that the application of resilient reactive synthesis techniques to these abstract models results in closed loop systems which are optimally resilient to these occasional high disturbance spikes. We have implemented this resilient ABCD workflow on top of SCOTS and showcase our method through multiple robot planning examples. △ Less

Submitted 14 August, 2020; originally announced August 2020.

Comments: 9 pages, 5 images, 1 table, to appear in CDC 2020

A Machine Learning Approach for Power Allocation in HetNets Considering QoS

Authors: Roohollah Amiri, Hani Mehrpouyan, Lex Fridman, Ranjan K. Mallik, Arumugam Nallanathan, David Matolak

Abstract: There is an increase in usage of smaller cells or femtocells to improve performance and coverage of next-generation heterogeneous wireless networks (HetNets). However, the interference caused by femtocells to neighboring cells is a limiting performance factor in dense HetNets. This interference is being managed via distributed resource allocation methods. However, as the density of the network inc… ▽ More There is an increase in usage of smaller cells or femtocells to improve performance and coverage of next-generation heterogeneous wireless networks (HetNets). However, the interference caused by femtocells to neighboring cells is a limiting performance factor in dense HetNets. This interference is being managed via distributed resource allocation methods. However, as the density of the network increases so does the complexity of such resource allocation methods. Yet, unplanned deployment of femtocells requires an adaptable and self-organizing algorithm to make HetNets viable. As such, we propose to use a machine learning approach based on Q-learning to solve the resource allocation problem in such complex networks. By defining each base station as an agent, a cellular network is modelled as a multi-agent network. Subsequently, cooperative Q-learning can be applied as an efficient approach to manage the resources of a multi-agent network. Furthermore, the proposed approach considers the quality of service (QoS) for each user and fairness in the network. In comparison with prior work, the proposed approach can bring more than a four-fold increase in the number of supported femtocells while using cooperative Q-learning to reduce resource allocation overhead. △ Less

Submitted 18 March, 2018; originally announced March 2018.

Comments: 7 pages, 7 figures, IEEE ICC'18

Physical Layer Security in Three-Tier Wireless Sensor Networks: A Stochastic Geometry Approach

Authors: Yansha Deng, Lifeng Wang, Maged Elkashlan, Arumugam Nallanathan, Ranjan K. Mallik

Abstract: This paper develops a tractable framework for exploiting the potential benefits of physical layer security in three-tier wireless sensor networks using stochastic geometry. In such networks, the sensing data from the remote sensors are collected by sinks with the help of access points, and the external eavesdroppers intercept the data transmissions.We focus on the secure transmission in two scenar… ▽ More This paper develops a tractable framework for exploiting the potential benefits of physical layer security in three-tier wireless sensor networks using stochastic geometry. In such networks, the sensing data from the remote sensors are collected by sinks with the help of access points, and the external eavesdroppers intercept the data transmissions.We focus on the secure transmission in two scenarios: i) the active sensors transmit their sensing data to the access points, and ii) the active access points forward the data to the sinks. We derive new compact expressions for the average secrecy rate in these two scenarios. We also derive a new compact expression for the overall average secrecy rate. Numerical results corroborate our analysis and show that multiple antennas at the access points can enhance the security of three-tier wireless sensor networks. Our results show that increasing the number of access points decreases the average secrecy rate between the access point and its associated sink. However, we find that increasing the number of access points first increases the overall average secrecy rate, with a critical value beyond which the overall average secrecy rate then decreases. When increasing the number of active sensors, both the average secrecy rate between the sensor and its associated access point and the overall average secrecy rate decrease. In contrast, increasing the number of sinks improves both the average secrecy rate between the access point and its associated sink, as well as the overall average secrecy rate. △ Less

Submitted 10 January, 2016; originally announced January 2016.

Comments: 11 pages, 7 figures

Power Allocation for Conventional and Buffer-Aided Link Adaptive Relaying Systems with Energy Harvesting Nodes

Authors: Imtiaz Ahmed, Aissa Ikhlef, Robert Schober, Ranjan K. Mallik

Abstract: Energy harvesting (EH) nodes can play an important role in cooperative communication systems which do not have a continuous power supply. In this paper, we consider the optimization of conventional and buffer-aided link adaptive EH relaying systems, where an EH source communicates with the destination via an EH decode-and-forward relay. In conventional relaying, source and relay transmit signals i… ▽ More Energy harvesting (EH) nodes can play an important role in cooperative communication systems which do not have a continuous power supply. In this paper, we consider the optimization of conventional and buffer-aided link adaptive EH relaying systems, where an EH source communicates with the destination via an EH decode-and-forward relay. In conventional relaying, source and relay transmit signals in consecutive time slots whereas in buffer-aided link adaptive relaying, the state of the source-relay and relay-destination channels determines whether the source or the relay is selected for transmission. Our objective is to maximize the system throughput over a finite number of transmission time slots for both relaying protocols. In case of conventional relaying, we propose an offline and several online joint source and relay transmit power allocation schemes. For offline power allocation, we formulate an optimization problem which can be solved optimally. For the online case, we propose a dynamic programming (DP) approach to compute the optimal online transmit power. To alleviate the complexity inherent to DP, we also propose several suboptimal online power allocation schemes. For buffer-aided link adaptive relaying, we show that the joint offline optimization of the source and relay transmit powers along with the link selection results in a mixed integer non-linear program which we solve optimally using the spatial branch-and-bound method. We also propose an efficient online power allocation scheme and a naive online power allocation scheme for buffer-aided link adaptive relaying. Our results show that link adaptive relaying provides performance improvement over conventional relaying at the expense of a higher computational complexity. △ Less

Submitted 10 September, 2012; originally announced September 2012.

Comments: Submitted to IEEE Transactions on Wireless Communications