Johdatus aikalogiikoihin
Lindstedt, Tinja (2023)
2023
Matematiikan maisteriohjelma - Master´s Programme in Mathematics
Informaatioteknologian ja viestinnän tiedekunta - Faculty of Information Technology and Communication Sciences
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Hyväksymispäivämäärä
2023-05-08
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:tuni-202304264626
https://urn.fi/URN:NBN:fi:tuni-202304264626
Tiivistelmä
Tutkielma toimii johdantona aikalogiikoihin, joiden avulla voidaan tarkastella erilaisten tapahtumien totuutta eri ajankohtina. Tässä tutkielmassa esitetään olennaisimmat käsitteet ja määritelmät liittyen modaalilogiikkaan, lineaariseen aikalogiikkaan ja haarautuviin aikalogiikoihin. Tutkielmassa on paljon selittäviä välihuomioita ja runsaasti esimerkkejä, joiden avulla tekstiä on helppo seurata. Lukijalta odotetaankin vain lauselogiikan perusteiden tuntemusta, sillä kaikki tutkielmassa käytettävät käsitteet on pyritty erikseen määrittelemään.
Tutkielman alussa esitetään ensin aikakehyksen ja sitten aikamallin määritelmät. Sen jälkeen käsitellään modaalilogiikkaa (”basic modal logic”, BML), jossa olevat operaattorit näkevät vain seuraavan ajanhetken. Seuraavaksi tarkastellaan lineaarista aikalogiikkaa (”linear temporal logic”, LTL), jossa oletetaan, että aika kulkee lineaarisesti, eikä se voi esimerkiksi haarautua tai pysähtyä. Tätä varten esitetään uusia operaattoreita, joilla voidaan viitata esimerkiksi siihen, että jokin asia on tosi joskus tai aina tulevaisuudessa. Myöhemmin tarkastellaan tilannetta, jossa aika voi haarautua monille eri poluille ja tätä varten esitetään kolme haarautuvaa aikalogiikkaa: saavutettavuuslogiikka (”temporal logic of reachability”, TLR), haarautuva (perus-) aikalogiikka (”computation tree logic”, CTL) ja haarautuva laajennettu aikalogiikka (”full computation tree logic”, CTL*). Erilaisten aikalogiikoiden esittelyn lisäksi tutkitaan esimerkkien kautta millaisia aikamallien ominaisuuksia näiden logiikoiden avulla voidaan ilmaista.
Tutkielman alussa esitetään ensin aikakehyksen ja sitten aikamallin määritelmät. Sen jälkeen käsitellään modaalilogiikkaa (”basic modal logic”, BML), jossa olevat operaattorit näkevät vain seuraavan ajanhetken. Seuraavaksi tarkastellaan lineaarista aikalogiikkaa (”linear temporal logic”, LTL), jossa oletetaan, että aika kulkee lineaarisesti, eikä se voi esimerkiksi haarautua tai pysähtyä. Tätä varten esitetään uusia operaattoreita, joilla voidaan viitata esimerkiksi siihen, että jokin asia on tosi joskus tai aina tulevaisuudessa. Myöhemmin tarkastellaan tilannetta, jossa aika voi haarautua monille eri poluille ja tätä varten esitetään kolme haarautuvaa aikalogiikkaa: saavutettavuuslogiikka (”temporal logic of reachability”, TLR), haarautuva (perus-) aikalogiikka (”computation tree logic”, CTL) ja haarautuva laajennettu aikalogiikka (”full computation tree logic”, CTL*). Erilaisten aikalogiikoiden esittelyn lisäksi tutkitaan esimerkkien kautta millaisia aikamallien ominaisuuksia näiden logiikoiden avulla voidaan ilmaista.