Searcharxiv⌕ Search

arXiv subjects

Rajarshi Ray

Publications and source records attributed to Rajarshi Ray.

At least 19 recordsLinked to original sources
arXiv2026

Runtime Enforcement of Hybrid System Properties

Runtime enforcement has emerged as a promising approach for ensuring the safety of autonomous and cyber-physical systems operating in uncertain and dynamic environments. Unlike traditional runtime verification, runtime enforcement actively intervenes during execution to prevent property violations by modifying unsafe system behaviors. Existing enforcement frameworks primarily focus on untimed or discrete-time specifications and are often limited to delaying or suppressing events, making them inadequate for reactive systems exhibiting complex continuous dynamics. In this paper, we propose a runtime enforcement framework where safety requirements are modeled using Hybrid Automata (HA). The framework combines discrete-event editing with continuous-time monitoring to support enforcement actions such as suppression, delay, and insertion of events at arbitrary time instants. Upon observing environmental inputs, the automaton is initialized, and runtime reachability analysis is used to synthesize safe corrective actions. We formally define the enforcement problem for safety hybrid automata, establish enforceability conditions, and present an online enforcement algorithm for reactive systems. A detailed case study on an Adaptive Cruise Control (ACC) system demonstrates the effectiveness of the proposed approach in maintaining safety properties under unsafe controller behaviors. Experimental results show that the framework introduces minimal computational overhead while ensuring continuous compliance with safety requirements in real time.

cs.FL↗
arXiv2026

Effective QCD model with consistent quasi-gluon treatment : formulation and application

The Polyakov loop enhanced Nambu-Jona-Lasinio model is reformulated in terms of the gluon quasi-particles in addition to the already existing quark quasi-particles. The formulation goes beyond the saddle point approximation for the gluon sector. The framework provides a physically consistent quasiparticle model for QCD thermodynamics. The ensuing advantages of this formulation is discussed using transport coefficients in the light quark sector.

hep-ph↗
arXiv2025

A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems

Reachability analysis of compositional hybrid systems, where individual components are modeled as hybrid automata, poses unique challenges. In addition to preserving the compositional semantics while computing system behaviors, algorithms have to cater to the explosion in the number of locations in the parallel product automaton. In this paper, we propose a bounded reachability analysis algorithm for compositional hybrid systems with piecewise affine dynamics, based on the principle of counterexample guided abstraction refinement (CEGAR). In particular, the algorithm searches for a counterexample in the discrete abstraction of the composition model, without explicitly computing a product automaton. When a counterexample is discovered in the abstraction, its validity is verified by a refinement of the state-space guided by the abstract counterexample. The state-space refinement is through a symbolic reachability analysis, particularly using a state-of-the-art algorithm with support functions as the continuous state representation. In addition, the algorithm mixes different semantics of composition with the objective of improved efficiency. Step compositional semantics is followed while exploring the abstract (discrete) state-space, while shallow compositional semantics is followed during state-space refinement with symbolic reachability analysis. Optimizations such as caching the results of the symbolic reachability analysis, which can be later reused, have been proposed. We implement this algorithm in the tool SAT-Reach and demonstrate the scalability benefits.

cs.LO↗
arXiv2025

Data-Driven Falsification of Cyber-Physical Systems

Cyber-Physical Systems (CPS) are abundant in safety-critical domains such as healthcare, avionics, and autonomous vehicles. Formal verification of their operational safety is, therefore, of utmost importance. In this paper, we address the falsification problem, where the focus is on searching for an unsafe execution in the system instead of proving their absence. The contribution of this paper is a framework that (a) connects the falsification of CPS with the falsification of deep neural networks (DNNs) and (b) leverages the inherent interpretability of Decision Trees for faster falsification of CPS. This is achieved by: (1) building a surrogate model of the CPS under test, either as a DNN model or a Decision Tree, (2) application of various DNN falsification tools to falsify CPS, and (3) a novel falsification algorithm guided by the explanations of safety violations of the CPS model extracted from its Decision Tree surrogate. The proposed framework has the potential to exploit a repertoire of \emph{adversarial attack} algorithms designed to falsify robustness properties of DNNs, as well as state-of-the-art falsification algorithms for DNNs. Although the presented methodology is applicable to systems that can be executed/simulated in general, we demonstrate its effectiveness, particularly in CPS. We show that our framework, implemented as a tool \textsc{FlexiFal}, can detect hard-to-find counterexamples in CPS that have linear and non-linear dynamics. Decision tree-guided falsification shows promising results in efficiently finding multiple counterexamples in the ARCH-COMP 2024 falsification benchmarks~\cite{khandait2024arch}.

cs.CR↗
arXiv2025

Preprint: Exploring Inevitable Waypoints for Unsolvability Explanation in Hybrid Planning Problems

Explaining unsolvability of planning problems is of significant research interest in Explainable AI Planning. AI planning literature has reported several research efforts on generating explanations of solutions to planning problems. However, explaining the unsolvability of planning problems remains a largely open and understudied problem. A widely practiced approach to plan generation and automated problem solving, in general, is to decompose tasks into sub-problems that help progressively converge towards the goal. In this paper, we propose to adopt the same philosophy of sub-problem identification as a mechanism for analyzing and explaining unsolvability of planning problems in hybrid systems. In particular, for a given unsolvable planning problem, we propose to identify common waypoints, which are universal obstacles to plan existence; in other words, they appear on every plan from the source to the planning goal. This work envisions such waypoints as sub-problems of the planning problem and the unreachability of any of these waypoints as an explanation for the unsolvability of the original planning problem. We propose a novel method of waypoint identification by casting the problem as an instance of the longest common subsequence problem, a widely popular problem in computer science, typically considered as an illustrative example for the dynamic programming paradigm. Once the waypoints are identified, we perform symbolic reachability analysis on them to identify the earliest unreachable waypoint and report it as the explanation of unsolvability. We present experimental results on unsolvable planning problems in hybrid domains.

cs.AI↗
arXiv2025

NTIRE 2025 Challenge on Image Super-Resolution (x4): Methods and Results

This paper presents the NTIRE 2025 image super-resolution ($\times$4) challenge, one of the associated competitions of the 10th NTIRE Workshop at CVPR 2025. The challenge aims to recover high-resolution (HR) images from low-resolution (LR) counterparts generated through bicubic downsampling with a $\times$4 scaling factor. The objective is to develop effective network designs or solutions that achieve state-of-the-art SR performance. To reflect the dual objectives of image SR research, the challenge includes two sub-tracks: (1) a restoration track, emphasizes pixel-wise accuracy and ranks submissions based on PSNR; (2) a perceptual track, focuses on visual realism and ranks results by a perceptual score. A total of 286 participants registered for the competition, with 25 teams submitting valid entries. This report summarizes the challenge design, datasets, evaluation protocol, the main results, and methods of each team. The challenge serves as a benchmark to advance the state of the art and foster progress in image SR.

cs.CV↗
arXiv2025

AUTONAV: A Toolfor Autonomous Navigation of Robots

We present a tool AUTONAV that automates the mapping, localization, and path-planning tasks for autonomous navigation of robots. The modular architecture allows easy integration of various algorithms for these tasks for comparison. We present the generated maps and path-plans by AUTONAV in indoor simulation scenarios.

cs.RO↗
arXiv2022

Probability distribution for black hole evaporation

Non-thermal correction to the emission probability of particles from black holes can be obtained if the backreaction or self-gravitational effects of the emitted particles on the black hole spacetime are taken into consideration. These non-thermally emitted particles conserve the entropy of the black hole, i.e, the entropy of the system of radiated particles after complete evaporation of the black hole matches the initial entropy of the black hole. Using the non-thermal emission probability, we have determined the probability for a black hole of mass $M$ to be completely evaporated by a given number of particles $n$. This is done by first evaluating the number of possible ways in which the black hole can be evaporated by emitting $n$ number of particles, and then the total number of ways in which the black hole can be evaporated. The ratio of these two quantities gives us the desired probability. From the probability distribution, we get a displacement relation between the most probable number of particles exhausting the black hole and the temperature of the initial black hole. This relation resembles Wien's displacement law for blackbody radiation.

gr-qc↗
arXiv2021

Consistent approach to study gluon quasi-particles

We discuss a novel approach to estimate the partition function in effective model frameworks when the effective potentials have multiple extrema, so that ascertaining a mean field becomes difficult. Using this approach we present a consistent model to study the thermodynamic properties of gluon quasi-particles as a function of temperature, both in the color confined and the color deconfined phases.

hep-ph↗
arXiv2021

Fast Falsification of Neural Networks using Property Directed Testing

Neural networks are now extensively used in perception, prediction and control of autonomous systems. Their deployment in safety-critical systems brings forth the need for verification techniques for such networks. As an alternative to exhaustive and costly verification algorithms, lightweight falsification algorithms have been heavily used to search for an input to the system that produces an unsafe output, i.e., a counterexample to the safety of the system. In this work, we propose a falsification algorithm for neural networks that directs the search for a counterexample, guided by a safety property specification. Our algorithm uses a derivative-free sampling-based optimization method. We evaluate our algorithm on 45 trained neural network benchmarks of the ACAS Xu system against 10 safety properties. We show that our falsification procedure detects all the unsafe instances that other verification tools also report as unsafe. Moreover, in terms of performance, our falsification procedure identifies most of the unsafe instances faster, in comparison to the state-of-the-art verification tools for feed-forward neural networks such as NNENUM and Neurify and in many instances, by orders of magnitude.

cs.AI↗
arXiv2021

A Beyond Mean Field Approach to Yang-Mills Thermodynamics

We propose a beyond mean field approach to evaluate Yang-Mills thermodynamics from the partition function with n-body gluon contribution, in the presence of a uniform background Polyakov field. Using a path integral based formalism, we obtain, unlike the previous mean field studies within this model framework, physically consistent results with good agreement to the lattice data throughout the temperature range.

hep-ph↗
arXiv2020

Modified Excluded Volume Hadron Resonance Gas Model with Lorentz Contraction

In this work we discuss a modified version of Excluded Volume Hadron Resonance Gas model and also study the effect of Lorentz contraction of the excluded volume on scaled pressure and susceptibilities of conserved charges. We find that the Lorentz contraction, coupled with the variety of excluded volume parameters reproduce the lattice QCD data quite satisfactorily.

hep-ph↗
arXiv2019

Finite temperature properties of a modified Polyakov$-$Nambu$-$Jona-Lasinio model

Thermodynamic properties of strongly interacting matter are investigated using the Polyakov loop enhanced Nambu$-$Jona-Lasinio model along with some modifications to include the hadrons. Various observables are shown to have a close agreement with the numerical data of QCD on lattice. The advantage of the present scheme over a similar study using a switching function is that here no extra parameters are to be fitted. As a result the present scheme can be easily extended for finite chemical potentials.

hep-ph↗
arXiv2019

Systematics of chemical freeze-out parameters in heavy-ion collision experiments

We discuss systematic uncertainties in the chemical freeze-out parameters from the $\chi^2$ analysis of hadron multiplicity ratios in the heavy-ion collision experiments. The systematics due to the choice of specific hadron ratios are found to lie within the experimental uncertainties. The variations obtained by removing the usual constraints on the conserved charges show similar behavior. The net charge to net baryon ratios in such unconstrained systems are commensurate with the expected value obtained from the protons and neutrons of the colliding nuclei up to the center of mass energies $\sim 40$ GeV. Beyond that the uncertainties in this ratio gradually increases, possibly indicating the reduction in baryon stopping.

hep-ph↗
arXiv2018

Simultaneous Solving of Batched Linear Programs on a GPU

Linear Programs (LPs) appear in a large number of applications and offloading them to a GPU is viable to gain performance. Existing work on offloading and solving an LP on a GPU suggests that there is performance gain generally on large sized LPs (typically 500 constraints, 500 variables and above). In order to gain performance from a GPU, for applications involving small to medium sized LPs, we propose batched solving of a large number of LPs in parallel. In this paper, we present the design and implementation of a batched LP solver in CUDA, keeping memory coalescent access, low CPU-GPU memory transfer latency and load balancing as the goals. The performance of the batched LP solver is compared against sequential solving in the CPU using the open source solver GLPK (GNU Linear Programming Kit) and the CPLEX solver from IBM. The evaluation on selected LP benchmarks from the Netlib repository displays a maximum speed-up of 95x and 5x with respect to CPLEX and GLPK solver respectively, for a batch of 1e5 LPs. We demonstrate the application of our batched LP solver to enhance performance in the domain of state-space exploration of mathematical models of control systems design.

cs.DC↗
arXiv2017

Thermodynamics of strongly interacting matter in a hybrid model

The equation of state and fluctuations of conserved charges in a strongly interacting medium under equilibrium conditions form the baseline upon which various possible scenarios in relativistic heavy-ion collision experiments are built. Many of these quantities have been obtained in the lattice QCD framework with reliable continuum extrapolations. Recently the Polyakov$-$Nambu$-$Jona-Lasinio model has been reparametrized to some extent to reproduce quantitatively the lattice QCD equation of state at vanishing chemical potentials. The agreement was precise except at low temperatures, possibly due to inadequate representation of the hadronic degrees of freedom in the model. This disagreement was also observed for some of the fluctuation and correlations considered. Here we address this issue by introducing the effects of hadrons through the Hadron Resonance Gas model. The total thermodynamic potential is now a weighted sum of the thermodynamic potential of the Polyakov$-$Nambu$-$Jona-Lasinio model and that of the Hadron Resonance Gas model. We find that the equation of state and the fluctuations and correlations obtained in this hybrid model agrees satisfactorily with the lattice QCD data in the low temperature regime.

hep-ph↗
arXiv2017

Exact Synthesis of Reversible Logic Circuits using Model Checking

Synthesis of reversible logic circuits has gained great atten- tion during the last decade. Various synthesis techniques have been pro- posed, some generate optimal solutions (in gate count) and are termed as exact, while others are scalable in the sense that they can handle larger functions but generate sub-optimal solutions. Although scalable synthe- sis is very much essential for circuit design, exact synthesis is also of great importance as it helps in building design library for the synthesis of larger functions. In this paper, we propose an exact synthesis technique for re- versible circuits using model checking. We frame the synthesis problem as a model checking instance and propose an iterative bounded model checking calls for an optimal synthesis. Experiments on reversible logic benchmarks shows successful synthesis of optimal circuits. We also illus- trate optimal synthesis of random functions with as many as 10 variables and up to 10 gates.

cs.ET↗