<!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>Reasoning and Planning for LTLf /LDLf goals</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Giuseppe De Giacomo</string-name>
          <email>degiacomo@dis.uniroma1.it</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Sapienza University of Rome</institution>
          ,
          <addr-line>Rome</addr-line>
          ,
          <country country="IT">Italy</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>This talk will be about reasoning and planning for goals expressed over nite traces, instead of states. We will look at goals speci ed in two speci c logics (i) LTLf , i.e., LTL interpreted over nite traces, which has the expressive power of FOL and star-free regular expressions over nite stings; and (ii) LDLf , i.e., Linear-time Dynamic Logic on nite traces, which has the expressive power of MSO and full regular expressions. We will review the main results and algorithmic techniques to handle reasoning, planning in deterministic domains, and especially planning in nondeterministic domains. We will also brie y consider stochastic domains. Moreover, we will draw connections with veri cation and reactive synthesis. The main catch is that working with these logics can be based on manipulation of regular automata on nite strings, for which well-established algorithms are available.</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>