Tez No	İndirme	Tez Künye	Durumu
202701		Formal methods and programming tools for modeling ant colonies / Karınca kolonilerinin modellenmesi için biçimsel yöntemler ve programlama araçları Yazar:EMİNE EKİN Danışman: PROF. DR. TATYANA YAKHNO Yer Bilgisi: Dokuz Eylül Üniversitesi / Fen Bilimleri Enstitüsü / Bilgisayar Mühendisliği Ana Bilim Dalı Konu:Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control Dizin:	Onaylandı Doktora İngilizce 2006 196 s.
Eniyileştime problemlerinin çözümünde doğadan esinlenerek geliştirilenalgoritmalar giderek artan bir yere sahiptir. Karınca kolonisi eniyileştirmealgoritmaları da doğa kaynaklı algoritmaların yakın dönemde geliştirilenörneklerinden biridir. Karınca kolonisi algoritmaları, karıncaların yiyecek aramasürecindeki olası bir çok yol arasından en kısa olanı bulabilme yeteneği baz alınarakgeliştirilmiştir. Bu yetenek hareket eden karıncaların yeryüzüne kimyasal bir maddebırakmaları, ve takipçilerinin de bu maddeyi algılayarak daha yoğun madde olanyolları tercih etmeleri olarak açıklanabilir. Birçok biyolojik sistemde de görülen budavranış sosyal davranış olarak isimlendirilmektedir.Karınca kolonilerinde görülen sosyal davranış iki ayrı inceleme alanı ile karşımızaçıkar. Birincisi, bu davranışın eniyiliştirme problemlerinin çözümündekullanılabilecek algoritmalar tarafından taklit edilmesi, diğeri ise koloni içindekibireylerin davranışları ile bunun koloni üzerindeki etkilerinin araştırılmasına ve dahaiyi anlaşılmasına yönelik olarak geliştirilen biçimsel modelleme yöntemleri. Biçimselmodellemenin avantajı uygun bir doğrulama yöntemi ile birleştirildiğinde yalnızcasosyal davranışın değil, karınca kolonilerinin birçok özelliklerininaraştırılabilmesidir.Bu tezde, her iki alanda da çalışmalar yapılmıştır. Karınca kolonisi en iyileştirmealgoritmaları kullanılarak gerçek hayattan, ve yöneylem araştırması alanından alınanproblemler çözülmüş benzer eniyiliştirme algoritmaları ile karşılaştırmalarıverilmiştir. Ayrıca gezgin satıcı problemi için geliştirilen uygulama ile algoritmanıntemel özelliklerinin, parametrelerin birbirlerilerine olan etkilerinin anlaşılmasısağlanmıştır. Ancak, asıl içerik biçimsel modelleme, doğrulama, ve ikisini birleştirenbir modelleme aracının geliştirilmesi üzerine yoğunlaşmıştır.Birçok biçimsel modelleme dili arasından olasılıksal olarak durumlar arası geçişeolanak sağlayan bir işlem cebri olan Bağlantılı Çalışan Sistemler için AğırlıklıEşlemeli Hesap ?Weighted Synchronized Calculus of Communicating Systems?(WSCCS) seçilmiştir. Ancak, modelleme, doğrulama ile birleştirilmediği süreceincelemesi yapılan sistem hakkında herhangi bir yargıda bulunmamıza olanaksağlamaz. Doğrulama işlemi, oluşturulan soyut modelin sistem tanımı ilekarşılaştırılarak teyit edilmesidir. Ayrıca, model üzerinde yapılabilen bazısorgulamalar sayesinde sistemin özellikleri de incelenebilir. Model denetimi birdoğrulama yöntemi olup verilen bir özelliği sistemin sağlayıp sağlamadığınınaraştırılmasıdır.Doğrulama yöntemi olarak seçilen model denetimi yaklaşımı ancak zamana bağlımantık ?temporal logics? ile yapılabildiği için, olasılıksal hesap ağacı mantığı?probabilistic Computational Tree Logic? (pCTL), bu tezde incelenen, ve karıncakolonilerinin toplu davranışlarını da kapsayabilmesi için genişletilen diğer birbiçimsel yöntemdir.Son olarak WSCCS modelleme ile model doğrulama işleminin birleştirilmesi içingeliştirilen modellerin ilgili geçişlerle birlikte ayrık durum uzayına dönüştürülmesizorunludur. ?Labeled Kripke Transition Systems? ayrık durum uzayı biçimselliğiolarak tanıtılmış, ancak durum geçişlerinde olasılık ve eylemlerin temsil edilebilmesiiçin tanımı genişletilmiştir.Bu tezde elde edilen başlıca kazanımlar; karınca kolonisi algoritmalarınıneniyileştirme problemlerinin çözümünde kullanılması için geliştirilen uygulamalar;karınca kolonilerinin modellemesinde kullanılmak üzere WSCCS dilinin detaylıincelenmesi; CTL zamana bağlı mantığı ve LKTS ayrık durum uzayıbiçimselliklerinin WSCCS dilinin temel özelliği olan olasılığa bağlı faaliyetleridesteklemek üzere genişletilmesi; modeller üzerinde yine olasılığa ve eyleme bağlısorgulamalar yapabilmek üzere bir model denetleme şemasının tasarlanması; ve tümbu işlemleri otomatik olarak yapabilmek için bir yazılım aracının geliştirilmesiolarak sayılabilir.Anahtar Kelimeler: Karınca Kolonisi Optimizasyonu, sosyal davranış, BağlantılıÇalışan Sistemler için Ağırlıklı Eşlemeli Hesap, model denetleme, olasılıksalhesaplama ağacı mantığı, etiketli Kripke geçiş sistemleri.
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).