Abstract
We explore the capabilities of GROOVE, a state-of-the-art toolset based on graph transformation systems, to perform different kinds of analyses of Reaction Systems, ranging from reachability and causal analysis to model checking. Our results are encouraging, as in the presence of large state spaces GROOVE improves the time required for both reachability and causal analyses by an order of magnitude, compared to other available tools. From the point of view of GROOVE, the implementation of Reaction Systems provided some interesting insights on the most convenient way to model certain computational requirements through negative and nested application conditions
| Original language | English |
|---|---|
| Pages (from-to) | 1075-1099 |
| Number of pages | 25 |
| Journal | Natural Computing |
| Volume | 24 |
| Issue number | 4 |
| Early online date | 24 Nov 2025 |
| DOIs | |
| Publication status | Published - Dec 2025 |
Keywords
- UT-Hybrid-D
- Reaction Systems
- Graph transformation
- GROOVE
- Causal analysis
- Formal methods