Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms

Created by W.Langdon from gp-bibliography.bib Revision:1.4192

  author =       "Gal Katz and Doron Peled",
  title =        "Genetic Programming and Model Checking: Synthesizing
                 New Mutual Exclusion Algorithms",
  booktitle =    "Automated Technology for Verification and Analysis",
  year =         "2008",
  volume =       "5311",
  series =       "Lecture Notes in Computer Science",
  pages =        "33--47",
  publisher =    "Springer",
  keywords =     "genetic algorithms, genetic programming, SBSE, EmCTL,
  isbn13 =       "978-3-540-88386-9",
  URL =          "",
  DOI =          "doi:10.1007/978-3-540-88387-6_5",
  size =         "15 pages",
  abstract =     "Recently, genetic programming and model checking were
                 combined for synthesizing algorithms that satisfy a
                 given specification
                 \cite{Katz:2008:TACAS},\cite{eurogp07:johnson}. In
                 particular, we demonstrated this approach by developing
                 a tool that was able to rediscover the classical mutual
                 exclusion algorithms \cite{Katz:2008:TACAS} with two or
                 three global bits. In this paper we extend the
                 capabilities of the model checking-based genetic
                 programming and the tool built to experiment with this
                 approach. In particular, we add qualitative
                 requirements involving locality of variables and
                 checks, which are typical of realistic mutual exclusion
                 algorithms. The genetic process mimics the actual
                 development of mutual exclusion algorithms, by starting
                 with an existing correct solution, which does not
                 satisfy some performance requirements, and converging
                 into a solution that satisfies these requirements. We
                 demonstrate this by presenting some nontrivial new
                 mutual exclusion algorithms, discovered with our
  notes =        "ATVA 2008

                 Buchi automata. p40 EXSPACE, 2EXPTIME. Three shared
                 bits, memory. Tarjan's strongly connected graph
                 algorithm. Runtime <14mins.",

Genetic Programming entries for Gal Katz Doron A Peled