Formal methods and programming tools for modeling ant colonies

Nature inspired algorithms have growing up interest in the area of optimization,and the class of ant colony optimization algorithms is one of the recently developedinstances of such algorithms. Ant Colony Optimization, ACO, algorithms rely on thebasic behavior of ants that is known as foraging behavior, which helps the antcolonies to find the shortest path among a number of possible choices. This isachieved by laying down a chemical substance, called pheromone, on the groundwhile moving; and preference of the paths with high pheromone level by thesuccessor ants. This type of behavior is also called social behavior in more abstractlevel, and covers many biological phenomena.There are two directions in dealing with the social behavior observed in antcolonies; one is transferring the idea to solve optimization problems, leading to theant colony algorithms, and the other one is formal modeling of the behavior followedwith a proper verification schema for better understanding of the relationshipbetween the local interactions of individuals in colonies, and the global dynamicalbehavior of the colony. Through formal modeling, and a proper verification approachnot only social behavior, but various aspects of ant behavior can be investigated.In this thesis, we have followed both directions. There are some applicationsdeveloped employing ACO algorithms for solving a real world problem, and aproblem from operations research area. In addition, the application developed forTraveling Salesman Problem serves for better understanding of the algorithm.However, much of the efforts have been spent for formal modeling, verification, anddeveloping an automated modeling tool.Among a variety of formal modeling languages, Weighted Synchronized Calculusof Communicating Systems, WSCCS, has been chosen which is a probabilistic statebased transition process algebra. However, modeling itself brings no insight unless itis combined with a verification schema. Verification aims to confirm the correctnessof the abstract model against its specification, and also to bring front the properties ofcolony being studied via asking some questions to the model. Model checking is atechnique of verification, and concerns to verify the model for a given property.In order to verify the correctness of the model, model checking approach has beenemployed. Since model checking can be performed via temporal logics, probabilisticComputation Tree Logic is another issue dealt with which is then extended to be ableto cover the notion of action.Combining the model checking and formal modeling by WSCCS can beaccomplished through transforming the model into a discrete state space withcorresponding transitions. Therefore, Labeled Kripke Transition Systems (LKTS) isanother formalism introduced, and extended to wrap the probability and action in itsstate transitions.The main achievements addressed in the thesis are: the ACO applicationsdeveloped to solve optimization problems, an investigation of WSCCS for modelingant colonies, extending the CTL and LKTS such that both systems allow representingprobabilistic action occurrences which is the most important property of WSCCS,designing a model checking schema that permits to query the model for probabilisticaction occurrences, and implementing a tool in order to automate the whole process.Keywords: Ant Colony Optimization (ACO), social behavior, WeightedSynchronized Calculus of Communicating Systems (WSCCS), model checking,probabilistic computation tree logic (PCTL), labeled Kripke transition systems(LKTS).