Haarautuvan ajan temporaalilogiikan CTL mallintarkastus

Saavutettavuus-analyysi on menetelmä jolla voidaan analysoida rinnakkaisen järjestelmän dynaamista käyttäytymistä. Yksi tapa määritellä järjestelmän käyttäytymiseltä vaadittavia ominaisuuksia on käyttää haarautuvan ajan temporaalilogiikkaa CTL. Mallintarkastuksella tutkitaan, täyttääkö järjestelmän käyttäytyminen siltä vaaditun ominaisuuden. Työssä analysoidaan useita mallintarkastus algoritmejä CTL:lle. Työn päätulos on uusi mallintarkastus algoritmi, joka aikakompleksisuudeltaan vastaa parhaita aikaisemmin esitettyjä algoritmejä, ja muistivaatimuksiltaan on joko yhtä hyvä tai vähemmän muistia vaativa kuin aikaisemmin esitetyt algoritmit, riippuen tutkittavan järjestelmän rakenteesta. Algoritmi sisältää lisäksi vastaesimerkki- ja todistaja-polun etsintä ominaisuuden, joka on hyödyllinen kun järjestelmän virheellisen käytöksen syytä pyritään etsimään. Esitetty algoritmi on myös hyvin suoraviivainen toteuttaa tehokkaalla tavalla, ja työssä algoritmi on toteutettu PROD työkalu-ohjelmistoon