UPPAAL TIGA er en forlengelse av UPPAAL [BDL04] og det implementerer den første effektiv on-the-fly algoritme for å løse spill basert på tidsbestemt spill automater med hensyn til reachability og sikkerhetsegenskaper.
Selv om tidsbestemt spill for lenge har vært kjent for å være decidable det har til nå vært en mangel på effektive og virkelig on-the-fly algoritmer for sin analyse.
UPPAAL TIGA gir et brukervennlig grafisk grensesnitt med den tilsvarende server, og en kommandolinje kontrolløren.
Algoritmen vi foreslår [CDFLL05] er en symbolsk forlengelse av on-the-fly algoritmen foreslått av Liu & Smolka [LS98] for lineær-time modell-kontroll av finite-state systemer. Å være on-the-fly, kan den symbolske algoritmen avslutte lenge før du har utforsket hele state-plass.
Også de enkelte trinn i algoritmen utføres effektivt ved anvendelse av såkalte soner som den underliggende datastrukturen. Vårt verktøy implementerer ulike optimaliseringer av den grunnleggende symbolske algoritmen, samt metoder for å innhente tids optimal vinnende strategier (for reachability spill).
Hva er nytt i denne versjonen:
Kommentarer ikke funnet