Abstract
This paper focusses on the usefulness of approximate probabilistic model checking for the internal and external validation of large-scale agent-based simulations. We describe the translation of typical validation criteria into a variant of linear time logic. We further present a prototypical version of a highly customisable approximate model checker which we used in a range of experiments to verify properties of large scale models whose complexity prevents them from being amenable to conventional explicit or symbolic model checking.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In Hérault’s paper, this parameter is referred to as \(diagram\) [11].
- 2.
Note that, in the presence of finite traces, the duality between invariants and negated reachability properties does not hold.
- 3.
We assume the following mapping: \(0 \rightarrow Susceptible, 1 \rightarrow Infected, 2 \rightarrow Recovered\).
- 4.
Alternatively, the property can also be expressed as follows: \(\mathbb {P}_{=0}(\mathbf {F}(health(x)=0 \wedge \mathbf {X}(health(x)=2) ))\)
- 5.
- 6.
At the time of writing, each computing unit is equivalent to a 1.0–1.2 GHz 2007 Opteron or 2007 Xeon processor.
- 7.
By ‘recovering’ we mean returning to a state in which at most 1% are infected.
- 8.
For example, a path could be labelled with multiple atomic propositions in a single iteration.
References
Amazon Elastic Compute Cloud (EC2). http://aws.amazon.com/ec2/
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Ballarini, P., Fisher, M., Wooldridge, M.: Uncertain agent verification through probabilistic model-checking. In: Barley, M., Mouratidis, H., Unruh, A., Spears, D., Scerri, P., Massacci, F. (eds.) SASEMAS 2004-2006. LNCS, vol. 4324, pp. 162–174. Springer, Heidelberg (2009)
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Dekhtyar, M.I., Dikovsky, A.J., Valiev, M.K.: Temporal verification of probabilistic multi-agent systems. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 256–265. Springer, Heidelberg (2008)
Dijkstra, E.W.: Go to statement considered harmful. Commun. ACM 11(3), 147–148 (1968)
Donaldson, R., Gilbert, N.: A monte carlo model checker for probabilistic LTL with numerical constraints. Technical report 282, Department of Computing Science, University of Glasgow (2008)
Fages, F., Rizk, A.: On the analysis of numerical data time series in temporal logic. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 48–63. Springer, Heidelberg (2007)
Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)
Galán, J.M., Izquierdo, L.R., Izquierdo, S.S., Santos, J.I., del Olmo, R., López-Paredes, A., Edmonds, B.: Errors and artefacts in agent-based modelling. J. Artif. Soc. Soc. Simul. 12(1), 1 (2009)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004)
Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Reading (2003)
Izquierdo, L.R., Izquierdo, S.S., Galán, J.M., Santos, J.I.: Techniques to understand computer simulations: markov chain analysis. JASSS 12(1), 6 (2009)
Kleijnen, J.P.C.: Validation of models: statistical techniques and data availability. In: Proceedings 31st Winter Simulation Conference, pp. 647–654. ACM (1999)
Konur, S., Dixon, C., Fisher, M.: Formal verification of probabilistic swarm behaviours. In: Dorigo, M., et al. (eds.) ANTS 2010. LNCS, vol. 6234, pp. 440–447. Springer, Heidelberg (2010)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Midgley, D., Marks, R.E., Kunchamwar, D.: Building and assurance of agent-based models: an example and challenge to the field. J. Bus. Res. 60(8), 884–893 (2007). (Complexities in Markets Special Issue.)
Sargent, R.G.: Verification and validation of simulation models. In: Proceedings of the 40th Conference on Winter Simulation, WSC ’08, pp. 157–169. Winter Simulation Conference (2008)
Stonedahl, F., Wilensky, U.: NetLogo Virus on a Network model. Technical report, Center for Connected Learning and Computer-Based Modeling, Northwestern University, Evanston, IL (2008)
Wan, W., Bentahar, J., Ben Hamza, A.: Model checking epistemic and probabilistic properties of multi-agent systems. In: Mehrotra, K.G., Mohan, ChK, Oh, J.C., Varshney, P.K., Ali, M. (eds.) IEA/AIE 2011, Part II. LNCS(LNAI), vol. 6704, pp. 68–78. Springer, Heidelberg (2011)
Wilensky, U.: NetLogo. Technical report, Center for Connected Learning and Computer-Based Modeling, Northwestern University, Evanston, IL (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herd, B., Miles, S., McBurney, P., Luck, M. (2014). Verification and Validation of Agent-Based Simulations Using Approximate Model Checking. In: Alam, S., Parunak, H. (eds) Multi-Agent-Based Simulation XIV. MABS 2013. Lecture Notes in Computer Science(), vol 8235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54783-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-54783-6_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54782-9
Online ISBN: 978-3-642-54783-6
eBook Packages: Computer ScienceComputer Science (R0)