Ant Colony Optimization. Innovation in Verification

Looking for better ways to search a huge state space in model checking, Ant Colony Optimization (ACO) is one possible approach. Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone. The authors presented the paper in the Biologically inspired Information and Communications Technologies 2015 conference. At publication the authors were at The Tokyo University of Science, NIT and SRA, all in Japan.

ACO is a method to efficiently find paths through a large state space using swarm intelligence. You might first want to read this intro to the general ACO technique here. The main refinement in this month’s paper adds a pheromone for the food (goal) to the pheromone trail the ants leave. The paper proposes a method using ACO to validate safety properties (a bad thing doesn’t happen). The method treats the property as a food source. If the ants find a path to the property that becomes a counterexample.

ACO has been studied for many optimization domains – the travelling salesman problem, scheduling, device sizing, antenna optimization and more. Google Scholar shows it as a very popular area for study – over 13k results for 2022 alone.

Paul’s view

What an eye-catching title for a paper! I wasn’t aware of ant colony optimization (ACO) as a technique for shortest path finding in a graph. Seeing this paper prompted me to first take a short random walk (no pun intended!) on the internet to learn more. Wikipedia was a good place to start as always.

In nature ants find an efficient path from their nest to some food though pheromones. They wander around randomly but with a bias towards walking where other ants have traveled before. Ants taking a shorter route from nest to food will make more trips in a time interval compared to ants taking longer routes. When integrated over thousands of ants making hundreds of journeys, shorter paths get more ant traffic which means more pheromones on those paths. Hence even more ants take those paths, until eventually all ants are marching in a continuous stream along the shortest path from nest to food..

ACO mimics this method algorithmically to find a shortest path through a graph. The probability of an ant following an edge in a graph depends on a combination of a static weight for that edge (e.g. 1/d where d is the distance along that edge) and a “pheromonal” weight that depends on how many other ants walked that same edge recently.

This month’s paper is on using ACO for model checking – to help efficiently search for a shortest path from initial state to error state in the state graph of a circuit. The authors’ key contribution is to augment the classic ACO edge probability function with a third component, a “goal pheromone”, to model ants “smelling” a food source. With each iteration of the ACO algorithm (where ants pick and walk along some edge in the graph), the goal pheromone simultaneously propagates backwards along edges starting from the error states (i.e. the food/goal) of the circuit. The goal pheromone assigns a much higher probability to an edge than a regular ant pheromone, so ants are most likely to walk along any edge they reach that is marked by the goal pheromone.

It’s a neat idea, and the paper is well written and easy to understand. However, the authors acknowledge that in any complex circuit the path depth from initial to error state is deep. So tracing backwards from the error states doesn’t particularly help. The search space diverges long before any ant can “smell” the food. Also, in the BDD/SAT-based world there are many other symbolic methods to narrow the search space in model checking. These would need to be benchmarked with ACO before a compelling commercial case for using it could be made.

Raúl’s view

In this 2015 paper, Kumazawa et.al. present an extension to Ant Colony Optimization (ACO) for model checking. The state of the art then was ACOhg – ACO for huge graphs. ACOhg differs from ACO in limiting the number of steps an ant can take to λc  to reduce the time and memory consumption. This limit may prevent ants from finding a final state that violates the property, so must be tuned carefully. The extension in this paper, EACOhg (Extended ACOhg) introduces an additional goal pheromone that mimics the smell from food in the real world and is stronger than the normal ant pheromone. The goal pheromone is put on transition edges once a final state is reached, and these edges are selected in preference to the edges with the normal pheromone.

Experimental results on 3 examples with 3843, 31747 and 266,218 states respectively are compared with ACOhg. They show a reduction in execution time of 10-45%. This with a slight increase in memory consumption of up to 5% (to hold the goal pheromones). Most important, the show reduction of the length of counterexamples (path length to a violation of the property being verified) of 15%-70%. Since gains are smallest in the largest model, the authors hypothesize that “the reason may be that the effect of smell- like pheromone is compromised in a large model” and plan to overcome that in future work.

The paper is largely self-contained and is an easy and enjoyable read. Results are meaningfully better the prior state-of-the-art, but the method is heuristic and requires some tuning. The authors list 9 coefficients which they deem to be “the best settings we decided through preliminary experiments”. They do not discuss the length of these experiments. And the usefulness of these coefficients for a different set of problems is not a given. Overall, a good introduction to ACO. I’m not aware of EDA solutions that use ACO in practice, but “the use of ACO for the solution of dynamic, multiobjective, stochastic, continuous and mixed-variable optimization problems is a current hot topic, as well as the creation of parallel implementations capable of taking advantage of the new available parallel hardware” [scholarpedia.org], giving about 10,000 hits for 2022 alone in Google scholar.