<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Verification of Temporal Properties in Communicating Datalog Programs</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Diego Calvanese</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Free University of Bozen-Bolzano, Italy Umeå University</institution>
          ,
          <country country="SE">Sweden</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>Logic-based languages, such as Datalog and Answer Set Programming, have been recently put forward as a data-centric model to efectively specify and implement network services and protocols, seeing them as dynamic systems of distributed computational nodes. In such systems, which we call Communicating Datalog Programs (CDPs), each node evolves an internal database, exchanges data with other nodes of the network via channels, and may incorporate fresh data from the external world. A rigorous, comprehensive characterization of the decidability and complexity of verification of temporal properties in CDPs is still missing. In this talk we analyze the diferent assumptions characterizing the problem space, and then discuss several diferent variants of the problem. In particular, for the significant case where the number of nodes in the network is fixed, we delineate the decidability frontier of verification and provide tight complexity bounds. The presented results are based on joint work with C. Aiswarya, Francesco Di Cosmo, Jorge Lobo, and Marco Montali.</p>
      </abstract>
      <kwd-group>
        <kwd>eol&gt;Formal Verification</kwd>
        <kwd>Data-aware Processes</kwd>
        <kwd>Communicating Datalog Programs</kwd>
        <kwd>Distributed Computation</kwd>
        <kwd>Temporal Properties</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>