Earlier in my career, I worked on using executable logical descriptions to
produce software that is "correct by construction":
Over a number of years I introduced, and helped develop, a leading
approach to automated proof in temporal logics:
- Fisher, M., and Owens, R., (eds) Executable Modal and Temporal
Volume 897 of Lecture Notes in Artificial
Intelligence, Springer-Verlag, 1995. (ISBN: 3-540-58976-7)
- Barringer, H., Fisher, M., Gabbay, D., Owens, R., and
Reynolds, M., (eds)
The Imperative Future: Principles of Executable
Temporal Logic. Research Studies Press, May
1996. (ISBN: 0-86380-190-0)
As formal techniques can be used to provide a novel route to the
automated, logical analysis (through
model-checking) of autonomous decision-making software (in the
form of agents), we produced one of the first formal agent verification systems:
- Fisher, M., Dixon, C., and Peim, M. Clausal
ACM Transactions on Computational
2(1):12-56. January 2001.
- Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U.
Mechanizing First-Order Temporal Resolution.
Elsevier Science, 2005.
- Degtyarev, A., Fisher, M., and Konev, B. Monodic
Temporal Resolution. ACM
Transactions on Computational Logic
Work with increasingly realistic scenarios then led on to
development of the first viable (and still leading) fully automated
verification system for practical rational agent programs:
It became clear that this work could have importance across
autonomous systems engineering and so, in collaboration with
engineers, my work has turned to analysing and developing practical
autonomous systems, primarily across aerospace and robotics:
- Bordini, R. H., Fisher, M., Visser, W., and Wooldridge, M.
Verifying Multi-Agent Programs by Model
Checking. Journal of
Autonomous Agents and Multi-Agent Systems
Springer, March 2006.
- Bordini, R. H., Fisher, M., Wooldridge, M., and Visser, W.
Property-based Slicing for Agent
Verification. Journal of Logic and
The last of these is particularly important, having an impact on how
certification for truly autonomous unmanned air systems might
- Dennis, L. A., Fisher, M., Lisitsa, A., Lincoln, N., and Veres, S. M.
Satellite Control Using Rational Agent Programming.
25(3):92-97, May/June, 2010.
- Konur, S., Dixon, C., and Fisher, M. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems 60(2):199-213, 2012.
- Lincoln, N., Veres, S. M., Dennis, L. A., Fisher, M., and Lisitsa, A. Autonomous Asteroid Exploration by Rational Agents. IEEE Computational Intelligence 8(4):25-38, 2013.
- Webster, M., Cameron, N., Jump, M., Fisher, M. Generating Certification Evidence for Autonomous Unmanned
Aircraft Using Model Checking and Simulation. Journal of Aerospace Information Systems 11(5):258-279, May 2014.
It is now clear not only that this underlying verification
technology is relevant across very many different autonomous and
robotic systems, but that such verification is essential if these
systems are to be accepted by engineers, certified by regulators, and
trusted by the public. Consequently, we promote this approach to verifiable
and are applying verification techniques across ethics, crowds, teamwork, human-robot interaction, and practical autonomous system verification:
- Dennis, L. A., Fisher, M., Slavkovik, M., and Webster, M. Formal Verification of Ethical Choices in Autonomous Systems.
Robotics and Autonomous Systems, 2016.
- Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K-L.,
Dautenhahn, K., and Saez-Pons, J.
Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study
IEEE Transactions on Human-Machine Systems, 2016.
- Dennis, L. A., Fisher, M., Lincoln, N., Lisitsa, A., and Veres, S. M.
Practical Verification of Decision-Making in Agent-Based Autonomous Systems
Automated Software Engineering, 2016.
- Slavkovik, M., Dennis, L. A., and Fisher, M. An Abstract Formal Basis for Digital Crowds. Distributed and Parallel Databases 33(1):3-31, 2015.
- Konur, S., Fisher, M., and Schewe, S. Combined Model Checking for Temporal, Probabilistic, and Real-time Logics. Theoretical Computer Science 503:61-88, 2013.