Public announcement logic with distributed knowledge: expressivity, completeness and complexity.

While dynamic epistemic logics with common knowledge have been extensively studied, dynamic epistemic logics with distributed knowledge have so far received far less attention. In this paper we study extensions of public announcement logic ( $$\mathcal{PAL }$$) with distributed knowledge, in particu...

Descripción completa

Detalles Bibliográficos
Publicado en:Synthese Vol. 190; pp. 135 - 163
Autores principales: Wáng, Yì, Ågotnes, Thomas
Formato: Artículo
Publicado: Springer Nature Dec2013 Supplement
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=93871262&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 93871262
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00397857
        4LI
      jtl: Synthese
      issn: 00397857
      maglogo: N
    pubinfo:
      dt: Dec2013 Supplement
      vid: 190
      pid: 237
      pub: Springer Nature
    artinfo:
      ui:
        93871262
        10.1007/s11229-012-0243-3
      ppf: 135
      ppct: 28
      formats:
        fmt:
          @attributes:
            type: P
            size: 580KB
      tig:
        atl: Public announcement logic with distributed knowledge: expressivity, completeness and complexity.
      aug:
        au:
          Wáng, Yì
          Ågotnes, Thomas
        affil:
          Department of Computing, Mathematics and Physics, Bergen University College, Bergen Norway
          Department of Information Science and Media Studies, University of Bergen, Bergen Norway
      su:
        Completeness theorem
        Epistemic logic
        Computational complexity
        Mathematical logic
        Proof theory
        Bisimulation
      sug:
        subj:
          Completeness theorem
          Epistemic logic
          Computational complexity
          Mathematical logic
          Proof theory
          Bisimulation
      keyword:
        Completeness
        Decidability
        Distributed knowledge
        Expressivity
        Folding
        Public announcement logic
        Trans-bisimulation
        Unravelling
      ab: While dynamic epistemic logics with common knowledge have been extensively studied, dynamic epistemic logics with distributed knowledge have so far received far less attention. In this paper we study extensions of public announcement logic ( $$\mathcal{PAL }$$) with distributed knowledge, in particular their expressivity, axiomatisations and complexity. $$\mathcal{PAL }$$ extended only with distributed knowledge is not more expressive than standard epistemic logic with distributed knowledge. Our focus is therefore on $$\mathcal{PACD }$$, the result of adding both common and distributed knowledge to $$\mathcal{PAL }$$, which is more expressive than each of its component logics. We introduce an axiomatisation of $$\mathcal{PACD }$$, which is not surprising: it is the combination of well-known axioms. The completeness proof, however, is not trivial, and requires novel combinations and extensions of techniques for dealing with $$S5$$ knowledge, distributed knowledge, common knowledge and public announcements at the same time. We furthermore show that $$\mathcal{PACD }$$ is decidable, more precisely that it is $$\textsc {exptime}$$-complete. This result also carries over to $$\mathcal{S 5\mathcal CD }$$ with common and distributed knowledge operators for all coalitions (and not only the grand coalition). Finally, we propose a notion of a trans-bisimulation to generalise certain results and give deeper insight into the proofs.
      pubtype: Academic Journal
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      custom: Synthese is a copyright of Springer, 2013. All Rights Reserved.
      item: Synthese
      holder: Springer Nature
      dt:
        @attributes:
          year: 2013
    holdings:
      @attributes:
        islocal: N