Title Složenost modalnih logika Title (english) Complexity of modal logics Author Helena Marciuš Mentor Mladen Vuković (mentor)Committee member Mladen Vuković (predsjednik povjerenstva)Committee member Matej Mihelčić (član povjerenstva)Committee member Vedran Krčadinac (član povjerenstva)Committee member Miljenko Huzak (član povjerenstva)Granter University of Zagreb Defense date and country 2022-09-29, Croatia Scientific / art field, NATURAL SCIENCES Abstract Glavni cilj ovog rada je dokazati nekoliko rezultata o složenosti modalnih logika. Rad je podijeljen u dva poglavlja. U prvom se poglavlju bavimo sintaksom i semantikom osnovnog modalnog jezika. Definiramo pojmove alfabeta i formula, Kripkeovih okvira i modela te istinitost i valjanost modalnih formula. Zatim definiramo najmanju normalnu modalnu logiku K te neka njezina proširenja - logike K4, T, S4, S5, te S4.3T. U prvom poglavlju dajemo i osnovne pojmove i rezultate teorije modela modalne logike. Definiramo redom sljedeće pojmove: generirani podmodel, izomorfizam i ograničeni morfizam. Za svaku od upravo navedenih konstrukcija modela dokazujemo da čuva istinitost. Definiramo i svojstvo konačnih modela i okvira. Na kraju poglavlja opisujemo karakteristične klase okvira pojedinih modalnih logika. U drugom poglavlju razmatramo složenost normalnih modalnih logika koje smo definirali u prvom poglavlju. Prvo definiramo pojam polinomnog svojstva konačnih modela te pojam definabilnosti klase okvira u logici prvog reda. Ti su pojmovi ključni za dokaz NP– potpunost logike S5 te za dokaz Hemaspaandrinog teorema o NP–potpunosti modalnih logika koje proširuju S4.3T. U drugom dijelu ovog poglavlja prvo definiramo pojam stabla koji će biti važan u ostatku poglavlja. Zatim dokazujemo da logika K nema polinomno svojstvo konačnih modela. Iz tog rezultata možemo naslutiti da logika K, nije NP –potpuna modalna logika. U nastavku definiramo pojam Hintikkinog skupa i pojam skupova svjedoka. Zatim dokazujemo tvrdnje koje nam daju sintaktički kriterij za provjeru ispunjivosti formule. Prvo navodimo algoritam \({Svjedok}\), a onda opisujemo rad Turingovog stroja koji provjerava K, – ispunjivost koristeći taj algoritam. Time dokazujemo da je logika K PSPACE–složena modalna logika. Zatim definiramo pojam QBF-formule te definiramo problem odredivanja istinitosti QBF-formula, u oznaci TQBF, za koji se zna da je PSPACE–potpun. Svodenjem problema TQBF na problem ispunjivosti proizvoljne normalne modalne logike \(\Lambda\) takve da je K ⊆ \(\Lambda\) ⊆ S4 dokazujemo Ladnerov teorem koji govori da je svaka logika izmedu K i S4 PSPACE–teška. Na kraju poglavlja ukratko opisujemo složenost logika LTL i PDL. Također dajemo primjer neodlučive modalne logike Tile.
Abstract (english) The main goal of this thesis is to present some results about the complexity of modal logics. The thesis consists of two chapters. In the first chapter, we describe the syntax and semantics of the basic modal language. We define alphabet, formulas, Kripke frames and models, satisfiability, and validity. We then define smallest normal modal logic K and its extensions - K4, T, S4, S5 and S4.3. In this chapter we also present basic notions and results of the model theory of modal logic. We define the following notions: generated submodel, isomorphism and bounded morphism. We prove that each of the defined constructions preserves satisfiability. We also define a finite model and finite frame property. At the end of the first chapter, we describe characteristic frame classes of some modal logics. The second chapter is about the complexity of normal modal logics defined in the first chapter. First, we define polysize model property and frame definability by a first-order sentence. These are key notions for proving NP-completeness of S5 and for proving Hemaspaandra’s theorem about the NP–completeness of normal modal logics extending S4.3. The second part of the second chapter starts with the definition of trees as they are very useful in the rest of the chapter. Then we show that K lacks polysize model property. From this result we can assume that K is not NP–complete. Furthermore, we define Hintikka sets and witness sets and give a syntactic criterion for the satisfiability of a formula. We also present an algorithm called \({Witness}\) and describe a Turing machine that decides Ksatisfiability using Witness. This show that K has PSPACE complexity. Moreover, we define QBF-formulas and QBF-validity problem, or TQBF problem, which is a known PSPACE-complete problem. By reducing the TQBF problem to the \(\Lambda\) -satisfiability problem, for normal modal logic Λ such that K ⊆ \(\Lambda\) ⊆ S4, we prove that every normal modal logic between K and S4 is PSPACE-hard. At the end of this chapter, we mention the complexity of logics LTL and PDL. We also give an example of an undecidable modal logic called Tile.
Keywords
sintaksa osnovnog modalnog jezika
semantika osnovnog modalnog jezika
Kripkeovi okviri i modeli
normalna modalna logika K
generirani podmodel
izomorfizam
ograničeni morfizam
Hemaspaandrinov teorem
Hintikkinov skup
Turingov stroj
Ladnerov teorem
Keywords (english)
syntax of basic modal language
semantics of basic modal language
Kripke frameworks and models
normal modal logic K
generated submodel
isomorphism
bounded morphism
Hemaspaandrin theorem
Hintikkin set
Turing machine
Ladner theorem
Language croatian URN:NBN urn:nbn:hr:217:221382 Study programme Title: Computer Science and Mathematics Type of resource Text File origin Born digital Access conditions Open access Terms of use Created on 2022-10-28 12:33:48
