A weakness measure for GR(1) formulae
File(s)main.pdf (461 KB)
Submitted version
Author(s)
Cavezza, D
Alrajeh, D
Gyorgy, A
Type
Conference Paper
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.
Date Issued
2018-07-12
Date Acceptance
2018-04-09
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
110
End Page
128
Journal / Book Title
Lecture Notes in Computer Science
Volume
10951
Copyright Statement
© 2018 Springer International Publishing AG, part of Springer Nature. The final authenticated version is available online at https://doi.org/10.1007/978-3-319-95582-7_7
Source Database
manual-entry
Source
22nd International Symposium on Formal Methods
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
ASSUMPTIONS
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2018-07-15
Finish Date
2018-07-17
Country
Oxford, UK
Date Publish Online
2018-07-12