Modal independence logic

Research output: Contribution to journalArticleResearchpeer review

Authors

External Research Organisations

  • University of Helsinki
  • Kiel University
View graph of relations

Details

Original languageEnglish
Pages (from-to)1333-1352
Number of pages20
JournalJournal of Logic and Computation
Volume27
Issue number5
Early online date25 Jun 2016
Publication statusPublished - Jul 2017

Abstract

This article introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of Väänänen's modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms.We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL.We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.

Keywords

    Computational complexity, Dependence logic, Expressivity over finite models, Independence, Team semantics

ASJC Scopus subject areas

Cite this

Modal independence logic. / Kontinen, Juha; Müller, Julian Steffen; Schnoor, Henning et al.
In: Journal of Logic and Computation, Vol. 27, No. 5, 07.2017, p. 1333-1352.

Research output: Contribution to journalArticleResearchpeer review

Kontinen, J, Müller, JS, Schnoor, H & Vollmer, H 2017, 'Modal independence logic', Journal of Logic and Computation, vol. 27, no. 5, pp. 1333-1352. https://doi.org/10.1093/logcom/exw019
Kontinen, J., Müller, J. S., Schnoor, H., & Vollmer, H. (2017). Modal independence logic. Journal of Logic and Computation, 27(5), 1333-1352. https://doi.org/10.1093/logcom/exw019
Kontinen J, Müller JS, Schnoor H, Vollmer H. Modal independence logic. Journal of Logic and Computation. 2017 Jul;27(5):1333-1352. Epub 2016 Jun 25. doi: 10.1093/logcom/exw019
Kontinen, Juha ; Müller, Julian Steffen ; Schnoor, Henning et al. / Modal independence logic. In: Journal of Logic and Computation. 2017 ; Vol. 27, No. 5. pp. 1333-1352.
Download
@article{5d1e8bf7a7d846bf898e67b80eb824dd,
title = "Modal independence logic",
abstract = "This article introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of V{\"a}{\"a}n{\"a}nen's modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms.We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL.We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.",
keywords = "Computational complexity, Dependence logic, Expressivity over finite models, Independence, Team semantics",
author = "Juha Kontinen and M{\"u}ller, {Julian Steffen} and Henning Schnoor and Heribert Vollmer",
note = "Funding Information: J.K. was supported by the Academy of Finland grants (292767) and (275241). Publisher Copyright: {\textcopyright} The Author, 2016. Published by Oxford University Press. All rights reserved. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.",
year = "2017",
month = jul,
doi = "10.1093/logcom/exw019",
language = "English",
volume = "27",
pages = "1333--1352",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "5",

}

Download

TY - JOUR

T1 - Modal independence logic

AU - Kontinen, Juha

AU - Müller, Julian Steffen

AU - Schnoor, Henning

AU - Vollmer, Heribert

N1 - Funding Information: J.K. was supported by the Academy of Finland grants (292767) and (275241). Publisher Copyright: © The Author, 2016. Published by Oxford University Press. All rights reserved. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.

PY - 2017/7

Y1 - 2017/7

N2 - This article introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of Väänänen's modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms.We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL.We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.

AB - This article introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of Väänänen's modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms.We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL.We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.

KW - Computational complexity

KW - Dependence logic

KW - Expressivity over finite models

KW - Independence

KW - Team semantics

UR - http://www.scopus.com/inward/record.url?scp=85029652167&partnerID=8YFLogxK

U2 - 10.1093/logcom/exw019

DO - 10.1093/logcom/exw019

M3 - Article

AN - SCOPUS:85029652167

VL - 27

SP - 1333

EP - 1352

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 5

ER -

By the same author(s)