W referacie zostanie przedstawiona metoda ograniczonej weryfikacji modelowej bazująca na testerach SMT (ang. Satisfiability Modulo Theories) dla systemów wieloagentowych modelowanych za pomocą wagowych systemów interpretowanych i własności wyrażanych w egzystencjalnym fragmencie wagowego CTLK (ang. Computation Tree Logic with Knowledge). Weryfikacja modelowa jest automatyczną metodą weryfikacji stosowaną dla wielu systemów współbieżnych jak np. systemy czasu rzeczywistego, systemy wieloagentowe, układy cyfrowe, systemy rozproszone, protokoły komunikacyjne, protokoły kryptograficzne i wiele innych. Ograniczona weryfikacja modelowa jest jedną z metod symbolicznej weryfikacji modelowej. Wykorzystuje ona redukcję problemu prawdziwości formuł temporalnych w danym systemie do problemu SAT (ang. Boolean Satisfiability Problem) lub SMT.

Problem SMT jest uogólnieniem problemu SAT, w którym zmienne Boolowskie są zastępowane przez predykaty z różnych teorii takich jak arytmetyka liniowa czy arytmetyka liczb całkowitych. SMT w porównaniu do SAT pozwala na wyrażenie wielu problemów w intuicyjny sposób, poprzez użycie bezkwantyfikatorowych formuł pierwszego rzędu, których spełnialność jest sprawdzana z dokładnością do teorii.

Systemy interpretowane należą do najpopularniejszych metod modelowania systemów wieloagentowych, jednakże nie uwzględniają kosztów akcji wykonywanych przez agentów. W tym celu zostały zaprojektowane wagowe systemy interpretowane (WIS). W modelu dla WIS każda tranzycja jest etykietowana nie tylko przez wspólną akcję, ale też przez nieujemną wartość całkowitą, która reprezentuje koszt wykonania akcji przez agenta.

Do zaimplementowania metody został użyty język C++ oraz SMT-tester Z3. Do przeprowadzenia badań eksperymentalnych zostały wykorzystane dwa systemy: wagowy generyczny paradygmat przetwarzania potokowego oraz wagowy protokół transmisji bitu. W referacie zostanie również przedstawione porównanie nowej metody bazującej na SMT z metodą wykorzystującą SAT. Wyniki eksperymentalne wykazały, że obie metody się uzupełniają: metoda ograniczonej weryfikacji modelowej bazująca na SMT jest szybsza dla jednego systemu, a metoda bazująca na SAT jest szybsza dla drugiego systemu. Jest to interesujący wynik, który pokazuje, że wybór metody ograniczonej weryfikacji modelowej powinien zależeć od rozważanego systemu.