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 synthesizing 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 synchronization, 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)
Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: Fich, F.E. (ed.) DISC 2003. LNCS, vol. 2848, pp. 136–150. Springer, Heidelberg (2003)
Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. ACM Commun. 22(5), 281–283 (1979)
Chellapilla, K.: Evolving computer programs without subtree crossover. IEEE Trans. Evolutionary Computation 1(3), 209–216 (1997)
Dolev, D., Klawe, M.M., Rodeh, M.: An O ( n logn ) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245–260 (1982)
Emerson, E.A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 325–339. Springer, Heidelberg (2004)
Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)
Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods (extended abstract). In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 438–449. Springer, Heidelberg (1993)
Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: The Spin Verification System, pp. 23–32. American Mathematical Society, Providence (1996)
Holzmann, G.J.: The SPIN Model Checker. Pearson Education, London (2003)
Holzmann, G.J., Peled, D.: An improvement in formal verification. In: FORTE, pp. 197–211 (1994)
Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007)
Katz, G., Peled, D.: Genetic programming and model checking: Synthesizing new mutual exclusion algorithms. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 33–47. Springer, Heidelberg (2008)
Katz, G., Peled, D.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141–156. Springer, Heidelberg (2008)
Katz, G., Peled, D.: Model checking driven heuristic search for correct programs. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 122–131. Springer, Heidelberg (2009)
Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337–359 (1992)
Kinnear Jr., K.E.: Evolving a sort: Lessons in genetic programming. In: IJCNN, vol. 2, pp. 881–888 (1993)
Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)
Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: PODC, pp. 239–247 (1989)
Lamport, L.: A theorem on atomicity in distributed algorithms. Distributed Computing 4, 59–68 (1990)
Le Lann, G.: Distributed systems - towards a formal approach. In: IFIP Congress, pp. 155–160 (1977)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97–107 (1985)
Niebert, P., Peled, D., Pnueli, A.: Discriminative model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 504–516. Springer, Heidelberg (2008)
Oppen, D.C.: A \(2^{2^{2^{pn}}}\) upper bound on the complexity of presburger arithmetic. J. Comput. Syst. Sci. 16(3), 323–332 (1978)
Overman, W.T., Crocker, S.D.: Verification of concurrent systems: Function and timing. In: PSTV, pp. 401–409 (1982)
Peterson, G.L.: An O(n log n) unidirectional algorithm for the circular extrema problem. ACM Trans. Program. Lang. Syst. 4(4), 758–762 (1982)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)
Suzuki, I.: Proving properties of a ring of finite state systems. Inf. Process. Lett. 28(4), 213–314 (1988)
Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. In: STOC, pp. 446–456 (1984)
Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katz, G., Peled, D. (2011). Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming. In: Namjoshi, K., Zeller, A., Ziv, A. (eds) Hardware and Software: Verification and Testing. HVC 2009. Lecture Notes in Computer Science, vol 6405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19237-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-19237-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19236-4
Online ISBN: 978-3-642-19237-1
eBook Packages: Computer ScienceComputer Science (R0)