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

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

@InProceedings{Katz:2008:TACAS,

• 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 programs.",

}

Genetic Programming entries for Gal Katz Doron A Peled

Citations