Using Agent JPF to build models for other model checkers

Research output: Contribution to conferencePaperpeer-review

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 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 Spin and Prism. In the case of Spin we also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.
Original languageUndefined
Pages273-289
Number of pages17
DOIs
Publication statusPublished - Sept 2013
EventCLIMA :14th International Workshop on Computational Logic in Multi-Agent Systems: Computational Logic in Multi-Agent Systems - Corunna, Spain
Duration: 16 Sept 201318 Sept 2013

Conference

ConferenceCLIMA :14th International Workshop on Computational Logic in Multi-Agent Systems
Country/TerritorySpain
CityCorunna
Period16/09/1318/09/13

Keywords

  • Model checker
  • multiagent system
  • linear temporal logic
  • Symbolic execution
  • Kripke Structure

Cite this