Improving swarming using genetic algorithms

From LRDE

Abstract

The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonethelessthe topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation is 10% faster than state-of-the-art algorithms on a general benchmark and 40% on a specialized benchmark. Even if we expected a decrease in an order of magnitude, these results are still encouraging since they suggest a new way to handle existing limitations. Empirically, our technique seems well suited for "linear topology", i.e., the one we can obtain when combining model checking algorithms with partial-order reduction techniques.

Documents

Bibtex (lrde.bib)

@Article{	  renault.20.isse,
  author	= {Etienne Renault},
  title		= {Improving swarming using genetic algorithms},
  journal	= {Innovations in Systems and Software Engineering: a NASA
		  journal (ISSE)},
  year		= 2020,
  volume	= {16},
  number	= {2},
  pages		= {143--159},
  month		= jun,
  publisher	= {Springer},
  abstract	= { The verification of temporal properties against a given
		  system may require the exploration of its full state space.
		  In explicit model checking, this exploration uses a
		  depth-first search and can be achieved with multiple
		  randomized threads to increase performance. Nonetheless,
		  the topology of the state space and the exploration order
		  can cap the speedup up to a certain number of threads. This
		  paper proposes a new technique that aims to tackle this
		  limitation by generating artificial initial states, using
		  genetic algorithms. Threads are then launched from these
		  states and thus explore different parts of the state space.
		  Our prototype implementation is 10\% faster than
		  state-of-the-art algorithms on a general benchmark and 40\%
		  on a specialized benchmark. Even if we expected a decrease
		  in an order of magnitude, these results are still
		  encouraging since they suggest a new way to handle existing
		  limitations. Empirically, our technique seems well suited
		  for "linear topology", i.e., the one we can obtain when
		  combining model checking algorithms with partial-order
		  reduction techniques. },
  doi		= {10.1007/s11334-020-00362-7}
}