Name
Abstract | ||
|---|---|---|
We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and PRISM model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1093/logcom/exv002 | JOURNAL OF LOGIC AND COMPUTATION |
Keywords | DocType | Volume |
Model checking,BDI agent programming,AJPF,SPIN,PRISM | Journal | 28 |
Issue | ISSN | Citations |
3 | 0955-792X | 2 |
PageRank | References | Authors |
0.39 | 19 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Louise A. Dennis | 1 | 360 | 37.62 |
| Michael Fisher | 2 | 96 | 7.91 |
| Matt Webster | 3 | 88 | 8.30 |