Relation-Changing Modal Logics
| Title | Relation-Changing Modal Logics |
| Publication Type | Thesis |
| Year of Publication | 2014 |
| Authors | Fervari, R |
| Academic Department | Facultad de Matemática, Astronomía y Física, Universidad Nacional de Córdoba |
| Date Published | March |
| University | Facultad de Matemática Astronomía y Física, Universidad Nacional de Córdoba |
| City | Córdoba, Argentina |
| Thesis Type | phd |
| Keywords | bisimu- lations, complexity, decidability, dynamic epistemic logics, dynamic operators, expressive power, Modal logics, relation-changing operators |
| Abstract | In this thesis we study dynamic modal operators that can change the model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to swap, delete or add pairs of related elements of the domain. We call the resulting logics Relation-Changing Modal Logics. We study local version of the operators (performing modifications from the evaluation point) and global version (changing arbitrarily edges in the model). We investigate several properties of the given languages, from an abstract point of view. First, we introduce the formal semantics of the model modifiers, afterwards we introduce a notion of bisimulation. Bisimulations are an important tool to investigate the expressive power of the languages introduced in this thesis. We show that all the languages are incomparable among them in terms of expressive power (except for the two versions of swap, which we conjecture are also incomparable). We continue by investigating the computational behaviour of this kind of operators. First, we prove that the satisfiability problem for some of the relation-changing modal logics we investigate is undecidable. Then, we prove that the model checking problem is PSpace-complete for the six logics. Finally, we investigate model checking fixing the model and fixing the formula (problems known as formula and program complexity, respectively). We show that it is possible to define complete but non-terminating methods to check satisfiability. We introduce tableau methods for relation-changing modal logics and we prove that all these methods are sound and complete, and we show some applications. In the last part of the thesis, we discuss a concrete context in which we can apply relation-changing modal logics: Dynamic Epistemic Logics (DEL). We motivate the use of the kind of logics that we investigate in this new framework, and we introduce some examples of DEL. Finally, we define a new relation-changing modal logic that embeds DEL and we investigate its computational behaviour. |
| Original Publication | Lógicas Modales con Operadores de Cambio de Accesibilidad |
PDF (Full text):
Work Package:
WP2
