Teknillinen Korkeakoulu
Tietotekniikan osasto
Tietojenkäsittelyteorian laboratorio
T-79.146 Logiikka tietotekniikassa:
erityiskysymyksiä I (2 ov)
Kevät 2002
Opintojakson tavoitteena on perehtyä
modaalilogiikkojen malli- ja todistusteoriaan,
todistusmenetelmiin ja laskennallisiin ominaisuuksiin sekä
tämäntyyppisten logiikkojen ajankohtaisiin sovellutuksiin
tietotekniikassa.
Tämän kevään teemana on
temporaalilogiikan sovellutukset rinnakkaisissa ja hajautetuissa
järjestelmissä.
Temporaalilogiikka on noussut keskeiseksi lähestymistavaksi
rinnakkaisten ja hajautettujen järjestelmien, kuten tietoliikenne- ja
ohjausjärjestelmien, kehitystyössä. Se tarjoaa käyttökelpoisen
menetelmän spesifioida ko. järjestelmiä ja sen pohjalta on
kehitetty tehokkaita automaattisia työkaluja järjestelmien
oikeellisuuden varmentamiseen. Tällaisten formaalien menetelmien käyttö
lisääntyy teollisuudessa voimakkaasti:
The use of formal verification tools is well established and
becoming more so. Simulation- and emulation-based methodologies aren't
sufficient to guarantee correctness with today's complex chips. (Carl
Pixley, Motorola Inc. in IEEE Spectrum, Jan 1997, p. 61)
Opintojaksolla tutustutaan keskeisimpien sovellutuksissa käytettävien
temporaalilogiikkojen (CTL, LTL) semanttiseen pohjaan,
ilmaisuvoimaan, laskennalliseen vaativuuteen ja käytettävien
automaattisten työkalujen (mallintarkistimet, teoreemantodistimet)
toteutusperiaatteisiin sekä sovellutuksiin.
Opintojakso soveltuu kaikille logiikasta ja formaaleista menetelmistä
kiinnostuneille sekä jatko-opiskelijoille mukaanlukien
HeCSEn (Helsinki Graduate School in Computer Science and
Engineering) opiskelijat. Kurssi koostuu luennoista,
laskuharjoituksista ja kotitehtävistä. Kurssin suorittaminen
edellyttää kotitehtävien ratkaisemista ja tentin suorittamista.
- Vastaava opettaja:
Prof. Ilkka Niemelä
puh. 451 3290, e-mail: Ilkka.Niemela@hut.fi,
URL: http://www.tcs.hut.fi/~ini/
- Luennot: Keskiviikoisin klo 14-16, sali TB353.
Ensimmäinen tilaisuus on 16.1.2002.
- Assistentti: DI Heikki Tauriainen, puh. 451 3263, e-mail:
Heikki.Tauriainen@hut.fi,
URL: http://www.tcs.hut.fi/~htauriai/
- Laskuharjoitukset:
Perjantaisin klo 10-11, sali TB353.
- Kirjallisuus:
M. Fitting, Basic Modal Logic, Handbook of Logic in
Artificial Intelligence and Logic Programming, Volume 1, Logical
Foundations, 1993.
E. Clarke and O. Grumberg and D. Peled,
Model Checking, The MIT Press, 1999. (Chapters 1-4)
E.A. Emerson, Automated Temporal Reasoning about Reactive Systems,
Logics for Concurrency, F. Moller and G. Birtwistle (Eds.),
Springer-Verlag, 1996, LNCS 1043, pp. 39-99.
- Kurssin kotisivu: http://www.tcs.hut.fi/Teaching/T-79.146/
- Uutisryhmä: opinnot.tik.logiikka
- Tentti: 8.5.2002, 13-16, sali T1
- Esitiedot: T-79.144 Logiikka tietotekniikassa:
perusteet tai vastaavat tiedot.