Decoupled formal synthesis for almost separable systems with temporal logic specifications
- Creators
- Livingston, Scott C.
- Prabhakar, Pavithra
- Others:
- Chong, Nak-Young
- Cho, Young-Jo
Abstract
We consider the problem of synthesizing controllers automatically for distributed robots that are loosely coupled using a formal synthesis approach. Formal synthesis entails construction of game strategies for a discrete transition system such that the system under the strategy satisfies a specification, given for instance in linear temporal logic (LTL). The general problem of automated synthesis for distributed discrete transition systems suffers from state-space explosion because the combined state-space has size exponential in the number of subsystems. Motivated by multi-robot motion planning problems, we focus on distributed systems whose interaction is nearly decoupled, allowing the overall specification to be decomposed into specifications for individual subsystems and a specification about the joint system. We treat specifically reactive synthesis for the GR(1) fragment of LTL. Each robot is subject to a GR(1) formula, and a safety formula describes constraints on their interaction. We propose an approach wherein we synthesize strategies independently for each subsystem; then we patch the separate controllers around interaction regions such that the specification about the joint system is satisfied.
Additional Information
© 2016 Springer Japan. Part of this work was done while the first author was visiting IMDEA in Madrid, Spain, during summer 2013.Attached Files
Accepted Version - Livingston-Prabhakar-DARS2014.pdf
Files
Name | Size | Download all |
---|---|---|
md5:2fe73eeec24042becdee0a50bdaca467
|
208.3 kB | Preview Download |
Additional details
- Eprint ID
- 53155
- Resolver ID
- CaltechAUTHORS:20141231-105326855
- Created
-
2015-01-06Created from EPrint's datestamp field
- Updated
-
2021-11-10Created from EPrint's last_modified field
- Series Name
- Springer Tracts in Advanced Robotics
- Series Volume or Issue Number
- 112