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
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)