Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking

TL;DR

This paper explores the use of the HASL formalism to analyze and characterize stochastic oscillators, leveraging its expressive power for formal verification of oscillatory behaviors.

Contribution

It demonstrates how HASL can be applied to define and evaluate properties of stochastic oscillators, providing a novel approach for formal analysis.

Findings

HASL effectively characterizes stochastic oscillator behaviors

The approach offers detailed insights into oscillatory trends

Formal verification of oscillators is enhanced using HASL

Abstract

The application of formal methods to the analysis of stochastic oscillators has been at the focus of several research works in recent times. In this paper we provide insights on the application of an expressive temporal logic formalism, namely the Hybrid Automata Stochastic Logic (HASL), to that issue. We show how one can take advantage of the expressive power of the HASL logic to define and assess relevant characteristics of (stochastic) oscillators.