Propositionaalinen dynaaminen logiikka

Abstract

Tämän pro gardu -tutkielman aiheena on propositionaalinen dynaaminen logiikka (PDL). PDL on modaalilogiikan laajennus, joka tarkastelee tietokoneohjelmia. Luvussa 2 annetaan propositio- ja modaalilogiikkaa koskevia määritelmiä, jotka tukevat varsinaista aihetta. Luvussa 3 käsitellään PDL:n peruskäsitteitä. PDL:n ohjelmat ilmaistaan kaksipaikkaisina relaatioina tilojen välillä ja ne tulkitaan siirroiksi, jotka muuttavat tilan toiseksi. Ohjelmia muodostetaan muun muassa operaatioiden valinnan ∪, komposition ; ja iteraation ∗ avulla. PDL:ään liitetään ääretön määrä mahdollisuusoperaattoreita modaalilogiikan yhden mahdollisuusoperaattorin sijaan. Jokaiseen ohjelmaan liitetään oma operaattorinsa hi. PDL:ssä joka ohjelmalla on oma vastaava relaationsa, joita voidaan muodostaa annettujen relaatioiden avulla. PDL-semantiikka on modaalilogiikan semantiikan kaltaista. Kaavojen totuutta tarkastellaan malleissa. PDL-malli on tilojen joukon W, relaation R ja valuaation V muodostama kolmikko. Kaava voi olla tosi jokaisessa PDLmallissa, jolloin kyseessä oleva kaava on PDL-validi. Luvun 3 lopussa esitetään PDL:n aksiomatisointi. Viimeisessä luvussa 4 määritellään bisimulaation käsite.

Kahtena päälähdeteoksena toimivat kirjat Modal logic (Blackburn, de Rijke, Venema) ja Dynamic logic (Harel, Kozen, Tiuryn). Lähteinä on käytetty myös kirjaa Johdatus modaalilogiikkaan (Rantala, Virtanen), Stanfordencyclopedia of philosophy -verkkosivuston julkaisua Propositional dynamic logic ja verkkojulkaisuja Game constructions that are safe for bisimulation (Pauly) ja On definability in multimodal logics (Halpern, Samet, Segev).