Integrating Model Checking and Inductive Logic Programming

  • Dalal Alrajeh
  • Alessandra Russo
  • Sebastian Uchitel
  • Jeff Kramer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7207)


Inductive Logic Programming can be used to provide automated support to help correct the errors identified by model checking, which in turn provides the relevant context for learning hypotheses that are meaningful within the domain of interest. Model checking and Inductive Logic Programming can thus be seen as two complementary approaches with much to gain from their integration. In this paper we present a general framework for such an integration, discuss its main characteristics and present an overview of its application.


Model Check Logic Program Linear Temporal Logic Inductive Logic Inductive Logic Programming 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alrajeh, D.: Requirements Elaboration using Model Checking and Inductive Learning. PhD thesis, Imperial College London, London, U.K. (2010)Google Scholar
  2. 2.
    Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: Deriving non-zeno behaviour models from goal models using ILP. J. Form. Asp. Comput. 22, 217–241 (2010)zbMATHCrossRefGoogle Scholar
  3. 3.
    Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: An inductive approach for modal transition system refinement. In: Technical Communications of the 27th Intl. Conf. on Logic Programming, pp. 106–116 (2011)Google Scholar
  4. 4.
    Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  6. 6.
    Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K. (eds.) Proc. of 5th Intl. Conf. on Logic Programming, pp. 1070–1080 (1988)Google Scholar
  7. 7.
    Giannakopoulou, D., Kramer, J., Cheung, S.: Behaviour analysis of distributed systems using the tracta approach. Autom. Softw. Eng. 6(1), 7–35 (1999)CrossRefGoogle Scholar
  8. 8.
    Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proc. of the 9th European Softw. Eng. Conf., pp. 257–266 (2003)Google Scholar
  9. 9.
    ITU. Message Sequence Charts. Intl. Telecommunications Union, Telecommunication Standardisation Sector (1996)Google Scholar
  10. 10.
    Jackson, M.: The world and the machine. In: Proceedings of the 17th International Conference on Software Engineering, pp. 283–292 (1995)Google Scholar
  11. 11.
    Keller, R.M.: Formal verification of parallel programs. Communications of the ACM 19(7), 371–384 (1976)zbMATHCrossRefGoogle Scholar
  12. 12.
    Kowalski, R.A., Sergot, M.: A logic-based calculus of events. New Generation Computing 4(1), 67–95 (1986)CrossRefGoogle Scholar
  13. 13.
    Letier, E., van Lamsweerde, A.: Deriving operational software specifications from system goals. In: Proc. of 10th ACM SIGSOFT Symp. on Foundations of Softw. Eng., pp. 119–128 (2002)Google Scholar
  14. 14.
    Lifschitz, V.: Answer set planning. In: ICLP, pp. 23–37 (1999)Google Scholar
  15. 15.
    Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. John Wiley and Sons (1999)Google Scholar
  16. 16.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer (1992)Google Scholar
  17. 17.
    Muggleton, S.: Inverse entailment and Progol. New Generation Computing 13, 245–286 (1995)CrossRefGoogle Scholar
  18. 18.
    Muggleton, S., de Raedt, L.: Inductive logic programming: Theory and methods. The Journal of Logic Programming 19-20(suppl. 1), 629–679 (1994)CrossRefGoogle Scholar
  19. 19.
    Nédellec, C., Rouveirol, C., Adé, H., Bergadano, F., Tausend, B.: Declarative bias in ILP. In: Advances in Inductive Logic Programming, vol. 32, pp. 82–103 (1996)Google Scholar
  20. 20.
    Ray, O.: Nonmonotonic abductive inductive learning. J. of Applied Logic 7(3), 329–340 (2009)zbMATHCrossRefGoogle Scholar
  21. 21.
    Sakama, C., Inoue, K.: Brave induction: a logical framework for learning from incomplete information. Machine Learning 76, 3–35 (2009)CrossRefGoogle Scholar
  22. 22.

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Dalal Alrajeh
    • 1
  • Alessandra Russo
    • 1
  • Sebastian Uchitel
    • 1
    • 2
  • Jeff Kramer
    • 1
  1. 1.Imperial College LondonUK
  2. 2.University of Buenos Aires/CONICETArgentina

Personalised recommendations