Page d'accueil du CNRS Page d'accueil de Paris Diderot Page d'accueil du LIAFA
LIAFA
Laboratoire d'Informatique Algorithmique: Fondements et Applications
CNRS UMR 7089, Université Paris Diderot - Paris 7, Case 7014
75205 Paris Cedex 13 - Tél: +33(0)1.57.27.92.56 - Fax: +33(0)1.57.27.94.09
Page d'accueil de la fondation Sciences Mathématiques de Paris Page d'accueil de FRMPC
   Staff      Contact      How to get to LIAFA      Teaching      Webmail   


Version française

Research reports

  • Report number: 2003-013
  • Authors: Volker Diekert and Paul Gastin
  • Title: Local temporal logic is expressively complete for cograph dependence alphabets
  • Summary:


     Recently, local logics for Mazurkiewicz traces are of increasing interest. This is mainly due to the fact that the satisfiability problem has the same complexity as in the word case. If we focus on a purely local interpretation of formulae at vertices (or events) of a trace, then the satisfiability problem of linear temporal logics over traces turns out to be PSPACE--complete. But now the difficult problem is to obtain expressive completeness results with respect to first order logic.

    The main result of the paper shows such an expressive completeness result, if the underlying dependence alphabet is a cograph, i.e., if all traces are series parallel posets. Moreover, we show that this is the best we can expect in our setting: If the dependence alphabet is not a cograph, then we cannot express all first order properties.



  • Complete report:
    PostScript file compressed with gzip
    PostScript format
    pdf format

 
 ©  LIAFA 1995, Last updating: 2013, May webmestre[at]liafa.univ-paris-diderot.fr