CaltechAUTHORS
  A Caltech Library Service

Symbolic construction of GR(1) contracts for systems with full information

Filippidis, Ioannis and Murray, Richard M. (2016) Symbolic construction of GR(1) contracts for systems with full information. In: 2016 American Control Conference (ACC). IEEE , Piscataway, NJ, pp. 782-789. ISBN 978-1-4673-8680-7 . http://resolver.caltech.edu/CaltechAUTHORS:20160801-165143151

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20160801-165143151

Abstract

This work proposes a symbolic algorithm for the construction of assume-guarantee specifications that allow multiple agents to cooperate. Each agent is assigned goals expressed in a fragment of linear temporal logic known as generalized Streett with one pair, GR(1). These goals may be unrealizable, unless each agent makes additional assumptions, about the behavior of other agents. The algorithm constructs a contract among the agents, in that only the infinite behavior of the given goals is constrained, known as liveness, not the finite one, known as safety. This defers synthesis to a later stage of refinement, modularizing the design process. We prove that there exist GR(1) games that do not admit any refining GR(1) contract. For this reason, we formulate contracts with nested GR(1) properties and auxiliary communication variables, and prove that they always exist. The algorithm's fixpoint structure is similar to GR(1) synthesis, enjoying time complexity polynomial in the number of states, and linear in number of recurrence goals.


Item Type:Book Section
Related URLs:
URLURL TypeDescription
http://dx.doi.org/10.1109/ACC.2016.7525009DOIArticle
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7525009PublisherArticle
http://resolver.caltech.edu/CaltechCDSTR:2016.003Related ItemTechnical Report
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2016 IEEE. This work was supported by STARnet, a Semiconductor Research Corporation program, sponsored by MARCO and DARPA.
Funders:
Funding AgencyGrant Number
STARnetUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO) UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Record Number:CaltechAUTHORS:20160801-165143151
Persistent URL:http://resolver.caltech.edu/CaltechAUTHORS:20160801-165143151
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:69367
Collection:CaltechAUTHORS
Deposited By: Kristin Buxton
Deposited On:02 Aug 2016 18:16
Last Modified:23 Mar 2017 17:18

Repository Staff Only: item control page