- author = "Gal Katz and Doron Peled",
- title = "Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms",
- booktitle = "Automated Technology for Verification and Analysis",
- year = "2008",
- volume = "5311",
- series = "Lecture Notes in Computer Science",
- pages = "33--47",
- publisher = "Springer",
- keywords = "genetic algorithms, genetic programming, SBSE, EmCTL, LTL",
- isbn13 = "978-3-540-88386-9",
-
DOI = "
doi:10.1007/978-3-540-88387-6_5",
- size = "15 pages",
- abstract = "Recently, genetic programming and model checking were combined for synthesizing algorithms that satisfy a given specification \cite{Katz:2008:TACAS},\cite{eurogp07:johnson}. In particular, we demonstrated this approach by developing a tool that was able to rediscover the classical mutual exclusion algorithms \cite{Katz:2008:TACAS} with two or three global bits. In this paper we extend the capabilities of the model checking-based genetic programming and the tool built to experiment with this approach. In particular, we add qualitative requirements involving locality of variables and checks, which are typical of realistic mutual exclusion algorithms. The genetic process mimics the actual development of mutual exclusion algorithms, by starting with an existing correct solution, which does not satisfy some performance requirements, and converging into a solution that satisfies these requirements. We demonstrate this by presenting some nontrivial new mutual exclusion algorithms, discovered with our tool.",
-
notes = "ATVA 2008
Buchi automata. p40 EXSPACE, 2EXPTIME. Three shared bits, memory. Tarjan's strongly connected graph algorithm. Runtime <14mins.",
