environment ID: E- Snow: StringLoc x StringLoc
- pulseloc : StringLoc
- pulseA:
pre: TRUE
post: E.pulseloc(e)=A - pulseB:
pre: TRUE
post: E.pulseloc(e)=B
- blastA:
pre: Att.loc(p)=A & Att.destroyed(p)=FALSE
post: TRUE - blastB:
pre: Att.loc(p)=B & Att.destroyed(p)=FALSE
post: TRUE
- pulseloc: NULL_StringLoc
agent ID: Att- loc : StringLoc
- destroyed : BOOLE
- gotoA:
pre: Att.loc(self)=init & E.pulseloc(e)!=A & !Snow(init,A) & Att.destroyed(self)=FALSE
post: Att.loc(self)=A - gotoB:
pre: Att.loc(self)=init & E.pulseloc(e)!=B & !Snow(init,B) & Att.destroyed(self)=FALSE
post: Att.loc(self)=B - goTargetA:
pre: Att.loc(self)=A & !Snow(A,target) & Att.destroyed(self)=FALSE
post: Att.loc(self)=target - goTargetB:
pre: Att.loc(self)=B & !Snow(B,target) & Att.destroyed(self)=FALSE
post: Att.loc(self)=target
- blastA: E
pre: Att.loc(self)=A
post: Att.destroyed(self)=TRUE - blastB: E
pre: Att.loc(self)=B
post: Att.destroyed(self)=TRUE
- loc: init
destroyed: FALSE
main controls
more options
witness of unsafety
Imagine a robotic swarm attacking a defense position, protected by a robot cannon. There are only two possible paths to reach the position: an attacker must first move to waypoint A or B, then move again to reach the target. Attackers can only move to either waypoint if the paths to A or B are not covered in snow, and similarly for reaching the target. The snow condition is not known in advance. The defensive cannon can target either waypoint with a blast or with an EMP pulse. The cannon program is so that a blast can only be fired if there are robots in that waypoint, and at least one robot under fire is hit. If instead the EMP pulse is directed towards A or B, no robot can move there. The cannon can use either the blast or activate the pulse at the same time but, while the EMP is active, the cannon can continue firing blasts. The EMP can cover either A or B, not both. The number of attackers is not known.
It appears that, even if all paths are free of snow, an effective defensive plan exists: at the beginning, use the pulse (say against A); let the enemy robots make their moves to B (the pulse remains active on A), then use the blast against B to destroy robots there. Whenever further attackers move to B, use again the blast, otherwise wait.
If one path is not viable the plan is even simpler: use the EMP to block the only waypoint or use the blast whenever attackers show up.
Question: does this strategy work? Answer: only if the blast destroys all robots in the waypoint against which it is fired. Q: if blasts do not hit all robots under fire, how many attackers may have a chance of reaching the target? A: at least two, if they move to the waypoint B together, since blasts always hit at least one robot. Q: is any attack plan for at least two robots guaranteed to work? A: no.
This scenario is trivial, however a complex network of waypoints or cannons capable of targeting multiple waypoints can make this arbitrarily complex, also given that the snow conditions cannot be foreseen, requiring to reason by cases. If ``playing'' as attackers, computing an attack plan (and for how many robots) that has chances against any number of cannons is even more complex.
The figure below represents the two templates as labelled finite-state transition systems (the environment is on the right).
Experiments
The textual encoding of the ABS corresponding to the PMAS in the running example is solved by MCMT v.3.0, on a machine with Ubuntu 18.04, 3.60 GHz Intel Core i7-7700 CPU, in 1.67 seconds using Z3 (version 4.8.9.0) as background SMT solver.
As expected, if we duplicate the robot templates, hence artificially increasing the number of transitions in the ABS, the performances decrease. Eliminating the alternation between the environment and the robots, greatly improves the performances even with several copies of the attacker template.
Conclusions
Assuming the asynchronous semantics adopted by SAFE Base, the PMAS is clearly unsafe if the protocol of the cannon is arbitrary, since it may adopt a naive behavior. In fact, MCMT returns a run template in which the cannon only uses the EMP pulse, without even attempting to fire blasts. However, even if the cannon is modeled according to the plan described above the PMAS is still unsafe: when the paths are clear of snow, it is sufficient that at least two attacking robots move at some step on the waypoint not protected by the pulse, so that one of them may not be killed by the cannon and will thus reach the target.
Observe that we can also model the case in which the cannon kills all robots in the location at which it is fired, but this requires the synchronous execution semantics assumed by SAFE For All.
Safe Swarms Club
better be safe than sorry