Two-stage agent program verification

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.