Asynchronous Correspondences Between Hybrid Trajectory Semantics

TL;DR

This paper formalizes hybrid system semantics as sets of trajectories, explores various abstraction methods including Galois connections, and examines the challenges of trace-based composition for verification and analysis.

Contribution

It introduces a unified framework for hybrid trajectory semantics and analyzes both stepwise and non-stepwise abstractions, including their composition issues.

Findings

Galois connections effectively relate concrete and abstract hybrid semantics.

Abstractions based on state correspondences like bisimulations are formalized.

Trace-based composition of abstractions presents significant challenges.

Abstract

We formalize the semantics of hybrid systems as sets of hybrid trajectories, including those generated by an hybrid transition system. We study the abstraction of hybrid trajectory semantics for verification, static analysis, and refinement. We mainly consider abstractions of hybrid semantics which establish a correspondence between trajectories derived from a correspondence between states such as homomorphisms, simulations, bisimulations, and preservations with progress. We also consider abstractions that cannot be defined stepwise like discretization. All these abstractions are Galois connections between concrete and abstract hybrid trajectory or discrete trace semantics. In contrast to semantic based abstractions, we investigate the problematic trace-based composition of abstractions.