Advertisement

Slicing Agent Programs for More Efficient Verification

  • Michael WinikoffEmail author
  • Louise Dennis
  • Michael Fisher
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11375)

Abstract

Agent programs are increasingly used as the core high-level decision-making components within a range of autonomous systems and, as the deployment of such systems in safety-critical scenarios develops, the need for strong and trustworthy verification becomes acute. Formal verification techniques such as model-checking provide this high level of assurance yet they are typically both complex and slow to deploy. In this chapter we introduce, develop and evaluate a program slicing technique that significantly improves the efficiency of such verification, hence providing more effective routes to the assurance of safety, reliability, and ethics in autonomous systems.

Keywords

Formal verification Program analysis Agent-oriented programming languages 

References

  1. 1.
    Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)CrossRefGoogle Scholar
  2. 2.
    Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Platforms and Applications. Springer, Boston (2005).  https://doi.org/10.1007/b137449CrossRefzbMATHGoogle Scholar
  3. 3.
    El Fallah Seghrouchni, A., Dix, J., Dastani, M., Bordini, R.H. (eds.): Multi-Agent Programming. Springer, Boston (2009).  https://doi.org/10.1007/978-0-387-89299-3zbMATHGoogle Scholar
  4. 4.
    Bordini, R.H., Fisher, M., Wooldridge, M., Visser, W.: Property-based slicing for agent verification. J. Log. Comput. 19(6), 1385–1425 (2009).  https://doi.org/10.1093/logcom/exp029MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bordini, R.H., Hübner, J.F., Wooldridge, M.: Programming Multi-Agent Systems in AgentSpeak Using Jason. Wiley, Chichester (2007)CrossRefGoogle Scholar
  6. 6.
    Boyer, R.S., Moore, J.S. (eds.): The Correctness Problem in Computer Science. Academic Press, London (1981)zbMATHGoogle Scholar
  7. 7.
    Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Cambridge (1987)Google Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000). ISBN 978-0-262-03270-4Google Scholar
  9. 9.
    DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems of programs. ACM Commun. 22(5), 271–280 (1979)CrossRefGoogle Scholar
  10. 10.
    Dennis, L., Fisher, M., Slavkovik, M., Webster, M.: Formal verification of ethical choices in autonomous systems. Robot. Auton. Syst. 77, 1–14 (2016).  https://doi.org/10.1016/j.robot.2015.11.012CrossRefGoogle Scholar
  11. 11.
    Dennis, L.A.: Gwendolen semantics: 2017. Technical report ULCS-17-001, Department of Computer Science, University of Liverpool (2017)Google Scholar
  12. 12.
    Dennis, L.A., Fisher, M., Lincoln, N.K., Lisitsa, A., Veres, S.M.: Practical verification of decision-making in agent-based autonomous systems. Autom. Softw. Eng. 23(3), 305–359 (2016).  https://doi.org/10.1007/s10515-014-0168-9CrossRefGoogle Scholar
  13. 13.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier, Amsterdam (1990)Google Scholar
  14. 14.
    Fetzer, J.H.: Program verification: the very idea. ACM Commun. 31(9), 1048–1063 (1988)CrossRefGoogle Scholar
  15. 15.
    Fisher, M., Dennis, L.A., Webster, M.: Verifying autonomous systems. ACM Commun. 56(9), 84–93 (2013)CrossRefGoogle Scholar
  16. 16.
    Georgeff, M.P., Lansky, A.L.: Procedural knowledge. Proc. IEEE Spec. Issue Knowl. Represent. 74, 1383–1398 (1986)Google Scholar
  17. 17.
    Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J.C.: Agent programming with declarative goals. In: Castelfranchi, C., Lespérance, Y. (eds.) ATAL 2000. LNCS (LNAI), vol. 1986, pp. 228–243. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44631-1_16CrossRefGoogle Scholar
  18. 18.
    Ingrand, F.F., Georgeff, M.P., Rao, A.S.: An architecture for real-time reasoning and system control. IEEE Expert 7(6), 34–44 (1992)CrossRefGoogle Scholar
  19. 19.
    Jongmans, S.-S.T.Q., Hindriks, K.V., van Riemsdijk, M.B.: Model checking agent programs by using the program interpreter. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) CLIMA 2010. LNCS (LNAI), vol. 6245, pp. 219–237. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14977-1_17CrossRefGoogle Scholar
  20. 20.
    Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Sci. Comput. Program. 148, 88–106 (2017).  https://doi.org/10.1016/j.scico.2017.05.006CrossRefGoogle Scholar
  21. 21.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_55CrossRefGoogle Scholar
  22. 22.
    Rao, A.S., Georgeff, M.P.: An abstract architecture for rational agents. In: Proceedings of 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 439–449 (1992)Google Scholar
  23. 23.
    Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: Van de Velde, W., Perram, J.W. (eds.) MAAMAW 1996. LNCS, vol. 1038, pp. 42–55. Springer, Heidelberg (1996).  https://doi.org/10.1007/BFb0031845CrossRefGoogle Scholar
  24. 24.
    Webster, M., Cameron, N., Fisher, M., Jump, M.: Generating certification evidence for autonomous unmanned aircraft using model checking and simulation. J. Aerosp. Inf. Syst. 11(5), 258–279 (2014)Google Scholar
  25. 25.
    Winikoff, M., Cranefield, S.: On the testability of BDI agent systems. J. Artif. Intell. Res. (JAIR) 51, 71–131 (2014).  https://doi.org/10.1613/jair.4458MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Winikoff, M.: An AgentSpeak meta-interpreter and its applications. In: Bordini, R.H., Dastani, M.M., Dix, J., El Fallah Seghrouchni, A. (eds.) ProMAS 2005. LNCS (LNAI), vol. 3862, pp. 123–138. Springer, Heidelberg (2006).  https://doi.org/10.1007/11678823_8CrossRefGoogle Scholar
  27. 27.
    Winikoff, M.: Jack\({}^{\text{ TM }}\) intelligent agents: an industrial strength platform. In: Bordini, R.H., Dastani, M., Dix, J., Fallah-Seghrouchni, A.E. (eds.) Multi-Agent Programming: Languages, Platforms and Applications, Multiagent Systems, Artificial Societies, and Simulated Organizations, vol. 15, pp. 175–193. Springer, Boston (2005).  https://doi.org/10.1007/0-387-26350-0_7CrossRefGoogle Scholar
  28. 28.
    Winikoff, M.: BDI agent testability revisited. J. Auton. Agents Multi-Agent Syst. (JAAMAS) 31(5), 1094–1132 (2017).  https://doi.org/10.1007/s10458-016-9356-2CrossRefGoogle Scholar
  29. 29.
    Wooldridge, M., Rao, A. (eds.): Foundations of Rational Agency. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (1999).  https://doi.org/10.1007/978-94-015-9204-8CrossRefzbMATHGoogle Scholar
  30. 30.
    Zhao, J., Cheng, J., Ushijima, K.: Literal dependence net and its use in concurrent logic programming environment. In: Proceedings of the Workshop on Parallel Logic Programming (Held with FGCS 1994), pp. 127–141 (1994)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Michael Winikoff
    • 1
    Email author
  • Louise Dennis
    • 2
  • Michael Fisher
    • 2
  1. 1.Victoria University of WellingtonWellingtonNew Zealand
  2. 2.Liverpool UniversityLiverpoolUK

Personalised recommendations