Name
Abstract | ||
|---|---|---|
Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs ( as well as the verification problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.3233/FI-2018-1707 | FUNDAMENTA INFORMATICAE |
Field | DocType | Volume |
Graph,Discrete mathematics,Petri net,Model checking,Negation,Fixed point algorithm,Equivalence (measure theory),Fixed point,State space,Mathematics | Journal | 161 |
Issue | ISSN | Citations |
4 | 0169-2968 | 0 |
PageRank | References | Authors |
0.34 | 0 | 12 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Engelbredt Dalsgaard | 1 | 71 | 4.25 |
| Søren Enevoldsen | 2 | 3 | 2.76 |
| Peter Fogh Odgaard | 3 | 43 | 11.58 |
| Lasse S. Jensen | 4 | 3 | 0.74 |
| Peter Gjøl Jensen | 5 | 32 | 9.38 |
| Tobias S. Jepsen | 6 | 3 | 0.74 |
| Isabella Kaufmann | 7 | 3 | 0.74 |
| Kim G. Larsen | 8 | 3922 | 254.03 |
| Søren M. Nielsen | 9 | 3 | 0.74 |
| Mads Chr. Olesen | 10 | 120 | 8.43 |
| Samuel Pastva | 11 | 6 | 3.85 |
| Jirí Srba | 12 | 252 | 28.68 |