King's College London

Research portal

Monitoring hierarchical agent-based simulation traces

Research output: Chapter in Book/Report/Conference proceedingConference paper

Original languageEnglish
Title of host publicationProceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
PublisherInternational Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)
Pages463-471
Number of pages9
Volume1
ISBN (Print)9781450337694
Publication statusPublished - 2015
Event14th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015 - Istanbul, Turkey
Duration: 4 May 20158 May 2015

Conference

Conference14th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015
CountryTurkey
CityIstanbul
Period4/05/20158/05/2015

Links

King's Authors

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.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454