Links

Tools

Export citation

Search in Google Scholar

Monitoring hierarchical agent-based simulation traces

Journal article published in 2015 by Benjamin Herd, Simon Miles ORCID, Peter Mcburney, Michael Luck ORCID
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Question mark in circle
Preprint: policy unknown
Question mark in circle
Postprint: policy unknown
Question mark in circle
Published version: policy unknown

Abstract

Due to their internal complexity, agent-based simulations are rarely amenable to conventional formal verification. With its focus on individual traces, runtime verification represents an interesting alternative for correctness assessment. Here, execution traces produced by the running system are observed by a monitor and checked for correctness on-the-fly. If the truth or falsity of a given property cannot be determined at time t, then the monitor creates an obligation that the current trace needs to satisfy at time t + 1 in order for the whole property to become true. With different observational levels, traces produced by agent-based simulations have an inherently hierarchical nature which complicates the structure and manipulation of obligations significantly. However, it turns out that this problem is general enough to be dealt with in an abstract, language-independent way. In this paper, we provide a general framework for the monitoring of hierarchical traces. It introduces different types of obligations and appropriate manipulation procedures along with minimal requirements that a property specification language needs to satisfy in order to be monitorable. We provide a full formalisation of the framework and an example implementation of a subset in Haskell.