Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction

We present a scalable methodology to verify stochastic hybrid systems for inequality linear temporal logic (iLTL) or inequality metric interval temporal logic (iMITL). Using the Mori–Zwanzig reduction method, we construct a finite-state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. Based on this, we propose the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in iLTL or iMITL. The scalability of the proposed algorithms is demonstrated by a case study.

Age of information of a server with energy requirements

We investigate a system with Poisson arrivals to two queues. One queue stores the status updates of the process of interest (or data packets) and the other handles the energy that is required to deliver the updates to the monitor. We consider that the energy is represented by packets of discrete unit. When an update ends service, it is sent to the energy queue and, if the energy queue has one packet, the update is delivered successfully and the energy packet disappears; however, in case the energy queue is empty, the update is lost. Both queues can handle, at most, one packet and the service time of updates is exponentially distributed. Using the Stochastic Hybrid System method, we characterize the average Age of Information of this system. Due to the difficulty of the derived expression, we also explore approximations of the average Age of Information of this system.

Multiscale Tumor Modeling With Drug Pharmacokinetic and Pharmacodynamic Profile Using Stochastic Hybrid System

Effective cancer treatment strategy requires an understanding of cancer behavior and development across multiple temporal and spatial scales. This has resulted into a growing interest in developing multiscale mathematical models that can simulate cancer growth, development, and response to drug treatments. This study thus investigates multiscale tumor modeling that integrates drug pharmacokinetic and pharmacodynamic (PK/PD) information using stochastic hybrid system modeling framework. Specifically, (1) pathways modeled by differential equations are adopted for gene regulations at the molecular level; (2) cellular automata (CA) model is proposed for the cellular and multicellular scales. Markov chains are used to model the cell behaviors by taking into account the gene expression levels, cell cycle, and the microenvironment. The proposed model enables the prediction of tumor growth under given molecular properties, microenvironment conditions, and drug PK/PD profile. Simulation results demonstrate the effectiveness of the proposed approach and the results agree with observed tumor behaviors.