On a notion of entropy for reachability properties

TL;DR

This paper introduces a new concept called reachability entropy to determine the minimum data rate needed for systems to satisfy reach-while-stay specifications, establishing a fundamental lower bound and providing computational methods.

Contribution

It defines reachability entropy, proves it as a tight lower bound for data rates, and offers a numerical procedure for finite abstractions of control systems.

Findings

Reachability entropy characterizes minimal data rates for reach-while-stay specifications.

The data-rate theorem establishes entropy as a tight lower bound.

Numerical methods for upper bounds are demonstrated with examples.

Abstract

In this work, we introduce a notion of reachability entropy to characterize the smallest data rate which is sufficient enough to enforce reach-while-stay specification. We also define data rates of coder-controllers that can enforce this specification in finite time. Then, we establish the data-rate theorem which states that the reachability entropy is a tight lower bound of the data rates that allow satisfaction of the reach-while-stay specification. For a system which is related to an another system under feedback refinement relation, we show that the entropy of the former will not be larger than that of the latter. We also provide a procedure to numerically compute an upper bound of the reachability entropy for discrete-time control systems by leveraging their finite abstractions. Finally, we present some examples to demonstrate the effectiveness of the proposed results.