Formal proof of abstraction for agent-based learning systems
Ryan Fraser Kirwan, Alice Ann Miller · ENLIGHTEN (Jurnal Bimbingan dan Konseling Islam) · 2013
We describe herein a formal proof of a simulation relation between a model of an Agent-Based Learning (ABL) system and our abstraction of it. Proving that a simulation relation exists means that all LTL properties we verify, via Model checking [4], for our abstraction also hold true in the original model. Formalising this relation allows us to apply the same abstraction technique to other ABL systems safe in the knowledge that a similar simulation relation will exist.