HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on Interval Analysis

TL;DR

HySIA is a reliable tool that uses interval analysis to simulate nonlinear hybrid automata and verify STL properties, providing precise and trustworthy results for complex hybrid systems.

Contribution

HySIA introduces a novel interval analysis-based approach for both simulation and verification of nonlinear hybrid automata and STL properties.

Findings

Successfully simulates complex hybrid automata with sharp interval enclosures

Verifies STL properties reliably using interval analysis

Demonstrates effectiveness through multiple example systems

Abstract

We present HySIA: a reliable runtime verification tool for nonlinear hybrid automata (HA) and signal temporal logic (STL) properties. HySIA simulates an HA with interval analysis techniques so that a trajectory is enclosed sharply within a set of intervals. Then, HySIA computes whether the simulated trajectory satisfies a given STL property; the computation is performed again with interval analysis to achieve reliability. Simulation and verification using HySIA are demonstrated through several example HA and STL formulas.