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.

[img] PDF - Submitted Version
See Usage Policy.


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:Book Section
Related URLs:
URLURL TypeDescription Paper ItemTechnical Report
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.
Funding AgencyGrant Number
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Record Number:CaltechAUTHORS:20160801-165143151
Persistent URL:
Official Citation:I. Filippidis and R. M. Murray, "Symbolic construction of GR(1) contracts for systems with full information," 2016 American Control Conference (ACC), Boston, MA, 2016, pp. 782-789. doi: 10.1109/ACC.2016.7525009
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:69367
Deposited On:02 Aug 2016 18:16
Last Modified:11 Nov 2021 04:13

Repository Staff Only: item control page