Model Checking-Based Genetic Programming with an Application to Mutual Exclusion

  • Gal Katz
  • Doron Peled
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


Two approaches for achieving correctness of code are verification and synthesis from specification. Evidently, it is easier to check a given program for correctness (although not a trivial task by itself) than to generate algorithmically correct-by-construction code. However, formal verification may give quite limited information about how to correct the code. Genetic programming repeatedly generates mutations of code, and then selects the mutations that remain for the next stage based on a fitness function, which assists in converging into a correct program. We use a model checking procedure to provide the fitness value in every stage. As an example, we generate algorithms for mutual exclusion, using this combination of genetic programming and model checking. The main challenge is to select a fitness function that will allow constructing correct solutions with minimal effort. We present our considerations behind the selection of a fitness function based not only on the classical outcome of model checking, i.e., the existence of an error trace, but on the complete graph constructed during the model checking process.


Model Check Genetic Programming Critical Section Mutual Exclusion Linear Temporal Logic 
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.


  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  2. 2.
    Perrig, A., Song, D.: Looking for diamonds in the desert - extending automatic protocol generation to three-party authentication and key agreement protocols. In: CSFW, pp. 64–76 (2000)Google Scholar
  3. 3.
    Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: Fich, F.E. (ed.) DISC 2003. LNCS, vol. 2848, pp. 136–150. Springer, Heidelberg (2003)Google Scholar
  4. 4.
    Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005)Google Scholar
  7. 7.
    Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)zbMATHGoogle Scholar
  8. 8.
    Holland, J.H.: Adaptation in Natural and Artificial Systems: An Introductory Analysis with Applications to Biology, Control and Artificial Intelligence. MIT Press, Cambridge (1992)Google Scholar
  9. 9.
    Montana, D.J.: Strongly typed genetic programming. Evolutionary Computation 3(2), 199–230 (1995)CrossRefGoogle Scholar
  10. 10.
    Banzhaf, W., Nordin, P., Keller, R.E., Francone, F.D.: Genetic Programming – An Introduction; On the Automatic Evolution of Computer Programs and its Applications, 3rd edn. Morgan Kaufmann, San Francisco (2001)Google Scholar
  11. 11.
    Schwefel, H.P.P.: Evolution and Optimum Seeking: The Sixth Generation. John Wiley & Sons, Inc. New York (1993)Google Scholar
  12. 12.
    Safra, S., Vardi, M.Y.: On ω automata and temporal logic. In: 21th Annual Symp. on Theory of Computing, pp. 127–137 (1989)Google Scholar
  13. 13.
    Safra, S.: Complexity of automata on infinite objects. PhD thesis, Rehovot, Israel (1989)Google Scholar
  14. 14.
    Emerson, E.A.: Automata, tableaux and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79–88. Springer, Heidelberg (1985)Google Scholar
  15. 15.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. IEEE Symp. on Logic in Computer Science, Boston, July 1986, pp. 332–344 (1986)Google Scholar
  18. 18.
    Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 445–459. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: DAC, pp. 596–602 (1994)Google Scholar
  20. 20.
    Angeline, P.J.: Genetic programming and emergent intelligence. In: Advances in Genetic Programming, pp. 75–98. MIT Press, Cambridge (1994)Google Scholar
  21. 21.
    Tackett, W.A.: Recombination, selection, and the genetic construction of computer programs. PhD thesis, Los Angeles, CA, USA (1994)Google Scholar
  22. 22.
    Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)CrossRefGoogle Scholar
  23. 23.
    Burns, J.E., Lynch, N.A.: Bounds on shared memory for mutual exclusion. Information and Computation 107(2), 171–184 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Peterson, G.L., Fischer, M.J.: Economical solutions to the critical section problem in a distributed system. In: ACM Symposium on Theory of Computing (STOC), pp. 91–97 (1977)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Gal Katz
    • 1
  • Doron Peled
    • 1
  1. 1.Department of Computer ScienceBar Ilan UniversityRamat GanIsrael

Personalised recommendations