Practical Verification of Decision-making in Agent-based Autonomous Systems
Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa and Sandor M. Veres
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.
Instructions for running the experiment:
$ mkdir SomeDir $ cd SomeDir $ vagrant init SomeName http://recomputation.org/library/journals/dennise14-ase.box $ vagrant up
Size: 1,038 MB | MD5: 57a70039b980f313aa44f454571b6254 | Download Experiment
- Approximate execution time - using configuration decribed in paper: 5 hours
- Approximate execution time - using above VM: 5 - 10 hours (dependent on host system)
Please follow instructions in the README file placed within the vagrant home directory. Given below is the command to login to VM from the host computer after the VM has been successfully started using the
vagrant up command.
$ vagrant ssh <VM>$ (type commands to run experiments)
To exit to the host machine from the VM type: