RQ1:Hyper-parameter analysis

In this RQ, we would like to assess the impact of the hyper-parameters. Table 2 presents the detailed results for different abstract models. We observe that larger values of c and k result in an increase in the number of abstract states and abstract transitions. For example, in ACC-SAC, when c = 10 and k = 4 change to c = 20 and k = 4, the number of abstract states increases from 3441 to 17834, and abstract transitions increase from 49965 to 211643. Intuitively, the preciseness of the abstract model also improves with a larger model size. For ACC-DDPG, the most precise model achieves a preciseness of 96.06%, while the case with the minimum number of states and transitions obtains a preciseness of 84.44%. However, it is worth noting that larger abstract models also require more verification time, as indicated by the “PMC time” column. With the increase in abstract state size, the PMC time could increase in order of magnitude, which is expected of the current model checking tools (the search space for them becomes quickly intractable with the increase in the number of states). For example, in CSTR-DDPG, the PMC time varies from 0.54 to 1608.56 seconds. An abstract model on a large scale might make the deployment of online safety monitoring impractical. Thus, in practice, users should find a balance between preciseness and PMC time when selecting hyper-parameters.