UPPAAL TIGA este o extensie a UPPAAL [BDL04] și pune în aplicare prima eficient algoritm on-the-fly pentru rezolvarea jocuri bazate pe automate de joc temporizat cu privire la proprietăți de accesibilitate și de siguranță.
Deși jocuri temporizate pentru mult timp au fost cunoscute a fi decidabile nu a fost până acum o lipsă de algoritmi eficienți și cu adevărat pe-the-fly pentru analiza lor.
UPPAAL TIGA oferă o interfață grafică ușor de utilizat cu serverul sa corespunzătoare, și un verificator de linie de comandă.
Algoritmul ne propunem [CDFLL05] este o extensie simbolică a algoritmului on-the-fly sugerat de Liu & Smolka [LS98] pentru liniar-time model de verificare a sistemelor finite de stat. Fiind pe-the-fly, algoritmul simbolic poate rezilia timp înainte de a fi explorat întregul spațiul stat.
De asemenea etapele individuale ale algoritmului sunt realizate în mod eficient prin utilizarea așa-numitelor zone ca structura de date de bază. Instrumentul nostru implementează diverse optimizări ale algoritmului simbolic de bază, precum și metode de obținere a unor strategii castigatoare timp optim (pentru jocurile de accesibilitate).
Ce este nou în această versiune:
Comentariile nu a fost găsit