Page 32 - Read Online

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

39,062,500 rules. During the RL comparison process, the compute system utilized however had 32 GB of
RAM, an insufficient amount to perform with a chromosome defining a rule-base of this magnitude. How-
ever, if this was reduced to 4 MFs per input, making the rule-base contain 4∗4 , or 4,194,304 total rules, then
10
32 GB of RAM was sufficient.

The RL process for these two variants was exactly the same as before, with a total of 60 chromosomes trained
over 50 generations. The maximum fitness found by generation for each of the systems is displayed in Figure
10. As anticipated, the 10-input 4-output variant had significantly worse performance than the original system,
though improvements were able tobe made throughout the RL process. Though the performance ceiling of the
original system is again bounded above by this variant’s, the amount of RL that would be necessary to surpass
the original’s performance is likely prohibitive.

Alternatively, the performance of the variant that solely combined the siege tank’s control into a single FIS
performed favorably compared to the study’s original system. As the genetic process is non-deterministic, and
the total number of fuzzy rules is still relatively small, the fact that the initial generation’s performance was
superior than the original study’s is well within expected range. While additional runs of the RL process would
create different results, the increased granularity of this variant as compared to the study’s original system
can be explained through the increase in the search space size. For the majority of this small, 50-generation
process, the original system has a higher maximum fitness, though the variant does ultimately end with a
higher performing fitness by the end of the run.

WhilethisisaverysmallGFTsystem, thiscomparisondemonstratestrade-offcomparisonsbetweenincreased
number of FISs (and thus, less overall rules) and the potential effect on RL performance. Though the single-
FIS for siege tank control variant performed slightly better, it would be more difficult to formally verify, and
overall has a more complex challenge for explainability as compared to the original system. For the remainder
of the study, the original GFT architecture will be utilized.

3.2. Formal verification
3.2.1 Safety specification 1
Again, our first specification, the Medivac Healing Spec, states ”If a marine’s health is very high and the marine
is not under attack, its corresponding healing bid must be very low”. Although simple, adherence to this
specification is desired in all cases. We can represent this in a numerical form by utilizing the points of our
MFs with maximum value for each linguistic term, as shown in Equation 2. This is then translated to Linear
Temporal Logic (LTL) as shown in Equation 3.

1 =If ( ℎ > 0.75) and ( = 0.0)
(2)
then ( < 0.25)

1 =□(( ℎ > 0.75) ∧ ( = 0.0)
(3)
→ ( < 0.25))

Utilizing Psion and JKIND, we can evaluate our singular FIS node over this specification and either receive
a mathematical guarantee that our system will adhere to this system in all cases, or receive a counterexample
trace which proves that our system does not. Table 2 shows that a counterexample was found. Note that
interestingly the presented counterexample corresponds to exactly the values 1.0 and 0.0 for our two inputs