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)

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


Use this Persistent URL to link to this item:


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 Paper ItemArticle ItemSoftware Implementation
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email
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
Funding AgencyGrant Number
Semiconductor Research CorporationUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Record Number:CaltechCDSTR:2016.003
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:67862
Deposited By: Ioannis Filippidis
Deposited On:07 Jul 2016 04:09
Last Modified:11 Nov 2021 03:55

Repository Staff Only: item control page