Robust Multi-Agent Coordination from CaTL Speciﬁcations Wenliang Liu1 Kevin Leahy2 Zachary Serlin2 Calin Belta1 Abstract We consider the problem of controlling a het-

2025-05-03 0 0 1.46MB 8 页 10玖币

侵权投诉

Robust Multi-Agent Coordination from CaTL+ Speciﬁcations

Wenliang Liu1, Kevin Leahy2, Zachary Serlin2, Calin Belta1

Abstract— We consider the problem of controlling a het-

erogeneous multi-agent system required to satisfy temporal

logic requirements. Capability Temporal Logic (CaTL) was

recently proposed to formalize such speciﬁcations for deploying

a team of autonomous agents with different capabilities and

cooperation requirements. In this paper, we extend CaTL to a

new logic CaTL+, which is more expressive than CaTL and has

semantics over a continuous workspace shared by all agents. We

deﬁne two novel robustness metrics for CaTL+: the traditional

robustness and the exponential robustness. The latter is sound,

differentiable almost everywhere and eliminates masking, which

is one of the main limitations of the traditional robustness

metric. We formulate a control synthesis problem to maximize

CaTL+ robustness and propose a two-step optimization method

to solve this problem. Simulation results are included to

illustrate the increased expressivity of CaTL+ and the efﬁcacy

of the proposed control synthesis approach.

I. INTRODUCTION

Due to their expressivity and similarity to natural lan-

guages, temporal logics, such as Linear Temporal Logic

(LTL) [1] and Signal Temporal Logic (STL) [2], have been

widely used to formalize speciﬁcations for control systems.

Many recent works proposed methodologies to generate

control strategies for dynamical systems from such speciﬁca-

tions. Roughly, these works can be grouped in two categories.

For speciﬁcations given in LTL and fragments of LTL,

abstractions and automata-based synthesis have been shown

to work for certain classes of systems with low-dimensional

state spaces [3]. For temporal logics with semantics over

real-valued signals, such as STL, control synthesis can be

formulated as an optimization problem, which can be solved

via Mixed Integer Programming (MIP) [4] or gradient-based

methods [5], [6].

Planning and controlling multi-agent systems from tempo-

ral logic speciﬁcations is a challenging problem that received

a lot of attention in recent years. In [7], the authors used dis-

tributed formal synthesis to allocate global task speciﬁcations

expressed as LTL formulas to locally interacting agents with

ﬁnite dynamics. Related works [8]–[10] proposed extensions

to more realistic models and scenarios. The authors of

This work was partially supported by the NSF under grant IIS-2024606.

DISTRIBUTION STATEMENT A. Approved for public release. Distri-

bution is unlimited. This material is based upon work supported by the

Under Secretary of Defense for Research and Engineering under Air Force

Contract No. FA8702-15-D-0001. Any opinions, ﬁndings, conclusions or

recommendations expressed in this material are those of the author(s) and

do not necessarily reﬂect the views of the Under Secretary of Defense for

Research and Engineering.

1Wenliang Liu and Calin Belta are with Boston University, Boston, MA,

USA wliu97@bu.edu, cbelta@bu.edu

2Kevin Leahy and Zachary Serlin are with MIT Lincoln Labora-

tory, Lexington MA 02421, USA kevin.leahy@ll.mit.edu,

zachary.serlin@ll.mit.edu

[11] used STL and Spatial Temporal Reach and Escape

Logic (STREL) as speciﬁcation languages to capture the

connectivity constraints of a multi-robot team.

The above approaches do not scale for large teams. Very

recent work has focused on development of logics and

synthesis algorithms speciﬁcally tailored for such situations.

The authors of [12] proposed Counting LTL (cLTL), which

is used to deﬁne tasks for large groups of identical agents.

Counting constraints specify the number of agents that need

to achieve a certain goal. As long as enough agents achieve

the goal, it does not matter which speciﬁc subgroup does

that. Similar ideas are used in Capability Temporal Logic

(CaTL) [13]. The atomic unit of a CaTL formula is a task,

which speciﬁes the number of agents with certain capability

that need to reach some region and stay there for some

time. Since agents can have different capabilities, CaTL is

appropriate for heterogeneous teams. Unlike cLTL, CaTL is a

fragment of STL, and allows for concrete time requirements.

The expressivities of both cLTL and CaTL are limited by

the deﬁnition of counting constraints and tasks, respectively.

For example, neither cLTL nor CaTL can require that “3

agents eventually reach region A” without requiring that the

3agents reach region A at the same time. This can be

restrictive. Consider, for example, a disaster relief scenario,

where a team of robots needs to deliver supplies to an

affected area. We require that enough supplies be delivered,

i.e., enough robots eventually reach the affected area, rather

than enough robots stay in the affected area at the same

time. In fact, a robot is supposed to go on to the next task

after drop off the supply without waiting for the other robots.

To solve this problem, an extension of cLTL, called cLTL+,

was proposed in [14], where a two-layer LTL structure was

deﬁned. However, cLTL+ can not specify concrete time

requirements. To address this limitation, we extend CaTL

to a novel logic called CaTL+, which has a two-layer

structure similar to cLTL+. The authors of [15] extended STL

with integral predicates, which also enables asynchronous

satisfaction, but it can only specify how many times a service

is needed. A CaTL+ task can specify the number of agents

that need to satisfy an arbitrary STL formula. Another related

work is CensusSTL [16], which is also a two-layer STL

that refers to mutually exclusive subsets of a group, rather

than capabilities of agents. Also, [16] focuses on inference

of formulas from data, rather than control synthesis.

CaTL has both qualitative semantics, i.e., a speciﬁcation

is satisﬁed or violated, and quantitative semantics (known

as robustness), which deﬁnes how much a speciﬁcation is

satisﬁed. The robustness of CaTL is an integer representing

the minimum number of agents that can be removed from

arXiv:2210.01732v2 [eess.SY] 12 Apr 2023

(added to) a given team in order to invalidate (satisfy) the

given formula. Such a robustness metric is discontinuous

and cannot represent how strongly each task is satisﬁed.

In this paper, for the new logic CaTL+, we deﬁne two

new quantitative semantics, called traditional robustness and

exponential robustness. Both are continuous with respect to

their inputs and can measure how strongly a task is satisﬁed.

A higher robustness indicates more agents reach the region

and stay closer to the center for a longer time. Similar to

the traditional robustness of STL [17], the new traditional

robustness only takes into account the most satisfaction or

violation point, and ignores all other points, which is called

masking. The proposed exponential robustness eliminates

masking by considering all subformulas, all time points

and all agents, which makes the control synthesis from

CaTL+ easier and the result more robust. This new deﬁnition

also includes a novel robustness for STL, which has the

strongest mask-eliminating property in promise of soundness

compared with existing STL robustness metrics.

We also formulate and solve a centralized control synthesis

problem from CaTL+. Control synthesis for cLTL [12],

cLTL+ [14], CaTL [13] and STL with integral predicates [15]

are solved in a graph environment using a (mixed) Integer

Linear Program (ILP), where the controls are transitions

between vertices in a graph. In this paper, we consider a

continuous workspace shared by all agents. Each agent has

its own discrete time dynamics with continuous state and

control spaces. We propose a two-step optimization: a global

optimization followed by a gradient-based local optimization

to obtain the controls that maximize CaTL+ robustness.

The contribution of this paper is threefold. First, we

extend CaTL to CaTL+, which is more expressive and works

for continuous environments. Second, we deﬁne two kinds

of robustness functions for CaTL+: the traditional and the

exponential robustness. The latter is differentiable almost

everywhere and eliminates masking, which makes it suitable

for gradient-based optimization. This new deﬁnition also

includes a novel STL robustness metric. Third, we propose a

two-step optimization strategy for CaTL+ control synthesis.

The resulting controls steer the system to satisfy the given

speciﬁcation robustly according to the simulation results.

II. SYSTEM MODEL AND NOTATION

Let |S| be the cardinality of a set S. We use bold symbols

to represent trajectories and calligraphic symbols for sets. For

z∈R, we deﬁne [z]+= max{0, z}and [z]−=−[−z]+.

Consider a team of agents labelled from a ﬁnite set J. Let

Cap denote a ﬁnite set of agent capabilities. We assume that

the agents operate in a continuous workspace S ⊆ Rns.

Deﬁnition 1. An agent j∈ J is a tuple Aj=

hXj, xj(0), Capj,Uj, fj, ljiwhere: Xj⊆Rnx,j is its state

space; xj(0) ∈ Xjis its initial state; Capj⊆Cap is its

ﬁnite set of capabilities; Uj⊆Rnu,j is its control space;

fj:Xj× Uj→ Xjis a differentiable function giving the

discrete time dynamics of agent j:

xj(t+ 1) = fjxj(t), uj(t), t = 0,1, . . . , H −1,(1)

Fig. 1: An earthquake emergency

response scenario. Mis the entire

square workspace. Initaand Initg

are the initial regions for the aerial

and ground vehicles. Cis where

the agents pick up supplies. Bis

a bridge and the 2rectangles R

correspond to the river. V1and V2

are 2affected villages.

where xj(t)and uj(t)are the state and control at time t,

His a ﬁnite time horizon determined by the task (detailed

later); lj:Xj→ S is a differentiable function that maps the

state of agent jto a point in the workspace shared by all

agents (this enables heterogeneous state spaces):

sj(t) = ljxj(t), t = 0,1, . . . , H. (2)

The trajectory of an agent j, called an individual trajec-

tory, is a sequence sj=sj(0) . . . sj(H). We assume that

∪j∈J Capj=Cap.

Given a team of agents {Aj}j∈J , the team trajectory

is deﬁned as a set of pairs S={(sj, Capj)}j∈J , which

captures all the individual trajectories with the corresponding

capabilities. Let Jc={j|c∈Capj}be the set of agent

indices with capability c. Let uj=uj(0) . . . uj(H−1) be

the sequence of controls for agent j.

Example. Consider an earthquake emergency response sce-

nario. The workspace S ⊂ R2is shown in Fig. 1. There are

4ground vehicles j∈ {1,2,3,4}and 2aerial vehicles j∈

{5,6}, totaling 6robots indexed from J={1,2,3,4,5,6}

in the workspace. A river Rruns through this area and

a bridge Bgoes across the river. All ground vehicles are

identical. The dynamics fj,j∈ {1,2,3,4}are given by

px,j (t+ 1) = px,j (t) + vj(t) cos θj(t),

py,j (t+ 1) = py,j (t) + vj(t) sin θj(t),

θj(t+ 1) = θj(t) + ωj(t),

(3)

where the state xjis the 2D position and orientation

[px,j py,j θj], the control ujis the forward and angular

speed [vjωj], the state space Xj=Xg⊂R3, the

control space Uj=Ug⊂R2, the initial state xj(0) is a

singleton randomly sampled in region Initgwith randomly

sampled orientation θj∈[1

4π, 3

4π]. The function lj(xj) =

[px,j py,j ] = sjmaps the state of agent jto a position

in the workspace S. The identical capabilities are given by

Capj={“Delivery”,“Ground”},j∈ {1,2,3,4}. All the

aerial vehicles are identical. For j∈ {5,6},fjare given by

px,j (t+ 1) = px,j (t) + vx,j (t),

py,j (t+ 1) = py,j (t) + vy,j (t),(4)

where the state xjis the 2D position [px,j py,j ], the control

ujis the speed [vx,j vy,j ], the state space Xj=Xa⊂R2,

the control space Uj=Ua⊂R2, the initial state xj(0)

is a singleton randomly sampled in the region Inita, the

identity mapping lj(xj) = xj=sjmaps the state of agent

jto a position in S. The identical capabilities are given

by Capj={“Delivery”,“Inspection”},j∈ {5,6}. For

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

RobustMulti-AgentCoordinationfromCaTL+SpecicationsWenliangLiu1,KevinLeahy2,ZacharySerlin2,CalinBelta1AbstractWeconsidertheproblemofcontrollingahet-erogeneousmulti-agentsystemrequiredtosatisfytemporallogicrequirements.CapabilityTemporalLogic(CaTL)wasrecentlyproposedtoformalizesuchspecicationsforde...

展开>> 收起<<

Robust Multi-Agent Coordination from CaTL Speciﬁcations Wenliang Liu1 Kevin Leahy2 Zachary Serlin2 Calin Belta1 Abstract We consider the problem of controlling a het-.pdf

共8页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Robust Multi-Agent Coordination from CaTL Speciﬁcations Wenliang Liu1 Kevin Leahy2 Zachary Serlin2 Calin Belta1 Abstract We consider the problem of controlling a het-

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: