Using Model Checking Techniques For Evaluating the Effectiveness of Evolutionary Computing in Synthesis of Distributed Fault-Tolerant Programs

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

@InProceedings{Zhu:2015:GECCO,

• author = "Ling Zhu and Sandeep Kulkarni",
• title = "Using Model Checking Techniques For Evaluating the Effectiveness of Evolutionary Computing in Synthesis of Distributed Fault-Tolerant Programs",
• booktitle = "GECCO '15: Proceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation",
• year = "2015",
• editor = "Sara Silva and Anna I Esparcia-Alcazar and Manuel Lopez-Ibanez and Sanaz Mostaghim and Jon Timmis and Christine Zarges and Luis Correia and Terence Soule and Mario Giacobini and Ryan Urbanowicz and Youhei Akimoto and Tobias Glasmachers and Francisco {Fernandez de Vega} and Amy Hoover and Pedro Larranaga and Marta Soto and Carlos Cotta and Francisco B. Pereira and Julia Handl and Jan Koutnik and Antonio Gaspar-Cunha and Heike Trautmann and Jean-Baptiste Mouret and Sebastian Risi and Ernesto Costa and Oliver Schuetze and Krzysztof Krawiec and Alberto Moraglio and Julian F. Miller and Pawel Widera and Stefano Cagnoni and JJ Merelo and Emma Hart and Leonardo Trujillo and Marouane Kessentini and Gabriela Ochoa and Francisco Chicano and Carola Doerr",
• isbn13 = "978-1-4503-3472-3",
• pages = "1119--1126",
• keywords = "genetic algorithms, genetic programming",
• month = "11-15 " # jul,
• organisation = "SIGEVO",
• address = "Madrid, Spain",
• URL = "http://doi.acm.org/10.1145/2739480.2754779",
• DOI = "doi:10.1145/2739480.2754779",
• publisher = "ACM",
• publisher_address = "New York, NY, USA",
• abstract = "In most applications using genetic programming (GP), objective functions are obtained by a terminating calculation. However, the terminating calculation cannot evaluate distributed fault-tolerant programs accurately. A key distinction in synthesizing distributed fault-tolerant programs is that they are inherently non-deterministic, potentially having infinite computations and executing in an unpredictable environment. In this study, we apply a model checking technique - Binary Decision Diagrams (BDDs) - to GP, evaluating distributed programs by computing reachable states of the given program and identifying whether it satisfies its specification. We present scenario-based multi-objective approach that each program is evaluated under different scenarios which represent various environments. The computation of the programs are considered in two different semantics respectively: interleaving and maximum-parallelism. In the end, we illustrate our approach with a Byzantine agreement problem, a token ring problem and a consensus protocol using failure detector S. For the first time, this work automatically synthesizes the consensus protocol with S. The results show the proposed method enhances the effectiveness of GP in all studied cases when using maximum-parallelism semantic.",
• notes = "Also known as \cite{2754779} GECCO-2015 A joint meeting of the twenty fourth international conference on genetic algorithms (ICGA-2015) and the twentith annual genetic programming conference (GP-2015)",

}

Genetic Programming entries for Ling Zhu Sandeep Kulkarni

Citations