CaltechAUTHORS
  A Caltech Library Service

Hiding variables when decomposing specifications into GR(1) contracts

Filippidis, Ioannis and Murray, Richard M. (2017) Hiding variables when decomposing specifications into GR(1) contracts. . (Unpublished) https://resolver.caltech.edu/CaltechAUTHORS:20200131-145354147

[img] PDF - Submitted Version
See Usage Policy.

201Kb

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20200131-145354147

Abstract

We propose a method for eliminating variables from component specifications during the decomposition of GR(1) properties into contracts. The variables that can be eliminated are identified by parameterizing the communication architecture to investigate the dependence of realizability on the availability of information. We prove that the selected variables can be hidden from other components, while still expressing the resulting specification as a game with full information with respect to the remaining variables. The values of other variables need not be known all the time, so we hide them for part of the time, thus reducing the amount of information that needs to be communicated between components. We improve on our previous results on algorithmic decomposition of GR(1) properties, and prove existence of decompositions in the full information case. We use semantic methods of computation based on binary decision diagrams. To recover the constructed specifications so that humans can read them, we implement exact symbolic minimal covering over the lattice of integer orthotopes, thus deriving minimal formulae in disjunctive normal form over integer variable intervals.


Item Type:Report or Paper (Discussion Paper)
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Additional Information:Submitted, 2017 Conference on Decision and Control. In distinguishing between syntax and semantics of assume-guarantee properties we benefited from discussions with Necmiye Özay and Scott Livingston. This work was supported by STARnet, a Semiconductor Research Corporation program, sponsored by MARCO and DARPA.
Funders:
Funding AgencyGrant Number
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
STARnetUNSPECIFIED
Record Number:CaltechAUTHORS:20200131-145354147
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20200131-145354147
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:101041
Collection:CaltechAUTHORS
Deposited By: Tony Diaz
Deposited On:31 Jan 2020 23:01
Last Modified:31 Jan 2020 23:01

Repository Staff Only: item control page