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

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

@InProceedings{DBLP:conf/hvc/KatzP09,

• 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 2009",
• 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 checks'.",
• bibsource = "DBLP, http://dblp.uni-trier.de",

}

Genetic Programming entries for Gal Katz Doron A Peled

Citations