Browse wiki
From MurrayWiki
Symbolic construction of GR(1) contracts for systems with full information 
Abstract 
This work proposes a symbolic algorithm fo … This work proposes a symbolic algorithm for the construction of assumeguarantee specifications that allow multiple agents to coop erate. Each agent is assigned goals expressed in a fragment of linear temporal logic known as gener alized 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 con tract 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 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. and linear in number of recurrence goals. +


Authors  Ioannis Filippidis and Richard M. Murray + 
Flags  NCS + 
Funding  The TerraSwarm Research Center + 
ID  2015h + 
Source  2016 American Control Conference (ACC) + 
Tag  fm16acc + 
Title  Symbolic construction of GR(1) contracts for systems with full information + 
Type  Conference Paper + 
Categories  Papers 
Modification date This property is a special property in this wiki.

10 June 2016 06:06:52 + 
URL This property is a special property in this wiki.

http://www.cds.caltech.edu/~murray/preprints/fm16acc.pdf + 
show properties that link here 