Avinash Malik

Weiwei Ai, Nitish Patel, Partha Roop et al.

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.

Eugene Yip, Sidharta Andalam, Partha S. Roop et al.

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.

Avinash Malik, Partha Roop

This paper presents a novel approach to including non-instantaneous discrete control transitions in the linear hybrid automaton approach to simulation and verification of hybrid control systems. In this paper we study the control of a continuously evolving analog plant using a controller programmed in a synchronous programming language. We provide extensions to the synchronous subset of the SystemJ programming language for modeling, implementation, and verification of such hybrid systems. We provide a sound rewrite semantics that approximate the evolution of the continuous variables in the discrete domain inspired from the classical supervisory control theory. The resultant discrete time model can be verified using classical model-checking tools. Finally, we show that systems designed using our approach have a higher fidelity than the ones designed using the hybrid automaton approach.

Avinash Malik, Partha Roop

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.

Partha Roop, Sobhan Chatterjee, Avinash Malik et al.

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.

Hongshen Yang, Avinash Malik

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.

Avinash Malik

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.

Ke Ren, Avinash Malik

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.

Avinash Malik, Tommy Peng, Mark Trew

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.

Avinash Malik, Partha S Roop, Sidharta Andalam et al.

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.