Browse wiki

From MurrayWiki
Jump to: navigation, search
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 assume-guarantee 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 fm16-acc  +
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/fm16-acc.pdf  +
hide properties that link here 
Symbolic construction of GR(1) contracts for systems with full information + Title
 

 

Enter the name of the page to start browsing from.