Aikalogiikka

Aikalogiikka, eli temporaalilogiikka, on logiikan ala, joka tutkii ajassa tapahtuvien ilmiöiden totuusarvojen suhteita ja mahdollistaa ajallisten ominaisuuksien ilmaisun. Se laajentaa perinteistä logiikkaa lisäämällä ajallisia operaatioita, joiden avulla voidaan kuvata milloin jokin lause on tosi nykyhetkellä sekä menneessä ja tulevaisuudessa. Yleisimpiä suuntauksia ovat lineaarinen aikalogiikka (LTL), joka tarkastelee yhtä lineaarista ajan kulkua, ja haarautuva aikalogiikka (CTL), joka mallintaa useita mahdollisia ajanhaaroja puumaisessa rakenteessa.

Semantiikassa LTL:n totuusarvot määritellään lineaarisella aikajonolla, ja sen keskeisiä operaatioita ovat Next (X), Finally (F), Globally (G) sekä Until (U). CTL:ssa totuus määritellään puumaisessa aikamallissa polkujen kautta, joissa käytetään polkutunnisteita A (kaikki polut) ja E (on olemassa polku). Näitä logiikkoja sovelletaan muun muassa ohjelmistojen ja järjestelmien mallintamiseen sekä varmistamiseen (model checking). Real-time -järjestelmissä on myös kehitetty määräaikaisia laajennuksia, kuten MTL, joissa aikavaatimukset ovat kiinteästi mukana.

Historia: Aikalogiikka sai alkunsa filosofi Arthur Priorin 1960-luvulla. Tietotekniikassa merkittäviä virstanpylväitä olivat Pnuelin kehittämä lineaarinen aikalogiikka (LTL) 1977 sekä Emersonin ja Clarke'n kehittämä haarautuva aikalogiikka (CTL). Nykyään aikalogiikka on keskeinen osa ohjelmistotieteen työkalupäätä, ja sitä sovelletaan muun muassa ohjelmistojen ja järjestelmien oikeellisuuden todentamiseen sekä reaaliaikaisiin järjestelmiin liittyviin suunnittelukysymyksiin.