Progress on model checking robot behaviour
Ryan Fraser Kirwan, Alice Ann Miller · ENLIGHTEN (Jurnal Bimbingan dan Konseling Islam) · 2012
We model systems that involve a learning robot which interacts with obstacles in a static environment. Our models are specified in Promela with a view to verifying them using SPIN [2]. Because of the complex nature of these systems our initial models have intractable state-spaces: we aren’t able to model check them. Last year [4] we introduced an abstraction technique to greatly reduce the state-space of our models. One of the challenges we now face is to prove that our abstraction technique is correct i.e., it preserves the properties of concern.