Automatic synthesis of multi-agent motion tasks based on LTL specifications

Savvas G. Loizou; Kostas J. Kyriakopoulos

doi:10.1109/cdc.2004.1428622

Automatic synthesis of multi-agent motion tasks based on LTL specifications

Savvas G. Loizou, Kostas J. Kyriakopoulos

Electrical Engineering

Research output: Contribution to journal › Conference article › peer-review

Abstract

In this paper we propose a methodology for automatically synthesizing motion task controllers based on Linear Temporal Logic (LTL) specifications. The proposed design of the underlying multi-agent controllers possess a special structure that allows for implicit satisfaction of basic liveness and safety specifications. The resulting closed loop system is of hybrid nature combining the continuous dynamics of the underlying system with the automatically synthesized switching logic that enforces the LTL specification. The effectiveness of the proposed scheme is verified through non-trivial computer simulations.

Original language	English (US)
Article number	TuA05.2
Pages (from-to)	153-158
Number of pages	6
Journal	Proceedings of the IEEE Conference on Decision and Control
Volume	1
DOIs	https://doi.org/10.1109/cdc.2004.1428622
State	Published - 2004
Event	2004 43rd IEEE Conference on Decision and Control (CDC) - Nassau, Bahamas Duration: Dec 14 2004 → Dec 17 2004

ASJC Scopus subject areas

Control and Systems Engineering
Modeling and Simulation
Control and Optimization

Access to Document

10.1109/cdc.2004.1428622

Cite this

@article{b25b658fa70c4106b77bd1f7247579ee,

title = "Automatic synthesis of multi-agent motion tasks based on LTL specifications",

abstract = "In this paper we propose a methodology for automatically synthesizing motion task controllers based on Linear Temporal Logic (LTL) specifications. The proposed design of the underlying multi-agent controllers possess a special structure that allows for implicit satisfaction of basic liveness and safety specifications. The resulting closed loop system is of hybrid nature combining the continuous dynamics of the underlying system with the automatically synthesized switching logic that enforces the LTL specification. The effectiveness of the proposed scheme is verified through non-trivial computer simulations.",

author = "Loizou, {Savvas G.} and Kyriakopoulos, {Kostas J.}",

year = "2004",

doi = "10.1109/cdc.2004.1428622",

language = "English (US)",

volume = "1",

pages = "153--158",

journal = "Proceedings of the IEEE Conference on Decision and Control",

issn = "0743-1546",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

note = "2004 43rd IEEE Conference on Decision and Control (CDC) ; Conference date: 14-12-2004 Through 17-12-2004",

}

TY - JOUR

T1 - Automatic synthesis of multi-agent motion tasks based on LTL specifications

AU - Loizou, Savvas G.

AU - Kyriakopoulos, Kostas J.

PY - 2004

Y1 - 2004

N2 - In this paper we propose a methodology for automatically synthesizing motion task controllers based on Linear Temporal Logic (LTL) specifications. The proposed design of the underlying multi-agent controllers possess a special structure that allows for implicit satisfaction of basic liveness and safety specifications. The resulting closed loop system is of hybrid nature combining the continuous dynamics of the underlying system with the automatically synthesized switching logic that enforces the LTL specification. The effectiveness of the proposed scheme is verified through non-trivial computer simulations.

AB - In this paper we propose a methodology for automatically synthesizing motion task controllers based on Linear Temporal Logic (LTL) specifications. The proposed design of the underlying multi-agent controllers possess a special structure that allows for implicit satisfaction of basic liveness and safety specifications. The resulting closed loop system is of hybrid nature combining the continuous dynamics of the underlying system with the automatically synthesized switching logic that enforces the LTL specification. The effectiveness of the proposed scheme is verified through non-trivial computer simulations.

UR - http://www.scopus.com/inward/record.url?scp=14344252158&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=14344252158&partnerID=8YFLogxK

U2 - 10.1109/cdc.2004.1428622

DO - 10.1109/cdc.2004.1428622

M3 - Conference article

AN - SCOPUS:14344252158

SN - 0743-1546

VL - 1

SP - 153

EP - 158

JO - Proceedings of the IEEE Conference on Decision and Control

JF - Proceedings of the IEEE Conference on Decision and Control

M1 - TuA05.2

T2 - 2004 43rd IEEE Conference on Decision and Control (CDC)

Y2 - 14 December 2004 through 17 December 2004

ER -

Automatic synthesis of multi-agent motion tasks based on LTL specifications

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this