<p>The research as a whole focuses on developing a parameterised way to establish whether or not a swarm displays a certain global emergent behaviour as a result of the sophisticated patterns of interactions among the agents to drone swarm algorithms, the novel challenge being that the number of drones to consider is unbounded and can change at runtime. To be able to tackle this problem, the logic framework of choice needed had to be highly parameterized and temporal in order to account for the changing behaviour of drone swarms over time and the fact that the number of drones is unbounded and a changing number of drones are involved. Probabilistic Computational Tree Logic (PCTL) satisfies these demands and facilitates the identification of emergent behaviour in a large swarm.</p>

<p>The research as a whole focuses on developing a parameterised way to establish whether or not a swarm displays a certain global emergent behaviour as a result of the sophisticated patterns of interactions among the agents to drone swarm algorithms, the novel challenge being that the number of drones to consider is unbounded and can change at runtime. Emergent behaviours in this context are those that exhibit global properties that come about as the result of interactions between individual drones in the system, but cannot be predicted by studying them individually. To be able to tackle this problem, the logic framework of choice needed had to be highly parameterized and temporal in order to account for the changing behaviour of drone swarms over time and the fact that the number of drones is unbounded and a changing number of drones are involved. Probabilistic Computational Tree Logic (PCTL) satisfies these demands and facilitates the identification of this emergent behaviour in a large swarm.</p>

<p>Computational Tree Logic (CTL) is a branching-time logic, meaning its model of time is a tree-like structure where the future is not determined (many paths in the future). Often used for model checkers in deterministic software verification applications. The researcher opted for the adapted Probabilistic Computational Tree Logic (PCTL) due to the probabilistic, non-deterministic nature of drone swarm evolution.</p>

<h1id="grammar">Grammar</h1>

<p>One possible well-defined grammar for PCTL is as follows:</p>

...

...

@@ -55,7 +55,7 @@

<p><strong>The formula <spanclass="math inline">\(P_{\geqslant{0.5}}\left[X^6\left(\text{connected}, 1\right)\right]\)</span> says “with probabilitiy at least <spanclass="math inline">\(0.5\)</span> agent <spanclass="math inline">\(1\)</span> will be connected after <spanclass="math inline">\(6\)</span> time steps.”</strong></p>

<p>In the work carried out by the researcher, path formulas and state formulas are represented by a slightly more domain specific adaptation of PCTL whose details will be omitted in this introduction, but as an overview, the definition also allows the researcher to:</p>

<ul>

<li>say whether an agent is connected to the swarm with at least a certain probability and a number of time steps, critical for checking some emergent behaviour.</li>

<li>say whether an agent satisfies a certain property (e.g. connectedness) with a specific probability after a number of time steps.</li>

<li>define time bounds for emergent behaviour.</li>

<p>As part of the preliminary paper <em>“Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems”</em>, new semantics for probabilistic swarms has been explored and brought to light.</p>

<p>The parameterised semantics, in general, deals with the environment of the swarm as well as the individual agents. The environment’s state is changing depending on the actions performed by all the agents while each agent chooses their next actions based upon a probability distribution which is calculated based on the agent’s own current state.</p>

<p>A more restricted version, in terms of the bounding of the number of time steps, of PCTL or Probabilistic Computation Tree Logic, is presented. This version, which is expressed as a fragment of PCTL, aims to be a form of formal identification of emergent properties.</p>

<p>It is to be determined whether a <em>global emergent behavior</em>, a certain characteristic exhibited swarm-wide or “globaly”, is always displayed in each swarm. As this behaviour acts as an indication for each member’s characteristics and its contribution, it is possible for a swarm to be validated before deployment for an arbitrary number of agents – given that a global emergent behavior is common amongst the agents. This will be achieved by the parameterised semantics described above.</p>

<p>It is to be determined whether a <em>global emergent behaviour</em>, a certain characteristic exhibited swarm-wide or “globally”, is always displayed in each swarm. Further, it is to be established whether the emergent property is above a certain <em>emergent threshold</em>. This is where swarms of a certain size equal and higher, compared to the threshold, exhibit this common behaviour. As this behaviour acts as an indication for each member’s characteristics and its contribution, it is possible for a swarm to be validated before deployment for an arbitrary number of agents – given that a global emergent behaviour is common amongst the agents for swarms at and above the threshold. This will be achieved by the parameterised semantics described above.</p>

<p>The restricted PCTL is utilized to create an algorithm to <em>solve the emergent property identification problem</em> (which determines whether the specification is an emergent property of the system or not) and the emergence <em>threshold identification problem</em> (which computes an emergence threshold for a given property of the system).</p>

<p>By the semantics introduced and the restricted algorithm utilising PCTL, reasoning about an unbounded swarm (in terms of size) is possible - a step towards the verification of unbounded drone swarms altogether.</p>

<h1id="synthesis-of-fault-tolerance-ratio">Synthesis of Fault Tolerance Ratio</h1>