标题： STL-GO：具有图运算符的时空逻辑用于具有多种网络拓扑的分布式系统 显示英文标题

标题： STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies

摘要： 多智能体系统（MASs）由多个自主代理组成，这些代理通过通信、协调和共同感知环境来完成复杂任务，在机器人技术、智慧城市和物联网应用等多种应用中都可以找到。 建模和监控MAS需求以保证整体任务目标、安全性和可靠性是一个重要问题。 这些需求隐式地要求对代理之间的各种传感和通信模式进行推理，分析代理任务之间的依赖关系，以及代理之间的空间或虚拟距离。 为了捕捉这种丰富的MAS需求，我们通过多个有向图对代理交互进行建模，并引入一种新的逻辑——带图运算符的时空逻辑（STL-GO）。 STL-GO的关键创新是图运算符，它们使我们能够推理出在底层交互图的入边或出边上满足感兴趣属性的代理数量；例如，要求一个代理应感知至少两个相邻代理，其任务图表明具有协作能力。 然后，我们提出了用于单个代理的新分布式监控条件，这些条件仅使用局部信息来确定是否满足STL-GO规范。 我们将STL-GO的表达能力与现有的时空逻辑形式化方法进行了比较，并在共享单车和多无人机案例研究中展示了STL-GO和我们的分布式监控器的实用性。 显示英文摘要

摘要： Multi-agent systems (MASs) consisting of a number of autonomous agents that communicate, coordinate, and jointly sense the environment to achieve complex missions can be found in a variety of applications such as robotics, smart cities, and internet-of-things applications. Modeling and monitoring MAS requirements to guarantee overall mission objectives, safety, and reliability is an important problem. Such requirements implicitly require reasoning about diverse sensing and communication modalities between agents, analysis of the dependencies between agent tasks, and the spatial or virtual distance between agents. To capture such rich MAS requirements, we model agent interactions via multiple directed graphs, and introduce a new logic -- Spatio-Temporal Logic with Graph Operators (STL-GO). The key innovation in STL-GO are graph operators that enable us to reason about the number of agents along either the incoming or outgoing edges of the underlying interaction graph that satisfy a given property of interest; for example, the requirement that an agent should sense at least two neighboring agents whose task graphs indicate the ability to collaborate. We then propose novel distributed monitoring conditions for individual agents that use only local information to determine whether or not an STL-GO specification is satisfied. We compare the expressivity of STL-GO against existing spatio-temporal logic formalisms, and demonstrate the utility of STL-GO and our distributed monitors in a bike-sharing and a multi-drone case study.