Synthesis of Distributed Control and Communication Schemes from Global LTL Specifications

被引:0
|
作者
Chen, Yushan [1 ]
Ding, Xu Chu [2 ]
Belta, Calin [2 ]
机构
[1] Boston Univ, Dept Elect & Comp Engn, Boston, MA 02215 USA
[2] Boston Univ, Dept Mech Engn, Boston, MA 02215 USA
来源
2011 50TH IEEE CONFERENCE ON DECISION AND CONTROL AND EUROPEAN CONTROL CONFERENCE (CDC-ECC) | 2011年
关键词
ABSTRACTIONS;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We introduce a technique for synthesis of control and communication strategies for a team of agents from a global task specification given as a Linear Temporal Logic (LTL) formula over a set of properties that can be satisfied by the agents. We consider a purely discrete scenario, in which the dynamics of each agent is modeled as a finite transition system. The proposed computational framework consists of two main steps. First, we extend results from concurrency theory to check whether the specification is distributable among the agents. Second, we generate individual control and communication strategies by using ideas from LTL model checking. We apply the method to automatically deploy a team of miniature cars in our Robotic Urban-Like Environment.
引用
收藏
页码:2718 / 2723
页数:6
相关论文
共 50 条
  • [21] Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
    Pruekprasert, Sasinee
    Eberhart, Clovis
    Dubut, Jeremy
    2021 60TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2021, : 1321 - 1328
  • [22] From asynchronous to synchronous specifications for distributed program synthesis
    Bernet, Julien
    Janin, David
    SOFSEM 2008: THEORY AND PRACTICE OF COMPUTER SCIENCE, 2008, 4910 : 162 - 173
  • [23] LTL f synthesis under environment specifications for reachability and safety properties
    Aminof, Benjamin
    De Giacomo, Giuseppe
    Di Stasio, Antonio
    Francon, Hugo
    Rubin, Sasha
    Zhu, Shufang
    INFORMATION AND COMPUTATION, 2025, 303
  • [24] Decomposition of Multi-Agent Planning under Distributed Motion and Task LTL Specifications
    Tumova, Jana
    Dimarogonas, Dimos V.
    2015 54TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2015, : 7448 - 7453
  • [25] Automated Synthesis of Low-rank Control Systems from sc-LTL Specifications using Tensor-Train Decompositions
    Alora, John Irvin
    Gorodetsky, Alex
    Karaman, Sertac
    Marzouk, Youssef
    Lowry, Nathan
    2016 IEEE 55TH CONFERENCE ON DECISION AND CONTROL (CDC), 2016, : 1131 - 1138
  • [26] Organising LTL monitors over distributed systems with a global clock
    Christian Colombo
    Yliès Falcone
    Formal Methods in System Design, 2016, 49 : 109 - 158
  • [27] SYNTHESIS OF PROTOCOL SPECIFICATIONS FROM SERVICE SPECIFICATIONS OF DISTRIBUTED SYSTEMS IN A MARKED GRAPH MODEL
    YAMAGUCHI, H
    OKANO, K
    HIGASHINO, T
    TANIGUCHI, K
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1994, E77A (10) : 1623 - 1633
  • [28] Organising LTL monitors over distributed systems with a global clock
    Colombo, Christian
    Falcone, Ylies
    FORMAL METHODS IN SYSTEM DESIGN, 2016, 49 (1-2) : 109 - 158
  • [29] Organising LTL Monitors over Distributed Systems with a Global Clock
    Colombo, Christian
    Falcone, Ylies
    RUNTIME VERIFICATION, RV 2014, 2014, 8734 : 140 - 155
  • [30] Organising LTL monitors over distributed systems with a global clock
    Colombo, Christian
    Falcone, Yliès
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8734 : 140 - 155