Informacje

Czwartki, o godz. 10:45

w sali seminaryjnej IPI PAN


Organizatorzy: Piotr Dembiński
Antoni Mazurkiewicz
Wojciech Penczek
Andrzej Tarlecki
Józef Winkowski

e-mail: Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie obsługi JavaScript.

Archiwum Seminarium Zakładu
Teoretycznych Podstaw Informatyki

2010/2011

2009/2010

2008/2009

2007/2008

2006/2007

2005/2006

2004/2005

2003/2004

2002/2003

2001/2002

godz. 14:00 (czwartek) Agnieszka Zbrzezny (Instytut Matematyki i Informatyki, Akademia im. Jana Długosza w Częstochowie)

Metoda ograniczonej weryfikacji modelowej bazująca na testerach SMT dla wagowych systemów interpretowanych i własności wyrażanych w WECTLK

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.