Page 24 - Read Online

Ernest et al. Complex Eng Syst 2023;3:4 I http://dx.doi.org/10.20517/ces.2022.54 Page 5 of 22

to evolve the population of candidate GFT solutions until termination criteria are met.

After some amount of training, a fixed configuration for the GFT architecture is evaluated, tested, and verified.
Additional numerical testing is often performed along with unit tests, formal verification, and human inspec-
tion and correction. If counterexamples to formal specifications are found, they are often mitigated through
direct designer input, or added to the RL process in such a way to penalize GFT configurations in the GA
population that have such violations. This iterative process continues until adherence to all specifications and
requirements is achieved and performance metrics are met.

2.1.3. Formal verification
As mentioned in Section 2.1.2, the process for verifying a GFT involves taking a GFT with a particular con-
figuration (fixed structure, parameters, etc.) and evaluating it against formal specifications about its behavior.
These specifications are often derived from system requirements, but can also be created from sources such as
numeral/simulation-based test results, rules of engagement or other high level behavioral constraints, certifi-
cation standard criteria, etc. The specifications are then translated from natural language to a formal language
using mathematical logic in order to be encoded for formal methods analysis. The formal languages used
depend on the necessary expressiveness of the language based on the specification itself. Some of these lan-
guages include Propositional Logic, First Order Logic (FOL), and temporal logics such as Linear Temporal
Logic, Computational Tree Logic, etc. Many others could be used depending on the use case and formulation
of the specifications and models, and Thales GFTs have been implemented with a number of these methods,
most commonly FOL and LTL.

ModelsoftheGFTarethentranslatedtoformalverificationtoolssuchasSMTsolversandmodelcheckers, and
then checked against the specifications. If counterexamples are found, modification of the GFT is performed
by the designer and/or the ML process. The tools used in this work are the state-of-the-art SMT solver Z3 [19]
along with the infinite state model checker jKIND [20] .

2.2. Starcraft 2 GFT development
The development process for the SC2 use case is largely the same as the general process described in Section
2.1. An initial GFT is constructed for parts of agent control based on expert knowledge, it is trained using
gradient-free RL in the SC2 environment, formal verification is performed and modifications are made based
on counterexamples generated, and then iterated until a performant, specification compliant GFT is found.

2.2.1. StarCraft 2 information
As this study is focusing on specific scenarios for demonstrating the explainability and formal verifiability of
this capability, we only consider four different unit types within this context:

• Marine: Abasichumaninfantryunitwhichcanfirea ranged volley ata certainfrequency. Hasanadvanced
technique Starcraft 2 players can utilize in which if they perform rapid movement commands between
volleys, they can both re-position slightly as well as fire faster, outputting more damage per second.
• Medivac: A human air vehicle which can utilize a limited resource pool to support ground biological units,
such as marines, by healing their durability at a set amount per second. Can also be utilized to transport
units, though this capability will not be utilized within the context of this study.
• Siege Tank: A human ground vehicle, which can move and attack ground units normally. In ”siege mode”
the tank becomes stationary, but can attack further and do increased damage per shot, but cannot attack
units within a short range of it. Most interestingly for this study, this unit is one of the few that does ”splash
damage” that includes friendly units. That is, friendly units near the target will take damage within a certain
range. As such, the siege tanks within this study will always be in ”siege mode”.
• Zergling: An alien (Zerg) insect unit that is a fast melee attacker. Can not attack air units but can quickly
overwhelm ground units. Will serve as the hostile unit type for this study.