Two-stage agent program verification

Dennis, Louise A ORCID: 0000-0003-1426-1896, Fisher, Michael and Webster, Matt ORCID: 0000-0002-8817-6881 (2018) Two-stage agent program verification. JOURNAL OF LOGIC AND COMPUTATION, 28 (3). pp. 499-523.

Text
jlc_final.pdf - Unspecified
Download (624kB)

Official URL: http://dx.doi.org/10.1093/logcom/exv002

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.

Item Type:	Article
Uncontrolled Keywords:	Model checking, BDI agent programming, AJPF, SPIN, PRISM
Depositing User:	Symplectic Admin
Date Deposited:	20 Apr 2016 13:45
Last Modified:	16 Dec 2022 06:45
DOI:	10.1093/logcom/exv002
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3000122