Compact Labelings For Efficient First-Order Model-Checking
| hal.structure.identifier | Laboratoire Bordelais de Recherche en Informatique [LaBRI] | |
| hal.structure.identifier | Institut universitaire de France [IUF] | |
| dc.contributor.author | COURCELLE, Bruno | |
| hal.structure.identifier | Laboratoire Bordelais de Recherche en Informatique [LaBRI] | |
| hal.structure.identifier | Algorithmics for computationally intensive applications over wide scale distributed platforms [CEPAGE] | |
| dc.contributor.author | GAVOILLE, Cyril | |
| hal.structure.identifier | Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes [LIMOS] | |
| dc.contributor.author | KANTÉ, Mamadou Moustapha | |
| dc.date.accessioned | 2024-04-15T09:53:32Z | |
| dc.date.available | 2024-04-15T09:53:32Z | |
| dc.date.created | 2008 | |
| dc.date.issued | 2011-01-07 | |
| dc.identifier.issn | 1382-6905 | |
| dc.identifier.uri | https://oskar-bordeaux.fr/handle/20.500.12278/198612 | |
| dc.description.abstractEn | We consider graph properties that can be checked from labels, i.e., bit sequences, of logarithmic length attached to vertices. We prove that there exists such a labeling for checking a first-order formula with free set variables in the graphs of every class that is \emph{nicely locally cwd-decomposable}. This notion generalizes that of a \emph{nicely locally tree-decomposable} class. The graphs of such classes can be covered by graphs of bounded \emph{clique-width} with limited overlaps. We also consider such labelings for \emph{bounded} first-order formulas on graph classes of \emph{bounded expansion}. Some of these results are extended to counting queries. | |
| dc.description.sponsorship | Décompositions des graphes et algorithmes - ANR-06-BLAN-0148 | |
| dc.language.iso | en | |
| dc.publisher | Springer Verlag | |
| dc.subject.en | First-Order Logic | |
| dc.subject.en | Labeling Scheme | |
| dc.subject.en | Local Clique-Width | |
| dc.subject.en | Local Tree-Width | |
| dc.subject.en | Locally Bounded Clique-Width. | |
| dc.subject.en | Locally Bounded Clique-Width | |
| dc.title.en | Compact Labelings For Efficient First-Order Model-Checking | |
| dc.type | Article de revue | |
| dc.subject.hal | Informatique [cs]/Algorithme et structure de données [cs.DS] | |
| dc.subject.hal | Informatique [cs]/Logique en informatique [cs.LO] | |
| dc.identifier.arxiv | 0811.4713 | |
| bordeaux.journal | Journal of Combinatorial Optimization | |
| bordeaux.page | 19--46 | |
| bordeaux.volume | 21 | |
| bordeaux.hal.laboratories | Laboratoire Bordelais de Recherche en Informatique (LaBRI) - UMR 5800 | * |
| bordeaux.issue | 1 | |
| bordeaux.institution | Université de Bordeaux | |
| bordeaux.institution | Bordeaux INP | |
| bordeaux.institution | CNRS | |
| bordeaux.peerReviewed | oui | |
| hal.identifier | hal-00342668 | |
| hal.version | 1 | |
| hal.popular | non | |
| hal.audience | Internationale | |
| hal.origin.link | https://hal.archives-ouvertes.fr//hal-00342668v1 | |
| bordeaux.COinS | ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.jtitle=Journal%20of%20Combinatorial%20Optimization&rft.date=2011-01-07&rft.volume=21&rft.issue=1&rft.spage=19--46&rft.epage=19--46&rft.eissn=1382-6905&rft.issn=1382-6905&rft.au=COURCELLE,%20Bruno&GAVOILLE,%20Cyril&KANT%C3%89,%20Mamadou%20Moustapha&rft.genre=article |
Fichier(s) constituant ce document
| Fichiers | Taille | Format | Vue |
|---|---|---|---|
|
Il n'y a pas de fichiers associés à ce document. |
|||