Teknillinen korkeakoulu, 
     Tietojenkäsittelyteorian laboratorio

T-79.5101 Laskennallisen logiikan jatkokurssi (4 op) L

Kevät 2007

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.

  • Kirjallisuus:
    M. Fitting: Basic Modal Logic, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1, Logical Foundations, 1993.
    E. Clarke, O. Grumberg, and D. Peled: Model Checking, The MIT Press, 1999. (Chapters 1-4)
    E.A. Emerson: Automated Temporal Reasoning about Reactive Systems, in F. Moller and G. Birtwistle (Eds.), Logics for Concurrency, Springer-Verlag, 1996, LNCS 1043, pp. 39-99.
  • Luennot: keskiviikkoisin klo 10-12, sali TB353; kurssi alkaa 17.1.2007.
  • Laskuharjoitukset: maanantaisin klo 12-13, sali TB353.
  • Vastaava opettaja: Prof. Ilkka Niemelä, sähköposti Ilkka.Niemelatkk.fi, kotisivu http://www.tcs.hut.fi/~ini/
  • Assistentti: DI Matti Järvisalo, sähköposti mjjtcs.hut.fi, kotisivu http://www.tcs.hut.fi/~mjj/
  • Esitiedot: T-79.3001/144 Logiikka tietotekniikassa: perusteet tai vastaavat tiedot
  • Kurssin kotisivu: http://www.tcs.hut.fi/Studies/T-79.5101/
  • Uutisryhmä: opinnot.tik.logiikka