Details
| Original language | English |
|---|---|
| Pages (from-to) | 1333-1352 |
| Number of pages | 20 |
| Journal | Journal of Logic and Computation |
| Volume | 27 |
| Issue number | 5 |
| Early online date | 25 Jun 2016 |
| Publication status | Published - 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
- Computer Science(all)
- Software
- Mathematics(all)
- Theoretical Computer Science
- Arts and Humanities(all)
- Arts and Humanities (miscellaneous)
- Computer Science(all)
- Hardware and Architecture
- Mathematics(all)
- Logic
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: Journal of Logic and Computation, Vol. 27, No. 5, 07.2017, p. 1333-1352.
Research output: Contribution to journal › Article › Research › peer review
}
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 -