Karınca kolonilerinin modellenmesi için biçimsel yöntemler ve programlama araçları

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.