Distributed Synthesis of Surveillance Strategies for Mobile Sensors

TL;DR

This paper presents a decentralized method for synthesizing surveillance strategies in mobile sensor networks, ensuring global surveillance objectives are met without centralized coordination by decomposing the problem into local subgames.

Contribution

The paper introduces a novel decentralized synthesis approach for mobile sensor surveillance, reducing computational complexity and enabling independent sensor strategy generation.

Findings

Decentralized strategies guarantee global surveillance objectives.

Method reduces state space complexity compared to centralized approaches.

Case study demonstrates practical application of the synthesis method.

Abstract

We study the problem of synthesizing strategies for a mobile sensor network to conduct surveillance in partnership with static alarm triggers. We formulate the problem as a multi-agent reactive synthesis problem with surveillance objectives specified as temporal logic formulas. In order to avoid the state space blow-up arising from a centralized strategy computation, we propose a method to decentralize the surveillance strategy synthesis by decomposing the multi-agent game into subgames that can be solved independently. We also decompose the global surveillance specification into local specifications for each sensor, and show that if the sensors satisfy their local surveillance specifications, then the sensor network as a whole will satisfy the global surveillance objective. Thus, our method is able to guarantee global surveillance properties in a mobile sensor network while synthesizing completely decentralized strategies with no need for coordination between the sensors. We also present a case study in which we demonstrate an application of decentralized surveillance strategy synthesis.

Tables

Table 1. TABLE I: Synthesis times for each surveillance subgame

	Subgame	Number of states	Synthesis time (s)
6 sensors	Subgame 1	69	101
	Subgame 2	74	206
	Subgame 3	62	111
	Subgame 4	52	88
	Subgame 5	77	285
	Subgame 6	66	64
	Total	400	855
3 sensors	Subgame 1	142	473
	Subgame 2	113	306
	Subgame 3	145	372
	Total	400	1151

Equations

$$((20,4),\{18\})\to \{\begin{array}{l}((15,3),\{19,23\})\\ ((21,9),\{19\})\\ ((21,9),\{17\})\\ ((15,9),\{19\})\end{array}$$

$$[[B_t]]=\{\begin{array}{ll}{B}_t& \text{if }{k}_i\notin B_t\\ B_t\cup (L\setminus {\tilde{L}}_i)& \text{if }{k}_i\in B_t.\end{array}$$

$$B_t\downarrow i=\{\begin{array}{ll}{B}_t& \text{if }{B}_t\subseteq {\tilde{L}}_i,\\ (B_t\cap {\tilde{L}}_i)\cup \{k_i\}& \text{otherwise}.\end{array}$$

$$f_s(s_0,\dots ,s_k,B_t,J)=(l_1,\dots ,l_n),$$

$$\begin{array}[]{lll}\mathit{local}_{i}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b})&\triangleq&\big{(}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\mathit{belief}\neq\{k_{i}\})\big{)}\rightarrow\\ &&\big{(}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(p_{b}\wedge(k_{i}\not\in\mathit{belief}))\big{)}.\end{array}$$

$${local}_i(\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}{p}_a\wedge \text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}\text{leavevmode}to8.7pt\text{vbox}to8.7pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.76527ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@lineto}4.09026pt6.67358pt\text{pgfsys@lineto}8.18053pt2.58333pt\text{pgfsys@lineto}4.09026pt-1.50694pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}{p}_b,n)\triangleq local(\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}{p}_a,n)\wedge {local}_i(\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}\text{leavevmode}to8.7pt\text{vbox}to8.7pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.76527ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@lineto}4.09026pt6.67358pt\text{pgfsys@lineto}8.18053pt2.58333pt\text{pgfsys@lineto}4.09026pt-1.50694pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}{p}_b).$$

Full text

I INTRODUCTION

The importance of surveillance in our daily life has been constantly growing in the past couple of decades, and with that, also the need for more efficient and sophisticated mechanisms for surveillance. One of the major challenges comes from the need to perform surveillance in large and complex environments, where it is not always feasible or cost effective to have complete surveillance coverage of the entire area at all times. Furthermore, sensors might not always be able to classify threats, and often require human intervention to assess the threat level. It can thus be necessary to deploy multiple mobile sensors, that work together with conventional static sensors to maintain a sufficient level of knowledge on the location of a potential threat. This is particularly crucial in applications where it is necessary to monitor a potential threat which can move over a large area until it can be accounted for.

In a formal setting, designing a surveillance strategy for a (mobile) sensor network dealing with a potentially adversarial target can be modelled as a two-player game in which one player represents the sensor network and the other player represents the adversary. There are several variants of such games, including pursuit-evasion games [1] and graph-searching games [2]. In such games, the problem is formulated as enforcing eventual detection, which is, in essence, a search problem – once the target is detected, the game ends. These types of games are too restrictive for applications where the goal is not to capture, but instead to maintain information about the location of the adversary for an unbounded time horizon.

Another class of games used in physical security are Stackelberg games, also known as leader-follower games. In such games the defender acts first, for example by placing their defence system, and the attacker follows with his action, possibly after obtaining information about the placed defence system. In recent years Stackelberg games have seen use in, among others, LAX airport, [3] and the US Coast Guard [4]. These games aim to compute randomized policies for the defender to protect target locations from an attacker. Extensions of this model [5] have been proposed to generate infinite-horizon patrolling strategies either for mobile resources alone or in concert with static alarm triggers [6, 7]. However, these models cannot be used to reason about the uncertain set of possible locations of dynamic threats.

Our objective in this work is not to just compute a patrolling strategy for the mobile sensors, but also to quantify the sensor network’s knowledge of the possible locations of active threats and use this information to synthesize strategies for the mobile sensors that provide knowledge guarantees on the threat location over an infinite-time horizon.

As a motivating case study we consider the use of autonomous drones working in cooperation with static sensors in wildlife conservation. UAVs are increasingly being adopted for monitoring of illegal hunting and poaching [8], though they are mostly remotely controlled [9]. In Kenya, for example, remotely controlled drones were deployed in 2014 in an attempt to reduce poaching by providing constant surveillance [10], allowing authorities to arrest rhino poachers when they are sensed by the drones. Autonomous UAVs have not been used in this setting yet, and proposed plans involve drones following pre-programmed paths [11]. In this paper, we propose a method for automatically constructing autonomous reactive surveillance strategies for multiple mobile sensors (like UAVs) working in concert with static sensors in the field.

We study the problem of synthesizing strategies for enforcing temporal surveillance objectives, such as the requirement to never let the sensor network’s uncertainty about the target’s location exceed a given threshold, or recapturing the target every time it escapes. To this end, we consider surveillance objectives specified in linear temporal logic (LTL), equipped with basic surveillance predicates. Our computational model is that of a two-player game played on a finite graph, whose nodes represent the joint possible locations of all the mobile sensors and the target, and whose edges model the possible (deterministic) moves between locations. The mobile sensors play the game with partial information, as they can only observe the target when it is in the area of sight of one of the sensors. The target, on the other hand, always has full information about the locations of all sensors in the network. In that way, we consider a model with one-sided partial information, making the computed strategy for the agent robust against a potentially more powerful adversary.

We formulate surveillance strategy synthesis as the problem of computing a joint winning strategy for the multiple mobile sensors in a partial-information game with a surveillance objective. Partial-information games with LTL objectives have been well studied [12, 13] and it is well known that the synthesis problem is EXPTIME-hard [14, 15]. In a companion publication at CDC 2018 we describe a framework for formalizing single-agent surveillance synthesis as a two-player game with partial information, and propose an abstraction-based method for solving such games. The interested reader is referred to the extended version [16] for details about the abstraction-based synthesis method. The price of resorting to abstraction is the potential overapproximation of the set of possible target locations (that is, loss of precision in the sensors’ knowledge) which may make satisfying the surveillance requirements more difficult. There is thus a trade-off between the strictness of the surveillance requirements, i.e, how closely a target needs to be tracked, and the size of the abstract game necessary for a surveillance strategy to exist.

Sensor networks consisting of a large number of dynamic sensors, as well as static sensors, can achieve better coverage, and thus, in general, can make do with much coarser abstractions to satisfy a given surveillance objective. However, even when using abstraction, the size of the game is exponential in the number of sensors. To address the blow-up of the state space incurred by a large number of sensors, we propose a decentralized synthesis method that aims to compute a surveillance strategy for each mobile sensor separately.

Contribution: Our contribution is as follows. We decompose the original surveillance game into a set of subgames, one for each sensor. Accordingly, the global surveillance objective is broken up into a local objective for each subgame. Our reduction guarantees that if the local strategy in each subgame satisfies the local surveillance objective, then the composition of the strategies fulfills the global surveillance objective. This allows us to solve each subgame under its local surveillance objective independently, using off-the-shelf reactive synthesis tools.

There has been work in decentralized synthesis for GR(1) specifications, however, the synthesis process often involves a centralized computation as in [17] or synchronization [18, 19]. Our approach, on the other hand is fully decentralized and the sensors require no coordination as simply satisfying their local properties guarantees the global objective.

II MOTIVATING CASE STUDY

We first describe the multi-agent surveillance synthesis problem informally, in the context of a motivating case study.

We consider wildlife conservation in Africa, in particular, at the Selous Game Reserve (SGR) located in Tanzania, where the African Black Rhinoceros population is under serious threat due to poaching. We are motivated by a recommended anti-poaching initiative in the SGR by the World Heritage Centre, to study the use of a sensor network for tracking the position of a potential poacher with user-specified precision. Since the SGR is a very large area, the network consists of both mobile and static sensors. We apply the distributed synthesis method proposed in this paper to synthesize surveillance strategies for the mobile sensors that satisfy the desired tracking requirement.

Figure 1 shows a section of the SGR that we represent as a gridworld which will form the state space of the game. Each static sensor monitors a given area of the grid (shown in yellow) and detects any presence of the target (i.e., threat) in these states, but cannot determine the target’s exact location. The requirement is to ensure that over and over again, the set of potential locations of the target is reduced to $5$ cells. In other words, every time the target escapes from the vision of all sensors, the network guarantees that eventually the uncertainty about its position will be reduced to $5$ grid cells.

III GAMES WITH SURVEILLANCE OBJECTIVES

We begin by providing a formal model for describing multi-agent surveillance strategy synthesis problems, in the form of a two-player game between the mobile sensors in a network and a target, in which the sensors have partial information about the target’s location.

III-A Multi-Agent Surveillance Game Structures

We define a multi-agent surveillance game structure to be a tuple $G=(S,s^{\mathsf{init}},T,\mathit{vis}_{1},\dots,\mathit{vis}_{n})$ where:

• •

$S=L_{s}\times L_{t}$ is the set of states, where $L_{s}=L_{1}\times L_{2}\times\dots\times L_{n}$ is the set of joint locations of the $n$ mobile sensors, $L_{i}$ is the set of possible locations of sensor $i$, and $L_{t}$ is the set of possible locations of the target;

• •

$s^{\mathsf{init}}=(l^{\mathsf{init}}_{1},\ldots,l^{\mathsf{init}}_{n},l_{t}^{\mathsf{init}})$ is the initial state;

• •

$T\subseteq S\times S$ is the transition relation describing the possible joint moves of the sensors and the target; and

• •

$\mathit{vis}_{1},\dots,\mathit{vis}_{n}$ are the visibility functions for the $n$ sensors, where $\mathit{vis}_{i}:L_{i}\times L_{t}\to\mathbb{B}$ maps a state $(l_{i},l_{t})$ to $\mathit{true}$ iff * position $l_{t}$ is in the area of sight of $l_{i}$*.

Additionally, we define the joint visibility function $\mathit{Vis}:S\to\mathbb{B}$ that maps a state $(l,l_{t})$ to $\mathit{true}$ iff the set $\mathcal{I}=\{i\mid\mathit{vis}_{i}(l_{i},l_{t})=\mathit{true}\}$ is non-empty. Informally, $\mathit{Vis}(l_{s},l_{t})$ is $\mathit{true}$ if the target is in view of at least one of the sensors.

The transition relation $T$ encodes the one-step move of the target and the $n$ sensors: First, the target makes a move, and then, the sensors move jointly in a synchronized manner.

We denote with $T{\downarrow}i$ the projection of the transition relation $T$ on the sets of locations of the target and the sensor with index $i$. Formally, we define $T{\downarrow}i=\{((l_{i},l_{t}),(l_{i}^{\prime},l_{t}^{\prime}))\in(L_{i}\times L_{t})^{2}\mid\exists l_{1},l_{1}^{\prime},\ldots,l_{i-1},l_{i-1}^{\prime},l_{i+1},l_{i+1}^{\prime},\ldots,l_{n},l_{n}^{\prime}:((l_{1},\ldots,l_{n},l_{t}),(l_{1}^{\prime},\ldots,l_{n}^{\prime},l_{t}^{\prime}))\in T\}.$

For a state $(l_{s},l_{t})\in S$ we define $\mathit{succ}_{t}(l_{s},l_{t})$ to be the set of possible successor locations of the target:

$\mathit{succ}_{t}(l_{s},l_{t})=\{l_{t}^{\prime}\in L_{t}\mid\exists l_{s}^{\prime}.\ ((l_{s},l_{t}),(l_{s}^{\prime},l_{t}^{\prime}))\in T\}$.

We extend $\mathit{succ}_{t}$ to sets of locations of the target by stipulating that for $L\subseteq L_{t}$, the set $\mathit{succ}_{t}(l_{s},L)$ consists of all possible successor locations of the target for states in $\{l_{s}\}\times L$. Formally, let $\mathit{succ}_{t}(l_{s},L)=\bigcup_{l_{t}\in L}\mathit{succ}_{t}(l_{s},l_{t})$.

For a state $(l_{s},l_{t})$ and a successor location of the target $l_{t}^{\prime}$, we denote with $\mathit{succ}(l_{s},l_{t},l_{t}^{\prime})$ the set of successor locations of the sensors, given that the target moves to $l_{t}^{\prime}$:

$\mathit{succ}(l_{s},l_{t},l_{t}^{\prime})=\{l_{s}^{\prime}\in L_{s}\mid((l_{s},l_{t}),(l_{s}^{\prime},l_{t}^{\prime}))\in T\}$.

We assume that, for every state $s\in S$, there exists a state $s^{\prime}\in S$ such that $(s,s^{\prime})\in T$, that is, from every state there is at least one move possible (including self transitions). We also assume, that when the target moves to an invisible location, its position does not influence the possible one-step moves of the sensors. Formally, we require that if $\mathit{Vis}(l_{s},l_{t}^{\prime})=\mathit{Vis}(l_{s},{\widehat{l}_{t}}^{\prime})=\mathit{false}$, then $\mathit{succ}(l_{s},l_{t},l_{t}^{\prime})=\mathit{succ}(l_{s},{\widehat{l}_{t}},\widehat{l_{t}}^{\prime})$ for all $l_{t},l_{t}^{\prime},\widehat{l}_{t},\widehat{l}_{t}^{\prime}\in L_{t}$. This assumption is natural in the setting where each of the sensors can move in one step only to locations that are in its sight.

Example 1

Figure 2 shows an example of a multi-agent surveillance game on a grid. The sets of possible locations $L_{i}$ and $L_{t}$ for the each of the sensors and for the target consist of the squares of the grid. The transition relation $T$ encodes the possible one-step moves of all the sensors and the target on the grid, and incorporates all desired constraints. For example, moving to a location occupied by another sensor or the target, or to an obstacle, is not allowed. In this example, the function $\mathit{vis}_{i}$ encodes straight-line visibility with a range of 2: a location $l_{t}$ is visible to sensor $i$ from location $l_{i}$ if there is no obstacle on the straight line between them and the distance between the target and sensor $i$ is not larger than 2. Initially the target is not in the area of sight of the sensors, but the initial position of the target is known. However, once the target moves to one of the locations reachable in one step, in this case, locations $17,19\text{ and }23$, this might no longer be the case. More precisely, if the target moves to location $17$, then the green sensor observes its location, but if it moves to one of the other locations, then neither sensor can observe it, and its exact location will not be known. ∎

III-B Static Sensors

We now describe a way to incorporate static sensors in the multi-agent surveillance game framework. Let $G$ be a multi-agent surveillance game structure as defined previously.

We identify a static sensor with a set of locations $\Lambda\subseteq L_{t}$ over which it operates. A surveillance game can have multiple static sensors (or none). Let $\mathcal{M}=\{\Lambda_{1},\dots,\Lambda_{m}\}$ be a given set of $m$ static sensors for $G$. For each location $l_{t}\in L_{t}$ we define $J(l_{t})$ to be the set of all indices of static sensors such that $l_{t}$ belongs to the corresponding set of locations, i.e, $J(l_{t})=\{j\in\{1,\ldots,m\}\mid l_{t}\in\Lambda_{j}\}$. We refer to $J(l_{t})$ as the set of triggered static sensors at location $l_{t}$. We also define $J(L)=\bigcup_{l_{t}\in L}J(l_{t})$ for a set of locations $L\subseteq L_{t}$.

We assume that sensors do not suffer from false positives or negatives (studying these is an avenue for future work).

III-C Belief-Set Game Structures

In surveillance strategy synthesis, we need to state properties of, and reason about, the information which the sensors have, i.e, the belief about the location of the target. To this end, we can employ a powerset construction which is commonly used to transform a partial-information game into a perfect-information one, by explicitly tracking the joint knowledge of the sensors as a set of possible locations of the target. In that way we define a two-player game in which one player represents the whole sensor network, and the other player represents the target.

Given a set $A$, we denote with $\mathcal{P}(A)=\{A^{\prime}\mid A^{\prime}\subseteq A\}$ the powerset (set of all subsets) of $A$.

Given a multi-agent surveillance game structure $G=(S,s^{\mathsf{init}},T,\mathit{vis}_{1},\ldots,\mathit{vis}_{n})$ with $m$ static sensors $\mathcal{M}=\{\Lambda_{1},\dots,\Lambda_{m}\}$, we define the corresponding belief-set game structure $G_{\mathsf{belief}}=(S_{\mathsf{belief}},s^{\mathsf{init}}_{\mathsf{belief}},T_{\mathsf{belief}})$ where:

• •

$S_{\mathsf{belief}}=L_{s}\times\mathcal{P}(L_{t})\times\mathcal{P}(\{1,\ldots,m\})$ is the set of states, where $L_{s}$ is the set of joint locations of the sensors, and $\mathcal{P}(L_{t})$ the set of belief sets describing information about the location of the target, and $\mathcal{P}(\{1,\ldots,m\})$ is the set of possible sets of triggered sensors;

• •

$s^{\mathsf{init}}_{\mathsf{belief}}=(l^{\mathsf{init}}_{1},\ldots,l^{\mathsf{init}}_{n},\{l_{t}^{\mathsf{init}}\},J(l_{t}^{\mathsf{init}}))$ is initial state;

• •

$T_{\mathsf{belief}}\subseteq S_{\mathsf{belief}}\times S_{\mathsf{belief}}$ is the transition relation where $((l_{s},B_{t},J),(l_{s}^{\prime},B_{t}^{\prime},J^{\prime}))\in T_{\mathsf{belief}}$ iff $l_{s}^{\prime}\in\mathit{succ}(l_{s},l_{t},l_{t}^{\prime})$ for some $l_{t}\in B_{t}$ and $l_{t}^{\prime}\in B_{t}^{\prime}$ , $J^{\prime}\subseteq J(B_{t}^{\prime})$, and one of the following three conditions is satisfied:

• (1)

$B_{t}^{\prime}=\{l_{t}^{\prime}\}$, $l_{t}^{\prime}\in\mathit{succ}_{t}(l_{s},B_{t})$, $\mathit{Vis}(l_{s},l_{t}^{\prime})=\mathit{true}$;

• (2)

$B_{t}^{\prime}=\{l_{t}^{\prime}\in\mathit{succ}_{t}(l_{s},B_{t})\mid\mathit{Vis}(l_{s},l_{t}^{\prime})=\mathit{false}\}\cap\\ \phantom{B_{t}^{\prime}=}\bigcap_{j\in J^{\prime}}\Lambda_{j},\text{ and }J^{\prime}\neq\emptyset$;

• (3)

$B_{t}^{\prime}=\{l_{t}^{\prime}\in\mathit{succ}_{t}(l_{s},B_{t})\mid\mathit{Vis}(l_{s},l_{t}^{\prime})=\mathit{false}\}\setminus\phantom{B_{t}^{\prime}=}\bigcup_{j=1}^{m}\Lambda_{j}$, and $J^{\prime}=\emptyset$.

Condition (1) captures the successor locations of the target that can be observed from one of the mobile sensors’ current locations. Condition (2) captures the cases when the target moves to a location that cannot be observed by the mobile sensors, but triggers a non-empty set $J^{\prime}$ of static sensors. Finally, condition (3) corresponds to the successor locations of the target not visible from the current location of any of the mobile sensors, and not triggering any static sensors.

Example 2

Consider the surveillance game structure from Example 1. The initial belief set is $\{18\}$, as the target’s initial position is known. Figure 2b shows some of the successor states of the state $((20,4),\{18\})$ in $G_{\mathsf{belief}}$.∎

Based on $T_{\mathsf{belief}}$, we can define the functions $\mathit{succ}_{t}:S_{\mathsf{belief}}\to\mathcal{P}(\mathcal{P}(L_{t})\times\mathcal{P}(\{1,\ldots,m\}))$ and $\mathit{succ}:S_{\mathsf{belief}}\times\mathcal{P}(L_{t})\times\mathcal{P}(\{1,\ldots,m\})\to\mathcal{P}(L_{s})$ similarly to the corresponding functions defined for $G$.

A run in $G_{\mathsf{belief}}$ is an infinite sequence $s_{0},s_{1},\ldots$ of states in $S_{\mathsf{belief}}$, where $s_{0}=s_{\mathsf{belief}}^{\mathsf{init}}$ and $(s_{i},s_{i+1})\in T_{\mathsf{belief}}$ for all $i$.

A strategy for the target in $G_{\mathsf{belief}}$ is a function $f_{t}:S_{\mathsf{belief}}^{+}\to\mathcal{P}(L_{t})\times\mathcal{P}(\{1,\ldots,m\})$ such that $f_{t}(\pi\cdot s)=(B_{t},J)$ implies $(B_{t},J)\in\mathit{succ}_{t}(s)$ for every $\pi\in S_{\mathsf{belief}}^{*}$ and $s\in S_{\mathsf{belief}}$. That is, a strategy for the target suggests a move resulting in some belief set reachable from a location in the current belief, and a set of triggered sensors.

A joint strategy for the sensors in $G_{\mathsf{belief}}$ is a function $f_{s}:S_{\mathsf{belief}}^{+}\times\mathcal{P}(L_{t})\to S_{\mathsf{belief}}$ such that, if, $f_{s}(\pi\cdot s,B_{t},J)=(l_{s}^{\prime},B_{t},J^{\prime})$ then, $B_{t}^{\prime}=B_{t}$, $J^{\prime}=J$, and $l_{s}^{\prime}\in\mathit{succ}(s,B_{t})$ for every $\pi\in S_{\mathsf{belief}}^{*}$, $s\in S_{\mathsf{belief}}$ and $B_{t}\in\mathcal{P}(L_{t})$. Intuitively, a strategy for the sensors suggests a joint move based on the observed history of the play, the current belief about the target’s position, and the set of currently triggered sensors.

The outcome of given strategies $f_{s}$ and $f_{t}$ for the sensors and the target in $G_{\mathsf{belief}}$, denoted $\mathit{outcome}(G_{\mathsf{belief}},f_{s},f_{t})$, is a run $s_{0},s_{1},\ldots$ of $G_{\mathsf{belief}}$ such that for every $i\geq 0$, we have $s_{i+1}=f_{s}(s_{0},\ldots,s_{i},B_{t}^{i})$, where $B_{t}^{i}=f_{t}(s_{0},\ldots,s_{i})$.

III-D Temporal Surveillance Objectives

We consider a set of surveillance predicates $\mathcal{SP}=\{p_{b}\mid b\in\mathbb{N}_{>0}\}$, where for $b\in\mathbb{N}_{>0}$ we say that a state $(l_{s},B_{t})$ in the belief game structure satisfies $p_{b}$ (denoted $(l_{s},B_{t})\models p_{b}$) iff $|\{l_{t}\in B_{t}\mid\mathit{Vis}(l_{s},l_{t})=\mathit{false}\}|\leq b$. Intuitively, $p_{b}$ is satisfied by the states in the belief game structure where the size of the belief set does not exceed the threshold $b\in\mathbb{N}_{>0}$.

We study surveillance objectives expressed in a fragment of linear temporal logic (LTL) over surveillance predicates. We consider safety surveillance objectives expressed using the temporal operator $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and liveness surveillance objectives expressed using the temporal operators $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and $\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$.

A safety surveillance objective $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$ requires that the size of the belief-set never exceeds the given threshold $b$. More formally, an infinite sequence of states $s_{0},s_{1},\ldots$ in $G_{\mathsf{belief}}$ satisfies the safety property $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$ if and only if for every $i\geq 0$ it holds that $s_{i}\models p_{b}$. A liveness surveillance objective $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, on the other hand, requires that the size of the belief is smaller or equal to the bound $b$ infinitely often. That is, $s_{0},s_{1},\ldots$ in $G_{\mathsf{belief}}$ satisfies $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$ if for every $i\geq 0$ there exists $j\geq i$ such that $s_{j}\models p_{b}$.

In this paper we consider safety and liveness surveillance objectives, as well as conjunctions of such objectives. We remark the following equivalences of surveillance objectives:

• •

$\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}\equiv\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{\min{(a,b)}}$;

• •

$\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}\equiv\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{\min{(a,b)}}$;

• •

if $a\leq b$, then $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}\equiv\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}$.

Using these equivalences, we can restrict our attention to surveillance objectives of one the following forms: $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$ or $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, where $a>b$.

III-E Multi-Agent Surveillance Synthesis Problem

A multi-agent surveillance game is a triple $(G,\mathcal{M},\varphi)$, where $G$ is a surveillance game structure, $\mathcal{M}$ is a set of static sensors, and $\varphi$ is a surveillance objective. A winning strategy for the sensors for $(G,\mathcal{M},\varphi)$ is a joint strategy $f_{s}$ for the sensors in the corresponding belief-set game structure $G_{\mathsf{belief}}$ such that for every strategy $f_{t}$ for the target in $G_{\mathsf{belief}}$ it holds that $\mathit{outcome}(G_{\mathsf{belief}},f_{s},f_{t})\models\varphi$. Analogously, a winning strategy for the target for $(G,\mathcal{M},\varphi)$ is a strategy $f_{t}$ such that, for every strategy $f_{s}$ for the mobile sensors in $G_{\mathsf{belief}}$, it holds that $\mathit{outcome}(G_{\mathsf{belief}},f_{s},f_{t})\not\models\varphi$.

**Problem statement: ** Given a multi-agent surveillance game $(G,\mathcal{M},\varphi)$, compute a joint strategy for the mobile sensors that is winning for the game $(G,\mathcal{M},\varphi)$.

In the remainder of the paper we show how to solve the multi-agent surveillance synthesis problem in a compositional manner. The key idea is to decompose the problem into a set of single-sensor surveillance games over smaller sets of locations, and solve each of these games separately.

IV DISTRIBUTED SURVEILLANCE GAMES

In the sequel we assume that $L_{1}=L_{2}=\dots=L_{t}\triangleq L$ in the surveillance game structure, i.e, all $n$ sensors and the target operate in the same state space. For the remainder of the paper, let $G=(S,s^{\mathsf{init}},T,\mathit{vis}_{1},\ldots,\mathit{vis}_{n})$ be a multi-agent surveillance game structure defined over $L$, and let $\mathcal{M}=\{\Lambda_{1},\dots,\Lambda_{m}\}$ be a set of static sensors. We define a state-space partition of size $n$ of the set $L$ of locations in a game structure $G$ to be a tuple $\widetilde{L}=(\widetilde{L}_{1},\ldots,\widetilde{L}_{n})$ of subsets of $L_{i}$ such that $\bigcup_{i=1}^{n}\widetilde{L}_{i}=L$, and $\widetilde{L}_{i}\cap\widetilde{L}_{j}=\emptyset$ for $i\neq j$.

IV-A Surveillance Subgames

We now describe how, given a state-space partition $\widetilde{L}=(\widetilde{L}_{1},\ldots,\widetilde{L}_{n})$, to construct a tuple of single-agent surveillance game structures $\widetilde{G}=(G^{1},\ldots,G^{n})$ that contains one surveillance subgame $G^{i}$ for each mobile sensor $i$. Each subgame, $G^{i}$ is defined over the subset of locations $\widetilde{L}_{i}$. Since the target and sensors operate on the same state space we will have $\widetilde{L}^{i}_{s}=\widetilde{L}^{i}_{t}=\widetilde{L}_{i}$. Additionally, to each $\widetilde{L}^{i}_{t}$ we add an auxiliary location $k_{i}$ that encapsulates all possible locations of the target that are outside of this subgame’s region, i.e., all locations in $L\setminus\widetilde{L}_{i}$. We then model transitions leaving or entering $\widetilde{L}^{i}_{t}$ as transitions to or from location $k_{i}$ respectively. We require that the initial location $l_{i}^{\mathsf{init}}$ of sensor $i$ is in $\widetilde{L}_{i}$.

Formally, given a subset $\widetilde{L}_{i}\subseteq L$ we define the subgame of $G$ corresponding to sensor $i$ as the tuple $G^{i}=(\widetilde{S}_{i},\widetilde{s}_{i}^{\mathsf{init}},\widetilde{T}_{i},\widetilde{\mathit{vis}}_{i})$ where:

• •

$\widetilde{S}_{i}=\widetilde{L}_{i}\times(\widetilde{L}^{i}_{t}\cup k_{i})$ is the set of states.

• •

$\widetilde{s}_{i}^{\mathsf{init}}=(l_{i}^{\mathsf{init}},\widetilde{l}_{t})$ is the initial state, where $\widetilde{l}_{t}=l_{t}^{\mathsf{init}}$, if $l_{t}^{\mathsf{init}}\in\widetilde{L}_{i}$, and $\widetilde{l}_{t}=k_{i}$ otherwise.

• •

The set $\widetilde{T}_{i}$ consists of two types of transitions: the transitions in $T{\downarrow}i$ that originate and end in the subgame’s region are preserved as they are. Transitions of the target exiting or entering $\widetilde{L}^{i}_{t}$ are replaced by transitions to and from location $k_{i}$ respectively, since $k_{i}$ represents all target locations outside of $\widetilde{L}^{i}_{t}$. Formally, for every pair of states $(\widetilde{l}_{i},\widetilde{l}_{t})\in\widetilde{S}_{i}$ and $(\widetilde{l}_{i}^{\prime},\widetilde{l}_{t}^{\prime})\in\widetilde{S}_{i}$ we have that $((\widetilde{l}_{i},\widetilde{l}_{t}),(\widetilde{l}_{i}^{\prime},\widetilde{l}_{t}^{\prime}))\in\widetilde{T}_{i}$ if and only if there exists a transition $((\widetilde{l}_{i},l_{t}),(\widetilde{l}_{i}^{\prime},l_{t}^{\prime}))\in T{\downarrow}i$ for which the following conditions are satisfied:

• –

if $\widetilde{l}_{t}\in\widetilde{L}_{t}^{i}$ and $\widetilde{l}_{t}^{\prime}\in\widetilde{L}_{t}^{i}$, then $\widetilde{l}_{t}=l_{t}$ and $\widetilde{l}_{t}^{\prime}=l_{t}^{\prime}$, that is, we have a transition internal for the region $\widetilde{L}_{t}^{i}$;

• –

if $\widetilde{l}_{t}\in\widetilde{L}_{t}^{i}$ and $\widetilde{l}_{t}^{\prime}=k_{i}$, then $l_{t}\in\widetilde{L}_{t}^{i}$ and $l_{t}^{\prime}\not\in\widetilde{L}_{t}^{i}$, that is, we have a transition exiting the region $\widetilde{L}_{t}^{i}$;

• –

if $\widetilde{l}_{t}=k_{i}$ and $\widetilde{l}_{t}^{\prime}\in\widetilde{L}_{t}^{i}$, then $l_{t}\not\in\widetilde{L}_{t}^{i}$ and $l_{t}^{\prime}\in\widetilde{L}_{t}^{i}$, that is, we have a transition entering the region $\widetilde{L}_{t}^{i}$;

• –

if $\widetilde{l}_{t}=k_{i}$ and $\widetilde{l}_{t}^{\prime}=k_{i}$, then $l_{t}\not\in\widetilde{L}_{t}^{i}$ and $l_{t}^{\prime}\not\in\widetilde{L}_{t}^{i}$, that is, we have a transition completely outside $\widetilde{L}_{t}^{i}$.

• •

The visibility function $\widetilde{\mathit{vis}}_{i}$ in the subgame $G^{i}$ agrees with the visibility function $\mathit{vis}_{i}$ of sensor $i$ in the original game when the target’s location is in the subgame’s region. Target locations outside of the region $\widetilde{L}_{t}^{i}$ (summarized by location $k_{i}$) are invisible to the sensor in the subgame. Formally, $\widetilde{\mathit{vis}}_{i}(\widetilde{l}_{i},l_{t})=\mathit{vis}_{i}(\widetilde{l}_{i},l_{t})$ when $l_{t}\in\widetilde{L}_{t}^{i}$, and $\widetilde{\mathit{vis}}_{i}(\widetilde{l}_{i},l_{t})=\mathit{false}$ if $l_{t}=k_{i}$.

Example 3

In Figure 3a, we have two subgames: $G^{1}$ for the green mobile sensor and $G^{2}$ for the blue one. The initial states in the subgames are $s_{1}=(20,14)$, and $s_{2}=(4,k_{2})$. Recall that $k_{i}$ is an indicator state to represent that the target is not subgame $i$. The transitions shown in Figure 3b show that the target has the ability to leave $G^{1}$ and enter $G^{2}$. ∎

Note that in this construction, sensor $i$ is not able to leave the region of locations $\widetilde{L}_{i}$. Furthermore, all the information about the target’s behaviour outside of the subgame’s region is completely hidden from the mobile sensor controller, since all locations outside of $\widetilde{L}_{t}^{i}$ are represented by the single location $k_{i}$. In section IV-C, we discuss the local knowledge (belief) of sensor $i$ in the game structure $G^{i}$.

IV-B Static Sensors in Subgames

We assumed that all information about the target’s behaviour outside of subgame $G^{i}$ is completely hidden from sensor $i$. Hence, sensor $i$ is only privy to static sensors that operate in the state space of the subgame $G^{i}$, i.e, static sensors $\Lambda_{m}$ where $\Lambda_{m}\cap\widetilde{L}_{i}\neq\emptyset$. For simplicity of the presentation we assume that each static static sensor operates in exactly one region $L_{i}$. Our results can easily be extended to the general case. We define $Q_{i}=\{i\mid\Lambda_{i}\cap\widetilde{L}_{i}\neq\emptyset\}$ to be the set of static sensors operating in the subgame $G^{i}$.

IV-C Local Beliefs in Surveillance Subgames

A surveillance subgame is a game structure with a single mobile sensor and some number of static sensors, and thus, is a special case of multi-agent surveillance game structure. With this, the definition of belief-set game structures from Section III-C directly applies to surveillance subgames.

In the belief-set game structure for a surveillance subgame $G^{i}=(\widetilde{S}_{i},\widetilde{s}_{i}^{init},\widetilde{T}_{i},\widetilde{\mathit{vis}}_{i})$ with static sensors $Q_{i}$, the belief sets represent the local belief of sensor $i$. More specifically, a belief set in $G^{i}_{\mathsf{belief}}$ is an element of $\mathcal{P}(\widetilde{L}^{i}_{t}\cup\{k_{i}\})$, and can thus contain the auxiliary location. Intuitively, if $k_{i}$ is present in the sensor’s current belief, then the target could possibly be outside of the local set of locations $\widetilde{L}_{i}$, or if the belief is the singleton $\{k_{i}\}$, then sensor $i$ knows for sure that the target is outside of its region. Additionally, if there is a triggered static sensor in the region, the sensor will know that the target must be in the state space of the static sensor and $k_{i}$ cannot be in the belief. Due to the definition of surveillance subgames in Section IV-A, the location $k_{i}$ must be in the belief of sensor $i$ whenever it is possible that the target is outside of its region. If $n\geq 2$, then at every given time $k_{i}$ must be in the belief set of at least one sensor (possibly several). We define the global interpretation $\llbracket B_{t}\rrbracket$ of a belief set $B_{t}$ in $G^{i}_{\mathsf{belief}}$, which is a set of locations in $G$, as

[TABLE]

Strategies of sensor $i$ in the belief-set game $G^{i}_{\mathsf{belief}}$ depend only on the sequence of states in this game, and thus, only on local information. Following the definitions in Section III-C, the outcome of a pair of given strategies $f_{i}$ and $f_{t_{i}}$ for the sensor and the target in $G^{i}_{\mathsf{belief}}$ is a sequence of states in $G^{i}_{\mathsf{belief}}$, each of which is a pair consisting of a location of sensor $i$ and a belief-set for sensor $i$ in $G^{i}_{\mathsf{belief}}$.

IV-D Distributed Surveillance Synthesis Problem

Given a state-space partitioning $\widetilde{L}$ and the corresponding tuple of subgames $\widetilde{G}=(G^{1},\ldots,G^{n})$ we will define a distributed surveillance strategy synthesis problem, which, intuitively, asks to synthesize strategies for the sensors in the individual belief subgames, such that together they guarantee the global surveillance objective. In this section we formalize this intuitive problem description. We first need to define what it means for the individual sensor strategies to jointly satisfy together a global requirement.

The surveillance requirements are defined in terms of the belief-states in $G_{\mathsf{belief}}$, but strategies in the belief subgames are defined in terms of sequences of local belief states. Hence, we need to define a mapping of states of the form $((l_{1},\ldots,l_{n}),B_{t},J)$ to elements of $\mathcal{P}(\widetilde{L}^{i}_{t}\cup\{k_{i}\})$ for each $i$. Since, by definition, a strategy for sensor $i$ in the corresponding belief subgame guarantees that it remains in $\widetilde{L}_{i}$, we only need to define the mapping for states $l_{i}\in\widetilde{L}_{i}$.

Formally, for a state $((l_{1},\ldots,l_{n}),B_{t},J)$ in $G_{\mathsf{belief}}$ we define its projection on belief subgame $i$ as $((l_{1},\ldots,l_{n}),B_{t},J){\downarrow}i=(l_{i},B_{t}{\downarrow}i,J\cap Q_{i})$, where

[TABLE]

The mapping extends to sequences of states in the usual way.

Intuitively, this mapping projects the joint knowledge of the sensors in $G_{\mathsf{belief}}$ onto the local belief of each sensor, where the sensors do not share their local beliefs with each other, that is, the sensors have no information about the target’s position outside of their own region. The global, shared belief of the sensors is formed by the combination of their local beliefs. More precisely, this is the intersection of the global interpretation of the local beliefs. Indeed, it is easy to see that the property $B_{t}=\bigcap_{i=1}^{n}\llbracket B_{t}{\downarrow}i\rrbracket$ holds.

Now we are ready to define the joint strategy of the sensors in $G_{\mathsf{belief}}$ obtained by executing together a given set of sensor strategies in the individual subgames. Let $f_{s_{1}},\ldots,f_{s_{n}}$ be strategies for the sensors in the belief subgames $(G^{1}_{\mathsf{belief}},\ldots,G^{n}_{\mathsf{belief}})$. We define the composition $f_{s_{1}}\otimes\ldots\otimes f_{s_{n}}$ of $f_{s_{1}},\ldots,f_{s_{n}}$, which is a joint strategy $f_{s}$ for the sensors in $G_{\mathsf{belief}}$, as follows: for every sequence $s_{0},\ldots,s_{k}$ of states in $G_{\mathsf{belief}}$, global belief $B_{t}\in\mathcal{P}(L_{t})$ and set of triggered sensors $J\subseteq\{1,\ldots,m\}$, we let

[TABLE]

where $l_{i}=f_{s_{i}}((s_{0},\ldots,s_{k}){\downarrow}i,B_{t}{\downarrow}i,J\cap Q_{i})$ for each $i$.

Remark. If, for some $i$, the projection $(s_{0},\ldots,s_{k}){\downarrow}i$ is undefined, then $f_{s}(s_{0},\ldots,s_{k},B_{t})$ is undefined. However, by the definition of each $f_{s_{i}}$ we are guaranteed that the projection is defined for every prefix consistent with $f_{s_{i}}$.

Intuitively, the joint strategy $f_{s_{1}}\otimes\ldots\otimes f_{s_{n}}$ makes decisions consistent with the choices of the individual strategies $f_{s_{1}},\ldots,f_{s_{n}}$ in the respective belief subgames.

Our goal is to synthesize a joint strategy $f_{s}$ that enforces a given surveillance property in the belief-set game $G_{\mathsf{belief}}$ by synthesizing individual strategies for all the sensors in the corresponding belief subgames. That is, we want to solve the following distributed surveillance synthesis problem.

**Problem statement: **Given a multi-agent surveillance game $(G,\mathcal{M},\varphi)$ with $n$ sensors, and a state-space partition $\widetilde{L}$, compute strategies $f_{s_{1}},\ldots,f_{s_{n}}$ for the sensors in the belief subgames $G^{1}_{\mathsf{belief}},\ldots,G^{n}_{\mathsf{belief}}$ respectively, such that the composed strategy $f_{s_{1}}\otimes\ldots\otimes f_{s_{n}}$ is a joint winning strategy for the sensors in the surveillance game $(G,\mathcal{M},\varphi)$.

Thus, in the distributed surveillance synthesis problem we have to compute strategies $f_{s_{1}},\ldots,f_{s_{n}}$ such that for every strategy $f_{t}$ for the target in $G_{\mathsf{belief}}$ it holds that $\mathit{outcome}(G_{\mathsf{belief}},f_{s_{1}}\otimes\ldots\otimes f_{s_{n}},f_{t})\models\varphi$. To this end, we have to provide local surveillance objectives for all the sensors, such that if all strategies are winning with respect to their local objectives, then their composition is winning with respect to the original surveillance objective. In this way we will reduce the multi-agent surveillance synthesis problem to $n$ single-agent surveillance problems over smaller sets of locations. This reduction is the subject of the next section.

V FROM GLOBAL TO LOCAL SPECIFICATIONS

In order to reduce the multi-agent surveillance synthesis problem for a given surveillance specification $\varphi$ to solving a number of single-sensor surveillance subgames, we need to provide local surveillance objectives for the individual subgames. The local objectives should be such that by composing the strategies that are winning with respect to the local objectives we should obtain a strategy that is winning for the global surveillance objective. More precisely, we have to provide local surveillance specifications $\varphi_{1},\ldots,\varphi_{n}$ such that if for each $i$ it holds that $f_{s_{i}}$ is a winning strategy for the sensor in $(G^{i},Q_{i},\varphi_{i})$, then the strategy $f_{s_{1}}\otimes\ldots\otimes f_{s_{n}}$ is a joint winning strategy for the sensors in $(G,\mathcal{M},\varphi)$.

Recall that the surveillance objective $\varphi$ is of the form $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, or $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, or $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, where $a>b$. We will provide translations for each of these types of specifications.

First, note that the belief sets in a belief subgame $G^{i}_{\mathsf{belief}}$ can contain the auxiliary location $k_{i}$, which represents all locations in $L\setminus\widetilde{L}_{i}$. Thus, when the local belief set contains $k_{i}$, the size of the global belief set depends on the local beliefs of the other agents as well. We have to account for this in the translation from global into local surveillance objectives.

Example 4

*Consider the global safety surveillance specification $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{5}$ in a network with two mobile sensors. In this case we can reduce the multi-agent surveillance problem to two single-agent surveillance games, each of which has $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{3}$ as the local specification.

To see why, consider the two possible cases of local belief set of sensor $1$ whose size is less than or equal to $3$. If $k_{1}$ is not part of the belief set of sensor $1$, then the target is definitely in the region of sensor $1$, meaning that the global belief is of size less than or equal to $3$, and hence smaller that $5$. If, on the other hand, $k_{1}$ is part of the local belief of sensor $1$, then the target can be in at most $2$ locations in $\widetilde{L}_{1}$. If at the same time we have that the local belief of sensor $2$ is of size at most $3$, this would guarantee that the size of the global belief does not exceed $5$.

Local specifications $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{4}$, on the other hand do not imply the global specification. Indeed, if at a given point in time both sensors have local beliefs of size $4$, each of which contains the corresponding location $k_{i}$, the resulting global belief will be of size $6$ and thus violate the global specification.∎*

Generalizing the observations made in this example, for any number of sensors $n\geq 2$ and global safety surveillance objective $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, we define the local safety surveillance objective for each of the sensors, denoted $\mathit{local}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b},n)$, as $\mathit{local}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b},n)\triangleq\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{c},$ where $c=\lfloor{\frac{b}{n}}\rfloor+1$. Since $n\geq 2$ and $b>0$, we have $c\leq b$.

Note that this translation is conservative, since if according to the belief of sensor $i$ the target could be outside its region, it should guarantee that the number of locations in its own region the target could be in is at most $\lfloor{\frac{b}{n}}\rfloor$, even if the target can possibly be in only one of the other regions. This conservativeness is necessary to guarantee soundness in the absence of coordination between the sensors.

We now turn to liveness surveillance objectives. It is easy to see that each sensor guaranteeing a small enough local belief infinitely often is not enough to satisfy the global surveillance objective, since the local guarantees can happen in time-steps different for the different sensors.

Example 5

Consider the global surveillance specification $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{5}$ for a network with two sensors. Suppose $f_{1}$ is a strategy for the sensor in $G^{1}_{\mathsf{belief}}$, which ensures that every even step the size of the local belief is $10$, and every odd step the local belief contains $k_{1}$ and its size is $3$. Strategy $f_{2}$ in $G^{2}_{\mathsf{belief}}$, is similar, but even and odd steps are interchanged: every even step the local belief contains $k_{2}$ and its size is $3$, and every odd step the size of the local belief is $10$. Thus, while $f_{1}$ and $f_{2}$ guarantee that their local belief is ”small enough” infinitely often, they do this at different steps.

We circumvent the problem illustrated in this example by requiring that each sensor satisfies the liveness guarantee on its own. For this, we have to consider two cases. First, if from some point on sensor $i$ always knows that the target is outside of its region, it has no obligation to satisfy the liveness surveillance guarantee. If, on the other hand, according to sensor $i$’s belief the target could be in $\widetilde{L}_{i}$ infinitely often (note that this is true for at least one sensor), then it has to satisfy the corresponding liveness guarantee.

In order to capture this intuition, we need two additional types of surveillance predicates. First, we need to be able to express the negation of the property that the local belief of sensor $i$ is the singleton $\{k_{i}\}$ (which means that sensor $i$ knows that the target is outside $\widetilde{L}_{i}$). For this, we introduce the predicate $\mathit{belief}\neq\{k_{i}\}$. Second, in order to express the local liveness guarantee, we need to be able to state that $k_{i}$ is not in $\widetilde{L}_{i}$ (which means that sensor $i$ knows that the target is in its region). The predicate we introduce for this property is $k_{i}\not\in\mathit{belief}$. Both predicates can be interpreted over belief sets similarly to $p_{b}$ and incorporated in LTL.

Formally, we define the local liveness specification for sensor $i$ denoted $\mathit{local}_{i}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b})$ as

[TABLE]

Note that the agent cannot trivially satisfy $\mathit{local}_{i}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b})$, since the belief set is defined precisely by it’s sequence of observations and is not under the agent’s direct control.

This translation is again conservative, since it would suffice that the liveness guarantee is satisfied by a single sensor. However, these can be different sensors for different behaviours of the target. Thus, we require that every sensor $i$ satisfies $\mathit{local}_{i}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b})$. This requires that if the target crosses from one region to another infinitely often, then both sensors have to satisfy the liveness surveillance objective.

Finally, for a global surveillance specification $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, the local surveillance specification for sensor $i$ is

[TABLE]

Slightly abusing the notation, we denote with $\mathit{local}_{i}(\varphi,n)$ the local surveillance specification for sensor $i$ for any of the three types of global surveillance specifications.

The next theorem, which follows from the definition of the local specifications, states the soundness of the reduction.

Theorem 1

Let $(G,\mathcal{M},\varphi)$ be a multi-agent surveillance game with $n$ sensors, where $\varphi$ is of the form $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, or $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, or $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{a}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{b}$, where $a>b$. Let $\widetilde{L}$ be a state-space partition. Suppose that $f_{1},\ldots,f_{n}$ are strategies for the sensors in the subgames $G^{1}_{\mathsf{belief}},\ldots,G^{n}_{\mathsf{belief}}$ respectively, such that for each sensor $i$ the strategy $f_{i}$ is winning in the surveillance game $(G^{i},Q_{i},\mathit{local}_{i}(\varphi,n))$. Then, it holds that the composed strategy $f_{s_{1}}\otimes\ldots\otimes f_{s_{n}}$ is a joint winning strategy for the sensors in the surveillance game $(G,\mathcal{M},\varphi)$.

VI EXPERIMENTAL EVALUATION

We now return to the case study outlined in Section II. We have implemented the proposed method in Python, using the slugs reactive synthesis tool [21], and evaluated it on the multi-agent surveillance game modelling the problem described in Section II. The experiments were performed on an Intel i5-5300U 2.30 GHz CPU with 8 GB of RAM.

We analyzed two scenarios. In Figure 4a, we have six mobile sensors. We compare the surveillance strategy with the situation in Figure 4b where we have three mobile sensors. In both cases there are four static sensors depicted in yellow in Figure 4. Our global surveillance task is $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{5}$, i.e, we need to infinitely often bring the belief of the target location to 5 cells or lower.

Solving either case centralized is not computationally feasible as the state space grows exponentially with the number of sensors - we will have in the order of $400^{6}$ and $400^{3}$ states respectively. Thus, we partition the multi-agent surveillance game into subgames as shown in Figures 4a and 4b. We then solve each game individually with local specifications $\mathit{local}_{i}(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{5})$. We solve these single-agent surveillance games using an abstraction-based method detailed in a companion publication at CDC 2018, detailed in [16]. We report the synthesis times in Table I.

The multi-agent surveillance game in Figure 4a results in more subgames compared to the game in 4b. However, each game is much smaller and strategies can be synthesized faster in each subgame. Figure 5 shows snapshots in time of the simulation of the 3 sensor surveillance game in Figure 4b. The target is being controlled by a human and the sensors are following their synthesized local surveillance strategies. The global belief is depicted in Figure 5 as grey cells, meaning that the combined knowledge of all the sensors has restricted the location of the target into one of the grey cells.

We see, in Figures 5a - 5c, that the target is in the subgame corresponding to sensor 2. Hence, only sensor 2 is moving and trying to lower its belief to below 5 cells (which it does in Figure 5d). In Figures 5b - 5d, the target starts moving towards subgame 3 at which point the target is detected by the static sensor in subgame 3 and sensor 3 takes over in figures 5e - 5f. There is no coordination between any of the agents, and each satisfy only their local surveillance specification. However, our construction guarantees that the global specification of $\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p_{5}$ will be satisfied.

VII CONCLUSIONS

We presented a method for decentralized synthesis of surveillance strategies for a mobile sensor network working together with static sensors. Problems that would otherwise be computationally intractable can be solved by decomposing the global game into local subgames for each sensor with individual surveillance specifications. We show that although each game is solved completely independently with no information sharing, we can still guarantee global surveillance properties. In future work we aim to incorporate false positives in static alarm triggers as well as noisy observations from the mobile sensors while still guaranteeing surveillance specifications.

Acknowledgement: This work was supported in part by grant Sandia National Lab 801KOB, grant ARO W911NF-15-1-0592, and grant DARPA W911NF-16-1-0001.