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. California Institute of Technology , Pasadena, CA. (Unpublished) http://resolver.caltech.edu/CaltechCDSTR:2016.003

[img] PDF - Submitted Version
Creative Commons Attribution Non-commercial No Derivatives.

224Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCDSTR:2016.003

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:Report or Paper (Technical Report)
Related URLs:
URLURL TypeDescription
http://dx.doi.org/10.1109/ACC.2016.7525009DOIConference Paper
http://resolver.caltech.edu/CaltechAUTHORS:20160801-165143151Related ItemArticle
https://github.com/johnyf/contract_makerRelated ItemSoftware Implementation
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email Address:jfilippidis@gmail.com
Additional Information:This work was supported by STARnet, a Semiconductor Research Corporation program, sponsored by MARCO and DARPA.
Group:Control and Dynamical Systems Technical Reports
Funders:
Funding AgencyGrant Number
TerraSwarmUNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
STARnetUNSPECIFIED
Record Number:CaltechCDSTR:2016.003
Persistent URL:http://resolver.caltech.edu/CaltechCDSTR:2016.003
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:67862
Collection:CaltechCDSTR
Deposited By: Ioannis Filippidis
Deposited On:07 Jul 2016 04:09
Last Modified:23 Mar 2017 17:19

Repository Staff Only: item control page