Büyük Dil Modeli (LLM) destekli yazılım geliştirmede, doğrulanabilir doğruluk, LLM'lerle daha büyük adımlar atmayı kolaylaştıran önemli bir temadır. Bu bağlamda, Petri ağlarının bir uzantısı olan Renkli Petri Ağları (CPN'ler) dikkat çekmektedir. Temelde yönlendirilmiş iki parçalı grafikler olan Petri ağlarında, yerler veri içermeyen jetonları barındırabilir ve geçişlerle (yan etkilerin gerçekleştiği yerler) birbirine bağlanır. Tek giriş ve çıkışa sahip Petri ağları, Sonlu Durum Makineleri ile eşdeğerdir. CPN'ler ise bu modeli genişleterek, her bir jetonun kendi verisine sahip olmasına olanak tanır. Bu özellik, CPN'lerin Rust'ın typestate deseniyle yakından eşleşmesini sağlar ve Rust'ın CPN semantiklerini kolayca uygulayabileceğini düşündürür.
CPN'ler, eşzamanlı uygulamalar yazmanın zorluğu ve derleme zamanında eşzamanlı programların resmi olarak doğrulanması potansiyeli nedeniyle özellikle ilgi çekicidir. Yüksek performanslı bir veri deposuyla birleştirildiğinde, bir CPN framework'ü, eşzamanlı uygulamaların zorlu kısımlarını (durum senkronizasyonu, çakışma tespiti, kilitlenmeyi önleme ve paylaşılan kaynaklara erişimi koordine etme) ele alabilir. Bu yetenekler, CPN'lerin iki temel özelliği olan 'guard'lar ve 'çoklu jeton tüketimi/üretimi' aracılığıyla mümkün olur. Guard'lar, bir geçişin gerçekleşmesi için doğru olması gereken boole koşulları listesidir. Çoklu jeton tüketimi/üretimi ise, bir geçişin birden fazla jeton üretmesi (çatallanma) veya birden fazla jeton gerektirmesi (birleşme) anlamına gelir, bu işlemler eşzamanlı olarak gerçekleşir.
CPN'lerin pratik bir uygulaması, kiralanmış proxy'ler ve hedef sitelerle web kazıma senaryosunda görülebilir. Sınırlı sayıda proxy'yi yönetmek, her bir hedefe aşırı istek göndermemek için kullanım oranını sınırlamak, aynı hedefe aynı anda birden fazla istek yapmaktan kaçınmak ve sorumlu bir kullanıcı olmak için alan adına çok sık istek göndermemek gibi karmaşık eşzamanlılık sorunları CPN'lerle modellenebilir. Geleneksel olarak merkezi bir veritabanı ile çözülen bu tür kaynak kiralama ve senkronizasyon problemleri, CPN semantikleriyle daha yapısal ve doğrulanabilir bir şekilde ele alınabilir.
Renkli Petri Ağları, eşzamanlı uygulamaların geliştirilmesindeki zorlukları aşarak, özellikle LLM destekli sistemlerde resmi doğrulama ve karmaşık durum yönetimini kolaylaştırma potansiyeli sunuyor.