arXiv subjects

S. Krishna

Publications and source records attributed to S. Krishna.

At least 19 recordsLinked to original sources

arXiv2026

Adaptive Strategies for GR(1) Games

We consider two-player GR(1) games on graphs, where the system player Eve must satisfy \[ \Box\Diamond A_1\land\cdots\land\Box\Diamond A_m \;\implies\; \Box\Diamond G_1\land\cdots\land\Box\Diamond G_n \] against the environment player Adam. Here $A_1,\ldots,A_m$ are assumptions on the environment, $G_1,\ldots,G_n$ are guarantees the system must provide, and $\Box\Diamond S$ denotes ``always eventually $S$''. Traditional static strategies are overly conservative: they may actively violate assumptions to trivially satisfy the implication, or abandon all guarantees when any assumption is violated. Existing methods to prevent such behaviors incur doubly exponential blowup. We introduce an adaptive framework treating Adam as a non-adversarial agent with unknown objectives. Eve monitors which assumptions Adam actually meets and adapts her strategy at runtime to maximize satisfied guarantees. Central to our approach is a novel algorithm for monitoring liveness properties $\Box\Diamond S$, enabling Eve to maintain real-time likelihood estimates of which assumptions will be fulfilled. Eve pre-computes strategies optimal for different assumption subsets, deploying a probability distribution over them that dynamically adjusts based on monitor outputs. We prove that when assumptions are violated, Eve's randomized adaptive strategy converges asymptotically to the deterministic strategy maximizing guarantees. A prototype demonstrates effectiveness and superior computational performance compared to the state of the art.

cs.LO↗

arXiv2026

Verifying Sequential Consistency under Bounded Preemptions

Gibbons and Korach studied a fundamental problem in 1997: given an observed sequence of reads and writes of a multi-threaded program, does there exist an interleaving which is sequentially consistent? Apart from applications in testing shared memory implementations, a procedure for this problem is employed in Dynamic Partial-Order-Reduction (DPOR) algorithms. The problem is known to be NP-hard even when different syntactic parameters are kept bounded. In this paper, we consider a restriction on the kind of interleaving required: does there exist a sequentially-consistent interleaving with at most {\pi} preemptions? Empirical evidence suggests that several bugs manifest within a few preemptive switches. This motivates us to investigate the problem under bounded preemptions. Our results exhibit a trichotomy: the problem lends to a polynomial-time algorithm for the class of single-writer programs where for each variable, there is a single thread writing to it; it becomes NP-hard for two-writer programs and finally, for three-writer programs, we get a conditional lower bound under the Exponential-Time-Hypothesis. When the number of preemptions {\pi} is not bounded, we show the problem to be W[1]-hard, and hence unlikely to be fixed-parameter-tractable with parameter {\pi}.

cs.PL↗

arXiv2026

Complexity of Consistency Testing for the Release-Acquire Semantics

In a seminal work, Gibbons and Korach studied the complexity of deciding whether an observed sequence of reads and writes of a multi-threaded program admits a sequentially consistent interleaving. They showed the problem to be NP-hard even under strong syntactic restrictions. More recently, Chakraborty et al. considered the problem for weak memory models and proved that NP-hardness remains even when the number of threads, the number of memory locations, and the value domain are all bounded. In this paper we revisit the problem for the release-acquire variants of the C11 memory model. Our main positive result is that consistency testing can be done in polynomial-time when each memory location is written by at most one thread (multiple readers are allowed). Notably, this restriction is already NP-hard for sequential consistency. We complement this upper bound with tight hardness results: the problem is NP-hard when two threads may write to the same location, and allowing three writers per location rules out 2^{o(k)}.n^{O(1)} algorithms under the Exponential Time Hypothesis, where k denotes the number of threads, and n the number of memory operations.

cs.CC↗

arXiv2025

Midinfrared Semiconductor Photonics - A Roadmap

Semiconductor photonic devices operating in the midwave infrared (mid-IR, which we roughly define here as wavelengths spanning 3 to 14 microns) uniquely address a wide range of current practical needs. These include chemical sensing, environmental monitoring, industrial process control, medical diagnostics, thermal imaging, LIDAR, free space optical communication, and security monitoring. However, mid-IR device technologies are currently still works in progress that are generally much less mature than their near infrared and visible counterparts. Not only are most of the relevant materials more difficult to grow and process, but attainment of the desired optical device performance is often fundamentally more challenging. This Roadmap will review the leading applications for mid-IR optoelectronics, summarize the status and deficiencies of current device technologies, and then suggest possible roadmaps for improving and maturing the performance, manufacturability, and cost of each device type so the critical needs that are uniquely addressed by mid-IR photonics can be satisfied.

physics.optics↗

arXiv2025

GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency

GPU computing is embracing weak memory concurrency for performance improvement. However, compared to CPUs, modern GPUs provide more fine-grained concurrency features such as scopes, have additional properties like divergence, and thereby follow different weak memory consistency models. These features and properties make concurrent programming on GPUs more complex and error-prone. To this end, we present GPUMC, a stateless model checker to check the correctness of GPU shared-memory concurrent programs under scoped-RC11 weak memory concurrency model. GPUMC explores all possible executions in GPU programs to reveal various errors - races, barrier divergence, and assertion violations. In addition, GPUMC also automatically repairs these errors in the appropriate cases. We evaluate GPUMC with benchmarks and real-life GPU programs. GPUMC is efficient both in time and memory in verifying large GPU programs where state-of-the-art tools are timed out. In addition, GPUMC identifies all known errors in these benchmarks compared to the state-of-the-art tools.

cs.LO↗

arXiv2024

Boundedness for Unions of Conjunctive Regular Path Queries over Simple Regular Expressions

The problem of checking whether a recursive query can be rewritten as query without recursion is a fundamental reasoning task, known as the boundedness problem. Here we study the boundedness problem for Unions of Conjunctive Regular Path Queries (UCRPQs), a navigational query language extensively used in ontology and graph database querying. The boundedness problem for UCRPQs is ExpSpace-complete. Here we focus our analysis on UCRPQs using simple regular expressions, which are of high practical relevance and enjoy a lower reasoning complexity. We show that the complexity for the boundedness problem for this UCRPQs fragment is $\Pi^P_2$-complete, and that an equivalent bounded query can be produced in polynomial time whenever possible. When the query turns out to be unbounded, we also study the task of finding an equivalent maximally bounded query, which we show to be feasible in $\Pi^P_2$. As a side result of independent interest stemming from our developments, we study a notion of succinct finite automata and prove that its membership problem is in NP.

cs.DB↗

arXiv2021

Scope-Bounded Reachability in Valence Systems

Multi-pushdown systems are a standard model for concurrent recursive programs, but they have an undecidable reachability problem. Therefore, there have been several proposals to underapproximate their sets of runs so that reachability in this underapproximation becomes decidable. One such underapproximation that covers a relatively high portion of runs is scope boundedness. In such a run, after each push to stack $i$, the corresponding pop operation must come within a bounded number of visits to stack $i$. In this work, we generalize this approach to a large class of infinite-state systems. For this, we consider the model of valence systems, which consist of a finite-state control and an infinite-state storage mechanism that is specified by a finite undirected graph. This framework captures pushdowns, vector addition systems, integer vector addition systems, and combinations thereof. For this framework, we propose a notion of scope boundedness that coincides with the classical notion when the storage mechanism happens to be a multi-pushdown. We show that with this notion, reachability can be decided in PSPACE for every storage mechanism in the framework. Moreover, we describe the full complexity landscape of this problem across all storage mechanisms, both in the case of (i) the scope bound being given as input and (ii) for fixed scope bounds. Finally, we provide an almost complete description of the complexity landscape if even a description of the storage mechanism is part of the input.

cs.FL↗

arXiv2020

Containment of Simple Regular Path Queries

Testing containment of queries is a fundamental reasoning task in knowledge representation. We study here the containment problem for Conjunctive Regular Path Queries (CRPQs), a navigational query language extensively used in ontology and graph database querying. While it is known that containment of CRPQs is expspace-complete in general, we focus here on severely restricted fragments, which are known to be highly relevant in practice according to several recent studies. We obtain a detailed overview of the complexity of the containment problem, depending on the features used in the regular expressions of the queries, with completeness results for np, pitwo, pspace or expspace.

cs.AI↗

arXiv2020

A Massive Field-Theoretic Model for Hodge Theory

Within the framework of Becchi-Rouet-Stora-Tyutin (BRST) formalism, we show that the four $(3+1)$-dimensional (4D) massive Abelian 2-form gauge theory (without any interaction with matter fields) is a model for the Hodge theory because its discrete and continuous symmetry transformations (and their corresponding Noether conserved charges) provide the physical realizations of the de Rham cohomological operators of differential geometry at the algebraic level. For this purpose, we incorporate the pseudo-scalar and axial-vector fields which appear in the theory with negative kinetic terms (but with proper definition of mass). The negative kinetic terms, for the above fields, are essential so that our theory could respect the discrete symmetry transformations which provide the physical realizations of the Hodge duality operation in the domain of differential geometry. Thus, our present endeavour, not only provides the physical realizations of all the mathematical ingredients connected with the de Rham cohomological operators of differential geometry, it also sheds light on the existence and emergence of fields with negative kinetic terms. We discuss the implications and relevance of the latter fields in the context of current models of dark matter and dark energy as well as the bouncing models of Universe.

hep-th↗

arXiv2019

Knowledge Compilation for Boolean Functional Synthesis

Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever \exists X F(X,Y) holds. In this paper, we investigate the relation between the representation of the specification F(X,Y) and the complexity of synthesis. We introduce a new normal form for Boolean formulas, called SynNNF, that guarantees polynomial-time synthesis and also polynomial-time existential quantification for some order of quantification of variables. We show that several normal forms studied in the knowledge compilation literature are subsumed by SynNNF, although SynNNFcan be super-polynomially more succinct than them. Motivated by these results, we propose an algorithm to convert a specification in CNF to SynNNF, with the intent of solving the Boolean functional synthesis problem. Experiments with a prototype implementation show that this approach solves several benchmarks beyond the reach of state-of-the-art tools.

cs.LO↗

arXiv2019

Synthesis of Computable Regular Functions of Infinite Words

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming $\omega$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function $f$ (equivalently specified by one of the aforementioned transducer model), is $f$ computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in $\mathsf{NLogSpace}$ (it was already known to be in $\mathsf{PTime}$ by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

cs.FL↗

arXiv2018

Planetary Nebulae with UVIT II: Revelations from FUV vision of Butterfly Nebula NGC 6302

The high excitation planetary nebula, NGC 6302, has been imaged in two far-ultraviolet (FUV) filters, F169M (Sapphire; λ$_{\rm eff}$: 1608 Å) and F172M (Silica; λ$_{\rm eff}$: 1717 Å) and two NUV filters, N219M (B15; λ$_{\rm eff}$: 2196 Å) and N279N (N2; λ$_{\rm eff}$: 2792 Å) with the Ultra Violet Imaging Telescope (UVIT). The FUV F169M image shows faint emission lobes that extend to about 5 arcmin on either side of the central source. Faint orthogonal collimated jet-like structures are present on either side of the FUV lobes through the central source. These structures are not present in the two NUV filters nor in the FUV F172M filter. Optical and IR images of NGC 6302 show bright emission bipolar lobes in the east-west direction with a massive torus of molecular gas and dust seen as a dark lane in the north-south direction. The FUV lobes are much more extended and oriented at a position angle of 113°. They and the jet-like structures might be remnants of an earlier evolutionary phase, prior to the dramatic explosive event that triggered the Hubble type bipolar flows approximately 2200 years ago. The source of the FUV lobe and jet emission is not known, but is likely due to fluorescent emission from H$_2$ molecules. The cause of the difference in orientation of optical and FUV lobes is not clear and, we speculate, could be related to two binary interactions.

astro-ph.GA↗

arXiv2018

Communicating Timed Processes with Perfect Timed Channels

We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the finite-state processes are replaced by timed automata, and messages inside the perfect channels are equipped with clocks representing their ages. In addition to the standard operations (resetting clocks, checking guards of clocks) each automaton can either (1) append a message to the tail of a channel with an initial age or (2) receive the message at the head of a channel if its age satisfies a set of given constraints. In this paper, we show that the reachability problem is undecidable even in the case of two timed automata connected by one unidirectional timed channel if one allows global clocks (that the two automata can check and manipulate). We prove that this undecidability still holds even for CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable (in $\mathsf{EXPTIME}$) in the case of two automata linked with one unidirectional timed channel and with no global clock. Finally, we consider the bounded-context case, where in each context, only one timed automaton is allowed to receive messages from one channel while being able to send messages to all the other timed channels. In this case we show that the reachability problem is decidable.

cs.FL↗

arXiv2017

Planetary Nebulae with Ultra-Violet Imaging Telescope (UVIT): Far Ultra-violet halo around the Bow Tie nebula (NGC 40)

Context. NGC 40 is a planetary nebula with diffuse X-ray emission, suggesting an interaction of the high speed wind from WC8 central star (CS) with the nebula. It shows strong Civ 1550 Å emission that cannot be explained by thermal processes alone. We present here the first map of this nebula in C IV emission, using broad band filters on the UVIT. Aims. To map the hot C IV emitting gas and its correspondence with soft X-ray (0.3-8 keV) emitting regions, in order to study the shock interaction with the nebula and the ISM. This also illustrates the potential of UVIT for nebular studies. Methods. Morphological study of images of the nebula obtained at an angular resolution of about 1.3" in four UVIT filter bands that include C IV 1550 Å and C II] 2326 Å lines and UV continuum. Comparisons with X-ray, optical, and IR images from literature. Results. The C II] 2326 Å images show the core of the nebula with two lobes on either side of CS similar to [N II]. The C IV emission in the core shows similar morphology and extant as that of diffuse X-ray emission concentrated in nebular condensations. A surprising UVIT discovery is the presence of a large faint FUV halo in FUV Filter with λeff of 1608 Å. The UV halo is not present in any other UV filter. FUV halo is most likely due to UV fluorescence emission from the Lyman bands of H2 molecules. Unlike the optical and IR halo, FUV halo trails predominantly towards south-east side of the nebular core, opposite to the CS's proper motion direction. Conclusions. Morphological similarity of C IV 1550 Å and X-ray emission in the core suggests that it results mostly from interaction of strong CS wind with the nebula. The FUV halo in NGC 40 highlights the existence of H2 molecules extensively in the regions even beyond the optical and IR halos.

astro-ph.GA↗

arXiv2017

Augmented Superfield Approach to Gauge-invariant Massive 2-Form Theory

We discuss the complete sets of the off-shell nilpotent (i.e. s^2_{(a)b} = 0) and absolutely anticommuting (i.e. s_b s_{ab} + s_{ab} s_b = 0) Becchi-Rouet-Stora-Tyutin (BRST) (s_b) and anti-BRST (s_{ab}) symmetries for the (3+1)-dimensional (4D) gauge-invariant massive 2-form theory within the framework of augmented superfield approach to BRST formalism. In this formalism, we obtain the coupled (but equivalent) Lagrangian densities which respect both BRST and anti-BRST symmetries on the constrained hypersurface defined by the Curci-Ferrari type conditions. The absolute anticommutativity property of the (anti-)BRST transformations (and corresponding generators) is ensured by the existence of the Curci-Ferrari type conditions which emerge very naturally in this formalism. Furthermore, the gauge-invariant restriction plays a decisive role in deriving the proper (anti-)BRST transformations for the St{ü}ckelberg-like vector field.

hep-th↗

arXiv2017

Effective Sextic Superpotential and $B-L$ violation in NMSGUT

We list operators of the superpotential of the effective MSSM that emerges from the NMSGUT up to sextic degree. We give illustrative expressions for the coefficients in terms of NMSGUT parameters. We also estimate the impact of GUT scale threshold corrections on these effective operators in view of the demonstration that $B$ violation via quartic superpotential terms can be suppressed to acceptable levels after including such corrections in the NMSGUT. We find a novel $B, B-L$ violating quintic operator that leads to the decay mode $n\to e^- K^+$. We also remark that the threshold corrections to the Type I seesaw mechanism make the deviation of right handed neutrino masses from the GUT scale more natural while Type II seesaw neutrino masses, which earlier tended to utterly negligible receive threshold enhancement. Our results are of relevance for analyzing $B-L$ violating operator based, sphaleron safe, Baryogenesis.

hep-ph↗

arXiv2017

N= 4 Supersymmetric Quantum Mechanical Model: Novel Symmetries

We discuss a set of novel discrete symmetry transformations of the N = 4 supersymmetric quantum mechanical model of a charged particle moving on a sphere in the background of Dirac magnetic monopole. The usual five continuous symmetries (and their conserved Noether charges) and two discrete symmetries together provide the physical realizations of the de Rham cohomological operators of differential geometry. We have also exploited the supervariable approach to derive the nilpotent N = 4 SUSY transformations and provided the geometrical interpretation in the language of translational generators along the Grassmannian directions onto (1, 4)-dimensional supermanifold.

hep-th↗

arXiv2016

Novel symmetries in an interacting N = 2 supersymmetric quantum mechanical model

We demonstrate the existence of a set of novel discrete symmetry transformations in the case of an interacting N = 2 supersymmetric quantum mechanical model of a system of an electron moving on a sphere in the background of a magnetic monopole and establish its interpretation in the language of differential geometry. These discrete symmetries are, over and above, the usual three continuous symmetries of the theory which together provide the physical realizations of the de Rham cohomological operators of differential geometry. We derive the nilpotent N = 2 SUSY transformations by exploiting our idea of supervariable approach and provide geometrical meaning to these transformations in the language of Grassmannian translational generators on a (1, 2)-dimensional supermanifold on which our N = 2 SUSY quantum mechanical model is generalized. We express the conserved supercharges and the invariance of the Lagrangian in terms of the supervariables (obtained after the imposition of the SUSY invariant restrictions) and provide the geometrical meaning to (i) the nilpotency property of the N = 2 supercharges, and (ii) the SUSY invariance of the Lagrangian of our N = 2 SUSY theory.

hep-th↗