An ACO approach to model checking

Ant Colony Optimization is a computational model inspired by the way
colonies of ant organizes their food foraging. The mechanism relies on
randomization and evaporation. Various NP-complete problem can be
approximated by ACO-based algorithms, e.g., travelling sales man and
set cover.

Starting point of the proposed graduation project is an ACO-algorithm
for SAT as presented in [1]. After mastering the technique, the
suitability of ACO for the model checking problems of CTL and the
mu-calculus can be investigated. An alternate direction is to study,
in a more abstract setting, adaptability of decision making based on
ACO in dynamic settings as initiated in [2].

[1] D. Moritz & M. Springer, Solving Satisfiability with Ant Colony
Optimization and Genetic Algorithms, University of Potsdam, 2010.

[2] C.Krause, E.P. de Vink & P.J. de Vink, Towards Dynamics Adaptation of
the Majority Rule Scheme, workshop proceedings QAPL 2013, Rome, 2013.