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

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

  author =       "Gal Katz and Doron Peled",
  title =        "Model Checking-Based Genetic Programming with an
                 Application to Mutual Exclusion",
  booktitle =    "Tools and Algorithms for the Construction and Analysis
                 of Systems",
  year =         "2008",
  editor =       "C. R. Ramakrishnan and Jakob Rehof",
  volume =       "4963",
  series =       "LNCS",
  pages =        "141--156",
  address =      "Budapest, Hungary",
  month =        mar # " 29-" # apr # " 6",
  publisher =    "Springer",
  note =         "Held as Part of the Joint European Conferences on
                 Theory and Practice of Software, ETAPS 2008",
  keywords =     "genetic algorithms, genetic programming, STGP, linear
                 temporal logic",
  isbn13 =       "978-3-540-78799-0",
  DOI =          "doi:10.1007/978-3-540-78800-3_11",
  size =         "16 pages",
  abstract =     "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.",
  notes =        "Fitness based on graph created by model checking, only
                 4 fitness levels per ... but then summed to give
                 combined fitness. Mutation only. Automatic conversion
                 between Buchi and Streett FSM. Approach is doublly
                 exponential: p148 {"}The translation may result in a
                 doubly exponential blowup{"} Deadlock and livelock
                 detection. Parsimony for bloat control leads to smaller

Genetic Programming entries for Gal Katz Doron A Peled