Towards an Approximate Conformance Relation for Hybrid I/O Automata

TL;DR

This paper introduces an approximate conformance relation for hybrid I/O automata that unifies existing notions, enabling comparison of discrete actions and continuous trajectories, and supports step-wise conformance proofs.

Contribution

It proposes a new approximate conformance notion that combines previous concepts and proves its semi-transitivity, facilitating incremental verification of hybrid systems.

Findings

The new conformance relation unifies discrete and continuous behavior comparison.

It satisfies semi-transitivity, enabling step-wise conformance reasoning.

The approach consolidates earlier notions into a single, more flexible framework.

Abstract

Several notions of conformance have been proposed for checking the behavior of cyber-physical systems against their hybrid systems models. In this paper, we explore the initial idea of a notion of approximate conformance that allows for comparison of both observable discrete actions and (sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely the notion of Hybrid Input-Output Conformance (HIOCO) by M. van Osch and the notion of Hybrid Conformance by H. Abbas and G.E. Fainekos. We prove that our proposed notion of conformance satisfies a semi-transitivity property, which makes it suitable for a step-wise proof of conformance or refinement.