Comparing Asynchronous $l$-Complete Approximations and Quotient Based Abstractions

TL;DR

This paper compares two abstraction techniques, quotient based abstractions and asynchronous l-complete approximations, for creating finite state models in hybrid system controller synthesis, highlighting their differences and conditions for equivalence.

Contribution

It provides a detailed comparison of QBA and SAlCA, establishing conditions for their equivalence and showing they are generally incomparable.

Findings

QBA and SAlCA are generally incomparable in behavior and similarity.

Necessary and sufficient conditions for their equivalence are derived.

Either QBA or SAlCA can produce a tighter abstraction depending on the system.

Abstract

This paper is concerned with a detailed comparison of two different abstraction techniques for the construction of finite state symbolic models for controller synthesis of hybrid systems. Namely, we compare quotient based abstractions (QBA), with different realizations of strongest (asynchronous) $l$-complete approximations (SAlCA) Even though the idea behind their construction is very similar, we show that they are generally incomparable both in terms of behavioral inclusion and similarity relations. We therefore derive necessary and sufficient conditions for QBA to coincide with particular realizations of SAlCA. Depending on the original system, either QBA or SAlCA can be a tighter abstraction.