Page 33 - Read Online

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

Figure 10. RL performance comparison of the variant with a single FIS for siege tank control, the variant with a single FIS providing all control
actions, and the original system that is utilized within this study.

Table 2. Counterexample for Spec 1 failure prior to modification
Variable Value
MarineHealth 1.0
MarineDamageRate 0.0
HealBid 0.3

respectively. A singular rule in our RB will correspond to exactly when the inputs are at those values, and
those values are the extremes of the normalized space for both inputs. Hence, upon investigation of our RB
we would see that we have a rule in our chromosome of ”If Marine Health is Very High and Marine Damage
Rate is None, then Healing Bid is Low”. By changing the output MF to ”Very Low” for this rule, we can easily
solve this specification failure.

Though not a requirement, it is also often very beneficial to develop a scenario within the simulation environ-
ment that can help represent a potential case of a found counterexample. Observing the agent’s performance
through these specifically designed scenarios can both provide insight to the control issue, as well as provide
feedback to the solution of the problem once found. Note that removing the failure case from a specific sce-
nario does not guarantee that the specification will always hold, but measures can be taken to ensure this
within regions of interest and verified again using Formal Methods. In this case, it is not necessary due to the
simplicity of the counterexample found, but was completed and is seen below in Figures 11 and 12.

A scenario was developed in which there are two marines, a medivac, and two zerglings. The zerglings are at
full health, but the marines are wounded. In particular, the marine at the top of the formation is moderately