A Weakness Measure for GR(1) Formulae

TL;DR

This paper introduces a new measure based on Hausdorff dimension to quantify the weakness of GR(1) formulas, improving upon existing measures like implication and entropy for better specification analysis.

Contribution

It proposes a refined weakness measure for GR(1) formulas using Hausdorff dimension, addressing limitations of previous measures like implication and entropy.

Findings

The Hausdorff dimension-based measure can distinguish weaker and stronger GR(1) formulas.

The measure is effective in computing assumptions refinements for GR(1) specifications.

Conditions are identified where this measure reliably indicates weakness.

Abstract

In spite of the theoretical and algorithmic developments for system synthesis in recent years, little effort has been dedicated to quantifying the quality of the specifications used for synthesis. When dealing with unrealizable specifications, finding the weakest environment assumptions that would ensure realizability is typically a desirable property; in such context the weakness of the assumptions is a major quality parameter. The question of whether one assumption is weaker than another is commonly interpreted using implication or, equivalently, language inclusion. However, this interpretation does not provide any further insight into the weakness of assumptions when implication does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it fails to provide a sufficiently refined notion of weakness in case of GR(1) formulae, a subset of linear temporal logic formulae which is of particular interest in controller synthesis. In this paper we propose a more refined measure of weakness based on the Hausdorff dimension, a concept that captures the notion of size of the omega-language satisfying a linear temporal logic formula. We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae. We evaluate our proposed weakness measure in the context of computing GR(1) assumptions refinements.