Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming

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

  author =       "Gal Katz and Doron Peled",
  title =        "Synthesizing Solutions to the Leader Election Problem
                 Using Model Checking and Genetic Programming",
  booktitle =    "5th International Haifa Verification Conference, HVC
  year =         "2009",
  editor =       "Kedar S. Namjoshi and Andreas Zeller and Avi Ziv",
  series =       "Lecture Notes in Computer Science",
  volume =       "6405",
  pages =        "117--132",
  address =      "Haifa, Israel",
  month =        oct # " 19-22",
  publisher =    "Springer",
  note =         "Revised Selected Papers published 2011",
  keywords =     "genetic algorithms, genetic programming, SBSE",
  isbn13 =       "978-3-642-19236-4",
  DOI =          "doi:10.1007/978-3-642-19237-1_13",
  size =         "16 pages",
  abstract =     "In recent papers [13,14,15], we demonstrated a
                 methodology for developing correct-by-design programs
                 from temporal logic specification using genetic
                 programming. Model checking the temporal specification
                 is used to calculate the fitness function for candidate
                 solutions, which directs the search from initial
                 randomly generated programs towards correct solutions.
                 This method was successfully demonstrated by
                 constructing solutions for the mutual exclusion
                 problem; later, we also imposed some realistic
                 constraints on access to variables. While the results
                 were encouraging for using the genetic synthesis
                 method, the mutual exclusion example includes some
                 limitations that fit well with the constraints of model
                 checking: the goal was finding a fixed finite state
                 program, and its state space was moderately small.
                 Here, in a more realistic setting, we challenge the
                 problem of synthesising a solution for the well known
                 leader election problem; under this problem, a
                 circular, unidirectional network with message passing
                 is seeking the identity of a process with a maximal
                 value. This identity, once found, can be used for
                 synchronisation, breaking symmetry and other network
                 applications. The problem is challenging since it is
                 parametric, and the state space of the solutions grows
                 up exponentially with the number of processes.",
  notes =        "Hardware and Software: Verification and Testing. Tool.
                 mutation only, 'correct-by-design' O(n**2), 'model
                 checking of instances in an incremental way' n 'grows
                 with the fitness level of the candidate solution'.
                 'large confidence'. Evolved programs 'tend to be
                 specific to some ring sizes', 'additional structural
  bibsource =    "DBLP,",

Genetic Programming entries for Gal Katz Doron A Peled