arXiv subjects

Avinash Malik

Publications and source records attributed to Avinash Malik.

At least 19 recordsLinked to original sources

arXiv2026

Sound Compilation of Weighted Event Signal Temporal Logic to Timeless Geometric Control

Cyber-Physical Systems (CPS) controllers synthesized from standard temporal logics rely on rigid global clocks, rendering them vulnerable to asynchronous timing anomalies like clock snaps, jitter, and network delays. To overcome these vulnerabilities, we introduce a fundamentally timeless geometric control paradigm alongside a novel specification language: Weighted Event-Based Signal Temporal Logic (weSTL+). This new weSTL+ logic combines the event triggered nature of Event-STL with weighted user preferences of weighted-STL making it suitable for specification of practical autonomous CPS. Using a two-pass compiler, our framework translates weSTL+ formulae directly into C^1-differentiable time-invariant geometric surrogate constraints via finite-time level-set inversion. By mapping temporal windows directly into physical time independent geometric boundaries, this approach entirely eliminates explicit runtime clock monitoring. Our autonomous robotics case study demonstrates that the proposed geometric architecture guarantees enforcement of safety and liveness under severe macroscopic timing discontinuities, succeeding where traditional time-indexed controllers fail.

eess.SY↗

arXiv2026

The Space-Time Transform: Memory-Augmented Control Barrier Functions

Control Barrier Functions (CBFs), their High-Order variants (HOCBFs) and Exponential CBFs (ECBFs) are standard geometric tools for enforcing nonlinear safety constraints. CBFs, and their variants, offer an elegant geometric framework for nonlinear safety, yet mathematically, they reduce to continuous-time convolutions restricted by zero-memory kernels. In the presence of high-frequency measurement noise, these memoryless operators act as improper filters, leading to significant control chattering and the potential loss of active control authority due to Quadratic Program (QP) infeasibility. To address this structural limitation, this paper introduces a space-time transform that embeds dynamic temporal filtering directly into the safety constraint synthesis. By designing a proper spatio-temporal kernel, this approach inherently attenuates high-frequency noise while preserving affine control authority. Crucially, we prove the robust forward invariance of the designed STT-CBF. Monte Carlo simulations of a third-order system demonstrate that the proposed framework achieves a 100% safety rate while reducing control total variation by over 99% compared to conventional parameterized barrier methods, mitigating hardware hazards and enabling reliable deployment on physical robotic platforms.

eess.SY↗

arXiv2026

CIPS: Maximal Certified Persistence in Cyber-Physical Systems

We introduce the Theory of Certified Information Persistence Systems (CIPS), a universal mathematical framework for computing the maximal certified persistence of information in cyber-physical systems (CPS). CIPS provides an axiomatic foundation that separates the continuous evolution of state validity from discrete, memoryless control interventions. By accommodating digital sampling and execution latency through robust set contraction, the framework mathematically isolates a system's maximal certified persistence horizon --- a strict theoretical upper bound on safe autonomous operation relative to the system's defined metric growth bounds. Our central representation theorem proves that CIPS provides a universal representation framework: every empirically safe scheduling policy, is structurally isomorphic to a conservative surrogate evaluation within a canonical CIPS. By dynamically targeting this latency-compensated canonical horizon, the framework minimizes conservatism relative to the bounding assumptions, achieving an optimal certified scheduling policy, minimizing computational and network interventions while mathematically guaranteeing continuous physical safety.

eess.SY↗

arXiv2026

An Asynchronous multi-rate Taylor method for Delay Differential Equations

The numerical simulation of high-dimensional, multi-rate Delay Differential Equations (DDEs) is fundamentally bottlenecked by synchronous time-stepping and the dynamic memory allocation required for continuous history tracking. In this paper, we introduce the Asynchronous Adaptive Taylor Solver (AATS), an event-driven integration framework designed to overcome these high-performance computing limitations. By assigning independent local clocks to individual coordinates and advancing them using high-order Taylor polynomials generated via compile-time Automatic Differentiation, AATS restricts computational work to actively evolving sub-graphs. To eliminate the severe memory overhead endemic to traditional DDE solvers, AATS utilizes statically allocated circular buffers to store polynomial segments, achieving interpolation-free continuous dense-output evaluation with a verified zero-allocation runtime memory footprint. Alongside this software architecture, we establish a novel continuous proof of convergence for asynchronous Taylor expansions and formally prove that the framework's algorithmic complexity scales linearly (O(N)). Extensive benchmarks against state-of-the-art synchronous solvers (Julia SciML) validate these theoretical bounds. On large-scale benchmarks (upto $N = 10000$ coordinates) AATS fundamentally minimizes the constant factor of algorithmic work by avoiding redundant evaluations, delivering empirically consistent with O(N) execution scaling and significant wall-clock speedups.

cs.MS↗

arXiv2026

Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS. However, static verification of STL is undecidable in general, except when we want to verify using run-time-based methods, which have limitations. We propose Synchronous Signal Temporal Logic (SSTL), a decidable fragment of STL, which admits static safety and liveness property verification. In SSTL, we assume that a signal is sampled at fixed discrete steps, called ticks, and then propose a hypothesis, called the Signal Invariance Hypothesis (SIH), which is inspired by a similar hypothesis for synchronous programs. We define the syntax and semantics of SSTL and show that SIH is a necessary and sufficient condition for equivalence between an STL formula and its SSTL counterpart. By translating SSTL to LTL_P (LTL defined over predicates), we enable decidable model checking using the SPIN model checker. We demonstrate the approach on a 33-node human heart model and other case studies.

cs.FL↗

arXiv2025

Efficient compilation and execution of synchronous programs via type-state programming

Synchronous programs are used extensively in implementation of safety critical embedded software. Imperative synchronous programming languages model multiple Finite State Machines (FSMs) executing in lockstep at logical clock ticks. The synchronous view of time along with the FSM based design enables easier formal verification. The synchronous composition of multiple FSMs, during compilation, results in the well known state space explosion problem. Hence, efficiently compiling imperative synchronous programs into small and fast executables is challenging. This paper introduces a novel linear time compilation technique for automata based compilation of synchronous programs. Graph based rewrite rules for kernel programming constructs are introduced. A linear time algorithm applies these rules to produce a FSM. The FSM is then encoded into a type-state program using template meta-programming in C++. Experimental results show that the compilation time and generated binary size is comparable, while the execution times are on average 31-60% faster than current state-of-the-art compilers.

cs.PL↗

arXiv2025

Timetide: A programming model for logically synchronous distributed systems

Massive strides in deterministic models have been made using synchronous languages. They are mainly focused on centralised applications, as the traditional approach is to compile away the concurrency. Time triggered languages such as Giotto and Lingua Franca are suitable for distribution albeit that they rely on expensive physical clock synchronisation, which is both expensive and may suffer from scalability. Hence, deterministic programming of distributed systems remains challenging. We address the challenges of deterministic distribution by developing a novel multiclock semantics of synchronous programs. The developed semantics is amenable to seamless distribution. Moreover, our programming model, Timetide, alleviates the need for physical clock synchronisation by building on the recently proposed logical synchrony model for distributed systems. We discuss the important aspects of distributing computation, such as network communication delays, and explore the formal verification of Timetide programs. To the best of our knowledge, Timetide is the first multiclock synchronous language that is both amenable to distribution and formal verification without the need for physical clock synchronisation or clock gating.

cs.PL↗

arXiv2025

Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains

Hybrid systems are mostly modelled, simulated, and verified in the time domain by computer scientists. Engineers, however, use both frequency and time domain modelling due to their distinct advantages. For example, frequency domain modelling is better suited for control systems, using features such as spectra of the signal. Considering this, we introduce, for the first time, a formal model called frequency automata for hybrid systems modelling and simulation, which are represented in combined time and frequency domains. We propose a sound translation from Hybrid Automata (HA) to Frequency Automata (FA). We also develop a numerical simulator for FA and compare it with the performance of HA. Our approach provides precise level crossing detection and efficient simulation of hybrid systems. We provide empirical results comparing simulation of HA via its translation to FA and its simulation via Matlab Simulink/Stateflow. The results show clear superiority of the proposed technique with the execution times of the proposed technique 118x to 1129x faster compared to Simulink/Stateflow. Moreover, we also observe that the proposed technique is able to detect level crossing with complex guards (including equality), which Simulink/Stateflow fail.

cs.FL↗

arXiv2024

Reinforcement Learning Pair Trading: A Dynamic Scaling approach

Cryptocurrency is a cryptography-based digital asset with extremely volatile prices. Around USD 70 billion worth of cryptocurrency is traded daily on exchanges. Trading cryptocurrency is difficult due to the inherent volatility of the crypto market. This study investigates whether Reinforcement Learning (RL) can enhance decision-making in cryptocurrency algorithmic trading compared to traditional methods. In order to address this question, we combined reinforcement learning with a statistical arbitrage trading technique, pair trading, which exploits the price difference between statistically correlated assets. We constructed RL environments and trained RL agents to determine when and how to trade pairs of cryptocurrencies. We developed new reward shaping and observation/action spaces for reinforcement learning. We performed experiments with the developed reinforcement learner on pairs of BTC-GBP and BTC-EUR data separated by 1 min intervals (n=263,520). The traditional non-RL pair trading technique achieved an annualized profit of 8.33%, while the proposed RL-based pair trading technique achieved annualized profits from 9.94% to 31.53%, depending upon the RL learner. Our results show that RL can significantly outperform manual and traditional pair trading techniques when applied to volatile markets such as~cryptocurrencies.

q-fin.CP↗

arXiv2024

Optimal market-neutral currency trading on the cryptocurrency platform

This research proposes a novel arbitrage approach in multivariate pair trading, termed the Optimal Trading Technique (OTT). We present a method for selectively forming a "bucket" of fiat currencies anchored to cryptocurrency for monitoring and exploiting trading opportunities simultaneously. To address quantitative conflicts from multiple trading signals, a novel bi-objective convex optimization formulation is designed to balance investor preferences between profitability and risk tolerance. We understand that cryptocurrencies carry significant financial risks. Therefore this process includes tunable parameters such as volatility penalties and action thresholds. In experiments conducted in the cryptocurrency market from 2020 to 2022, which encompassed a vigorous bull run followed by a bear run, the OTT achieved an annualized profit of 15.49%. Additionally, supplementary experiments detailed in the appendix extend the applicability of OTT to other major cryptocurrencies in the post-COVID period, validating the model's robustness and effectiveness in various market conditions. The arbitrage operation offers a new perspective on trading, without requiring external shorting or holding the intermediate during the arbitrage period. As a note of caution, this study acknowledges the high-risk nature of cryptocurrency investments, which can be subject to significant volatility and potential loss.

cs.CE↗

arXiv2021

Impulse data models for the inverse problem of electrocardiography

The proposed method re-frames traditional inverse problems of electrocardiography into regression problems, constraining the solution space by decomposing signals with multidimensional Gaussian impulse basis functions. Impulse HSPs were generated with single Gaussian basis functions at discrete heart surface locations and projected to corresponding BSPs using a volume conductor torso model. Both BSP (inputs) and HSP (outputs) were mapped to regular 2D surface meshes and used to train a neural network. Predictive capabilities of the network were tested with unseen synthetic and experimental data. A dense full connected single hidden layer neural network was trained to map body surface impulses to heart surface Gaussian basis functions for reconstructing HSP. Synthetic pulses moving across the heart surface were predicted from the neural network with root mean squared error of $9.1\pm1.4$%. Predicted signals were robust to noise up to 20 dB and errors due to displacement and rotation of the heart within the torso were bounded and predictable. A shift of the heart 40 mm toward the spine resulted in a 4\% increase in signal feature localization error. The set of training impulse function data could be reduced and prediction error remained bounded. Recorded HSPs from in-vitro pig hearts were reliably decomposed using space-time Gaussian basis functions. Predicted HSPs for left-ventricular pacing had a mean absolute error of $10.4\pm11.4$ ms. Other pacing scenarios were analyzed with similar success. Conclusion: Impulses from Gaussian basis functions are potentially an effective and robust way to train simple neural network data models for reconstructing HSPs from decomposed BSPs. The HSPs predicted by the neural network can be used to generate activation maps that non-invasively identify features of cardiac electrical dysfunction and can guide subsequent treatment options.

q-bio.QM↗

arXiv2019

Recommendation Engine for Lower Interest Borrowing on Peer to Peer Lending (P2PL) Platform

Online Peer to Peer Lending (P2PL) systems connect lenders and borrowers directly, thereby making it convenient to borrow and lend money without intermediaries such as banks. Many recommendation systems have been developed for lenders to achieve higher interest rates and avoid defaulting loans. However, there has not been much research in developing recommendation systems to help borrowers make wise decisions. On P2PL platforms, borrowers can either apply for bidding loans, where the interest rate is determined by lenders bidding on a loan or traditional loans where the P2PL platform determines the interest rate. Different borrower grades -- determining the credit worthiness of borrowers get different interest rates via these two mechanisms. Hence, it is essential to determine which type of loans borrowers should apply for. In this paper, we build a recommendation system that recommends to any new borrower the type of loan they should apply for. Using our recommendation system, any borrower can achieve lowered interest rates with a higher likelihood of getting funded.

q-fin.GN↗

arXiv2019

Deep learning neural nets for detecting heart activity

The prediction of heart surface potentials using measurements from the body's surface is known as the inverse problem of electrocardiography. It is an ill-posed problem due to the multiple factors that affect the heart signal as it propagates through the body. This report details research performed into a machine learning solution to signal reconstruction as well as an analysis of optimal torso electrode positioning for prediction involving different areas of the heart. The dataset contains simultaneous measurements from a large number of body surface potential (BSP) and heart surface potential (HSP) electrodes, as well as their geometric locations, recorded from an experiment using a human model. Initially, Time Delayed Neural Nets were trained and tested across all BSP to HSP relationships resulting in a slight trend of increased reconstruction correlation with decreased separation of electrodes. However, the TDNNs had overfitted to the data and failed to predict alternate heartbeat pacings. Feed Forward Neural Nets (FFNNs) were tested in a many BSP to many HSP prediction method. Again overfitting occurred. To reduce overfitting, the number of training signals was reduced by analysing the optimal training BSPs for each HSP when using basic perceptrons. This analysis involved repeat sampling and ranking of different BSP combinations, initially, using a Monte Carlo approximation, until being replaced with a meta-heuristic which increased the yield of successful BSP combinations. Successful reconstructions across heartbeat pacings were produced using these optimal BSP combinations for 80 of the 108 HSPs, and future work exists for the testing of this method of prediction using real patient data.

physics.med-ph↗

arXiv2018

Quantized State Hybrid Automata for Cyber-Physical Systems

Cyber-physical systems involve a network of discrete controllers that control physical processes. Examples range from autonomous cars to implantable medical devices, which are highly safety critical. Hybrid Automata (HA) based formal approach is gaining momentum for the specification and validation of CPS. HA combines the model of the plant along with its discrete controller resulting in a piece-wise continuous system with discontinuities. Accurate detection of these discontinuities, using appropriate level crossing detectors, is a key challenge to simulation of CPS based on HA. Existing techniques employ time discrete numerical integration with bracketing for level crossing detection. These techniques involve back-tracking and are highly non-deterministic and hence error prone. As level crossings happen based on the values of continuous variables, Quantized State System (QSS)- integration may be more suitable. Existing QSS integrators, based on fixed quanta, are also unsuitable for simulating HAs. This is since the quantum selected is not dependent on the HA guard conditions, which are the main cause of discontinuities. Considering this, we propose a new dynamic quanta based formal model called Quantized State Hybrid Automata (QSHA). The developed formal model and the associated simulation framework guarantees that (1) all level crossings are accurately detected and (2) the time of the level crossing is also accurate within floating point error bounds. Interestingly, benchmarking results reveal that the proposed simulation technique takes 720, 1.33 and 4.41 times fewer simulation steps compared to standard Quantized State System (QSS)-1, Runge-Kutta (RK)-45, and Differential Algebraic System Solver (DASSL) integration based techniques respectively.

eess.SY↗

arXiv2018

A machine learning approach to reconstruction of heart surface potentials from body surface potentials

Invasive cardiac catheterisation is a common procedure that is carried out before surgical intervention. Yet, invasive cardiac diagnostics are full of risks, especially for young children. Decades of research has been conducted on the so called inverse problem of electrocardiography, which can be used to reconstruct Heart Surface Potentials (HSPs) from Body Surface Potentials (BSPs), for non-invasive diagnostics. State of the art solutions to the inverse problem are unsatisfactory, since the inverse problem is known to be ill-posed. In this paper we propose a novel approach to reconstructing HSPs from BSPs using a Time-Delay Artificial Neural Network (TDANN). We first design the TDANN architecture, and then develop an iterative search space algorithm to find the parameters of the TDANN, which results in the best overall HSP prediction. We use real-world recorded BSPs and HSPs from individuals suffering from serious cardiac conditions to validate our TDANN. The results are encouraging, in that coefficients obtained by correlating the predicted HSP with the recorded patient' HSP approach ideal values.

cs.LG↗

arXiv2017

An intracardiac electrogram model to bridge virtual hearts and implantable cardiac devices

Virtual heart models have been proposed to enhance the safety of implantable cardiac devices through closed loop validation. To communicate with a virtual heart, devices have been driven by cardiac signals at specific sites. As a result, only the action potentials of these sites are sensed. However, the real device implanted in the heart will sense a complex combination of near and far-field extracellular potential signals. Therefore many device functions, such as blanking periods and refractory periods, are designed to handle these unexpected signals. To represent these signals, we develop an intracardiac electrogram (IEGM) model as an interface between the virtual heart and the device. The model can capture not only the local excitation but also far-field signals and pacing afterpotentials. Moreover, the sensing controller can specify unipolar or bipolar electrogram (EGM) sensing configurations and introduce various oversensing and undersensing modes. The simulation results show that the model is able to reproduce clinically observed sensing problems, which significantly extends the capabilities of the virtual heart model in the context of device validation.

eess.SY↗

arXiv2016

Towards the Emulation of the Cardiac Conduction System for Pacemaker Testing

The heart is a vital organ that relies on the orchestrated propagation of electrical stimuli to coordinate each heart beat. Abnormalities in the heart's electrical behaviour can be managed with a cardiac pacemaker. Recently, the closed-loop testing of pacemakers with an emulation (real-time simulation) of the heart has been proposed. An emulated heart would provide realistic reactions to the pacemaker as if it were a real heart. This enables developers to interrogate their pacemaker design without having to engage in costly or lengthy clinical trials. Many high-fidelity heart models have been developed, but are too computationally intensive to be simulated in real-time. Heart models, designed specifically for the closed-loop testing of pacemakers, are too abstract to be useful in the testing of physical pacemakers. In the context of pacemaker testing, this paper presents a more computationally efficient heart model that generates realistic continuous-time electrical signals. The heart model is composed of cardiac cells that are connected by paths. Significant improvements were made to an existing cardiac cell model to stabilise its activation behaviour and to an existing path model to capture the behaviour of continuous electrical propagation. We provide simulation results that show our ability to faithfully model complex re-entrant circuits (that cause arrhythmia) that existing heart models can not.

eess.SY↗

arXiv2015

A synchronous rendering of hybrid systems for designing Plant-on-a-Chip (PoC)

Hybrid systems are discrete controllers that are used for controlling a physical process (plant) exhibiting continuous dynamics. A hybrid automata (HA) is a well known and widely used formal model for the specification of such systems. While many methods exist for simulating hybrid automata, there are no known approaches for the automatic code generation from HA that are semantic preserving. If this were feasible, it would enable the design of a plant-on-a-chip (PoC) system that could be used for the emulation of the plant to validate discrete controllers. Such an approach would need to be mathematically sound and should not rely on numerical solvers. We propose a method of PoC design for plant emulation, not possible before. The approach restricts input/output (I/O) HA models using a set of criteria for well-formedness which are statically verified. Following verification, we use an abstraction based on a synchronous approach to facilitate code generation. This is feasible through a sound transformation to synchronous HA. We compare our method (the developed tool called Piha) to the widely used Simulink R simulation framework and show that our method is superior in both execution time and code size. Our approach to the PoC problem paves the way for the emulation of physical plants in diverse domains such as robotics, automation, medical devices, and intelligent transportation systems.

cs.FL↗