Tietojenkäsittelytieteen laitos

Dosenttikoeluento

Päivä	Perjantai, 19. joulukuuta 1997
Aika	klo 11
Paikka	Sali A414 (Teollisuuskatu 23, 4. krs)

---

Tiivistelmä

Reaktiivisten, ei-terminoivien ohjelmien spesifioitiin ja verifiointiin käytettävät menetelmät perustuvat usein ohjelman generoimien äärettömien tapahtumajonojen kielen kuvaamiseen. Kiintopistelogiikat ja automaatit ovat kaksi laajalti tutkittua formalismia, joiden avulla voidaan kuvata tällaisia äärettömien merkkijonojen kieliä.

Kertaan luennolla yleisimmät tavat laajentaa tavallisten äärellisillä merkkijonoilla toimivien automaattien teoria äärettömille jonoille, esittelen lineaarisen kiintopistelogiikan perusteet ja tarkastelen tämän jälkeen näiden kahden formalismin suhdetta. Keskeisenä teemana on osoittaa, että näennäisistä eroista huolimatta automaatit ja kiintopistelogiikan kaavat voidaan oleellisesti samaistaa ja nähdä molemmat formalismit saman yleisen käsitteen eri ilmentyminä.