Safety Verification and Universal Invariants for Relational Action Bases
Authors: Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
IJCAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We then demonstrate feasibility through an extensive experimental evaluation conducted on a suitably extended version of the only existing formal modeling and verification benchmark for data-aware processes [Gianola, 2022]. As a second technical contribution, we put MCMT at work: we show that it terminates producing a correct answer with very good performance, on a set of 34 RABs that we derive from a benchmark of data-aware processes [Li et al., 2017]. We now put our verification machinery in practice, exploiting that, as shown in our technical development, we can employ the different modules of MCMT to handle parameterized safety checking of RABs. We test the novel features of RABs, namely universal quantification and arithmetics on relational dynamic systems, for which no other existing tool can be employed. Specifically, we conduct an extensive experimental evaluation on RABs representing 33 (32 plus one variant) concrete data-aware processes derived from the existing benchmark in [Li et al., 2017]. Results are shown in Table 1 (more detailed information is in [Ghilardi et al., 2022b]), which reports, for each example: (i) if it contains arithmetics (Ar) and universal guards (UG); (ii) the number of transitions (#T), also counting those that contain quantified data variables (#Q). The table also includes several measures: (i) number of UNSAFE (#U) and SAFE (#S) outcomes; (ii) seconds for the average (µT) and maximum (Max T) MCMT execution time; (iii) indications of number of calls to the external SMT solver (#(calls)). |
| Researcher Affiliation | Academia | 1Dipartimento di Matematica, Universit a degli Studi di Milano, Milan, Italy 2Faculty of Engineering, Free University of Bozen-Bolzano, Bolzano, Italy 3DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark |
| Pseudocode | Yes | Algorithm 1: BReach RAB |
| Open Source Code | Yes | The benchmark is on https://github.com/AlessandroGianola/RAB-verification. |
| Open Datasets | Yes | We conduct an extensive experimental evaluation on RABs representing 33 (32 plus one variant) concrete data-aware processes derived from the existing benchmark in [Li et al., 2017]. |
| Dataset Splits | No | The paper conducts experiments on models derived from a benchmark but does not specify training/validation/test dataset splits, which is common in machine learning but not typically applicable to formal verification benchmarks of this nature. |
| Hardware Specification | Yes | Experiments were performed on a 2.3 GHz Intel Core i5 machine with mac OS High Sierra and 8 GB RAM. |
| Software Dependencies | No | The paper mentions using the MCMT model checker and Z3 solver but does not provide specific version numbers for these or other software components used in the experiments. |
| Experiment Setup | No | The paper describes the encoding of models into RABs and the use of MCMT for verification, but it does not provide specific hyperparameters, training configurations, or detailed system-level settings typically found in an "experimental setup" section for machine learning or simulation studies. |