Seminar of the Department of Theoretical Foundations of Computer Science:


Information:

Thursdays, 10:45 am
Place of the seminar: ICS PAS seminar room

The organizers:

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

e-mail: Wojciech.Penczek@ipipan.waw.pl 

 Archives of Seminar of the Department of Theoretical Foundations of Computer Science
2010/2011 2005/2006
2009/2010 2004/2005
2008/2009 2003/2004
2007/2008 2002/2003
2006/2007 2001/2002

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

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.

ATTENTION! This site uses cookies and similar technologies.

If you do not change your browser settings, you automatically agree to this.

I understand