tralala_documents_lille.inc 14.1 KB
Newer Older
1
2

<li>
3
<paper file="http://www.grappa.univ-lille3.fr/twiki/pub/Private/IovkaBoneva/BonevaTalbot-ModelChecking.pdf">
4

5
<title>On Complexity of Model-Checking for the TQL Logic</title>
6

7
<author>Iovka Boneva</author>
8
9
10

<author>Jean-Marc Talbot</author>

11
<comment>3rd IFIP International Conference on Theoretical Computer Science.</comment>
12

13
<abstract><p>In this paper we study the complexity of the model-checking problem for the tree logic introduced as the basis for the query language TQL [Cardelli, Ghelli 01: Query Language Based on the Ambient Logic]. We define two distinct fragments of this logic: TL containing only spatial connectives and TLe containing spatial connectives and quantification. We show that the combined complexity of TL is PSPACE-hard. We also study data complexity of model-checking and show that it is linear for TL, hard for all levels of the polynomial hierarchy for TLe and PSPACE-hard for the full logic. Finally we devise a polynomial space model-checking algorithm showing this way that the model-checking problem for the TQL logic is PSPACE-complete.</p></abstract>
14
15
16
</paper>
</li>

17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
<li>
<paper file="http://www.ps.uni-sb.de/Papers/abstracts/mini.html">

<title>Minimizing Tree Automata for Unranked Trees</title>

<author>Wim Martens</author>

<author>Joachim Niehren</author>

<comment>10th International Symposium on Database Programming Languages. Submitted.</comment>

<abstract><p>Automata for unranked trees form a foundation for XML schemas,
 querying and pattern languages. We study the problem of efficiently
 minimizing such automata. We start with the unranked tree automata
 (UTAs) that are standard in database theory, assuming bottom-up 
 determinism and that horizontal recursion is represented by 
 deterministic finite automata. We show that minimal 
 UTAs in that class are not unique and that minimization 
 is NP-hard. We then study more recent automata classes that do allow for 
 polynomial time minimization. Among those, we show that bottom-up
 deterministic stepwise tree automata yield the most succinct
 representations.
 
 
 </p></abstract>
</paper>
</li>

45
<li>
46
<paper file="http://www.ps.uni-sb.de/Papers/paper_info.php?label=n-ary-query">
47

48
<title>N-ary Queries by Tree Automata </title>
49
50
51

<author>Joachim Niehren</author>

52
<author>Laurent Planque</author>
53

54
<author>Jean-Marc Talbot</author>
55

56
<author>Sophie Tison</author>
57

58
<comment>A previous version has been presented at the 19th International Workshop on Unification.</comment>
59
60

<abstract><p>N-ary queries in trees select sets of n-tuples of nodes. We propose and investigate representation formalisms for n-ary queries by tree automata, both for ranked and unranked trees. We show that existential run-based queries capture MSO in the \nary case as well as universal run-based queries. We then investigate queries by unambiguous tree automata that are relevant for query induction. We characterize queries by unambiguous automata by a natural fragment of MSO, show how to decide whether regular queries are definable in that fragment, and how to answer them efficiently in linear time. </p></abstract>
61
62
63
</paper>
</li>

64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
<li>
<paper file="https://www.ps.uni-sb.de/Papers/abstracts/lambdafut.html">

<title>A  Concurrent  Lambda  Calculus  with  Futures</title>

<author>Joachim  Niehren </author>

<author> Jan  Schwinghammer </author>

<author> Gert  Smolka</author>

<comment>5th International Workshop on Frontiers in Combining Systems.</comment>

<abstract><p>
 We  introduce  a  new  concurrent  lambda  calculus  with  futures,  
 lambda(fut),  to  model  the  operational  semantics  of  Alice,  a  
 concurrent  extension  of  ML.  lambda(fut)  is  a  minimalist  
 extension  of  the  call-by-value  lambda-calculus  that  yields  
 the  full  expressiveness  to  define,  combine,  and  implement
 a  variety  of  standard  concurrency  constructs  such  as  channels,  
 semaphores,  and  ports.  We  present  a  linear  type  system  for
 lambda(fut)  by  which  the  safety  of  such  definitions  
 and  their  combinations  can  be  proved:
 Well-typed  implementations  cannot  be  corrupted  in  any  well-typed  context.
 
 </p></abstract>
</paper>
</li>

93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
<li>
<paper file="http://www.ps.uni-sb.de/Papers/abstracts/wellnested-cu.bib">

<title>Well-nested  Context  Unification</title>

<author>Jordi  Levy </author>

<author> Joachim  Niehren </author>

<author> Mateu  Villaret</author>

<comment>20th  International  Conference  on  Automated  Deduction.</comment>

<abstract><p>
 Context  unification  (CU)  is  the  famous  open  problem  of  
 solving  context  equations  for  trees.  We  distinguish  
 a  new  decidable  fragment  of  CU  -  well-nested  CU  -
 and  present  a  new  unification  algorithm  that  solves  
 well-nested  context  equations  in  non-deterministic  
 polynomial  time.  We  show  that  minimal  
 well-nested  solutions  of  context  equations  can  be
 composed  from  the  material  present  in  the  equation.  
 This  surprising  property  is  highly  wishful  when  
 modeling  natural  language  ellipsis  in  CU.  
 
 </p></abstract>
</paper>
</li>

<li>
123
<paper file="http://www.lifl.fr/~debarbie/DOC/IndexesAndPathConstraints.pdf">
124

125
<title>Indexes and path constraints in semistructured data</title>
126

127
<author>Yves Andre</author>
128

129
<author>Anne-Cecile Caron</author>
130

131
<author>Denis Debarbieux</author>
132

133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
<author>Yves Roos</author>

<comment>Workshop on Logical Aspects and Applications of Integrity Constraints.</comment>

<abstract><p>In this paper, we study semistructured data and indexes preserving
inclusion constraints.
A semistructured datum is modelled by multi-rooted edge-labeled
directed graphs. 
We consider regular path queries and inclusion constraints other these data.
These constraints are binary relations over regular 
path expressions q and r, and are interpreted on a datum as
``for this datum, the answer to query q is included in the answer to query r''.
We study how to represent inclusion constraints that are common to several data.
Our work is based on two existing indexes: dataguide and 1-index. 
Given a set of data S, we extract from the
dataguide of S a finite set C(S) of  (finite) inclusion constraints 
such that an inclusion constraint is satisfied by a datum of S if
and only if it is implied by C(S).
 We use 1-index which are covering indexes preserving inclusion
constraints. 
Experiments
compare the different ways of using the 1-index to index a set of data.</p></abstract>
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
</paper>
</li>

<li>
<paper file="http://www.lifl.fr/~debarbie/DOC/ExtractionAndImplicationOfPathConstraints.pdf">

<title>Extraction and Implication of Path Constraints</title>

<author>Yves André</author>

<author>Anne-Cécile Caron</author>

<author>Denis Debarbieux</author>

<author>Yves Roos</author>

<author>Sophie Tison</author>

<comment>Proceedings of the 29th Symposium on Mathematical Foundations of Computer Science.</comment>

<abstract><p>We consider semistructured data as rooted edge-labeled directed graphs, and path inclusion
constraints on these graphs.
In this paper, we give a new decision algorithm 
for the implication problem of a constraint
$p  \preceq q$ by a set of constraints $p_i  \preceq u_i$ where $p$, $q$, and the $p_i$'s are regular
path expressions and the $u_i$'s are non-empty paths, improving in this particular  case, the
more general algorithms of S. Abiteboul and V. Vianu, and Alechina et al.
Moreover, in the case of a set of word equalities $u_i \equiv v_i$, we give a more efficient 
decision algorithm for the implication of a word equality $u \equiv v$,  improving the 
more general algorithm of P. Buneman et al., and
we prove that, in this case, the implication problem for non-deterministic models or 
for (complete) deterministic models are equivalent.</p></abstract>
</paper>
</li>

<li>
191
<paper file=" http://www.ps.uni-sb.de/Papers/abstracts/clls-cu.html">
192

193
<title>Describing  Lambda  Terms  in  Context  Unification</title>
194
195
196

<author>Joachim Niehren</author>

197
<author>Mateu Villaret</author>
198

199
200
201
202
203
204
205
206
207
208
209
210
<comment>5th International Conference on Logical Aspects in Computational Linguistics.</comment>

<abstract><p>The  constraint  language  for  lambda  structures  (CLLS)  is
a  description  language  for  lambda  terms.  CLLS  provides
parallelism  constraints  to  talk  about  the  tree  structure  
of  lambda  terms,  and  lambda  binding  constraints  to  specify
variable  binding.  
Parallelism  constraints  alone  have  
the  same  expressiveness  as  context  unification.  In  this  paper,
we  show  that  lambda  binding  constraints  can  also  be  expressed  
in  context  unification  when  permitting  tree  
regular  constraints.  </p></abstract>
211
212
213
214
</paper>
</li>

<li>
215
<paper file="http://www.lifl.fr/~boneva/papers/lics2005.pdf">
216

217
<title>Expressiveness of a spatial logic for trees</title>
218

219
<author>Iovka Boneva</author>
220

221
<author>Jean-Marc Talbot</author>
222

223
<author>Sophie Tison</author>
224

225
<comment>20th Annual IEEE Symposium on Logic in Computer Science.</comment>
226

227
<abstract><p>In this paper we investigate the quantifier-free fragment of the TQL logic proposed by Cardelli and Ghelli. The TQL logic, inspired from the ambient logic, is the core of a query language for semistructured data represented as unranked and unordered trees. The fragment we consider here, named STL, contains as main features spatial composition and location as well as a fixed point construct. We prove that satisfiability for STL is undecidable.We show also that STL is strictly more expressive that the Presburger monadic second-order logic (PMSO) of Seidl, Schwentick and Muscholl when interpreted over unranked and unordered edge-labeled trees. We define a class of tree automata whose transitions are conditioned by arithmetical constraints; we show then how to compute from a closed STL formula a tree automaton accepting precisely the models of the formula. Finally, still using our tree automata framework, we exhibit some syntactic restrictions over STL formulae that allow us to capture precisely the logics MSO and PMSO.</p></abstract>
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
</paper>
</li>

<li>
<paper file="http://www.ps.uni-sb.de/Papers/abstracts/pdl05.html">

<title>Complexity of Subtype Satisfiability over Posets</title>

<author>Joachim Niehren</author>

<author>Tim Priesnitz</author>

<author>Zhendong Su</author>

<comment>14th European Symposium on Programming.</comment>

<abstract><p>Subtype satisfiability is an important problem for designing advanced
subtype systems and subtype-based program analysis algorithms. The
problem is well understood if the atomic types form a lattice. However,
little is known about subtype satisfiability over posets. In this
paper, we investigate algorithms for and the complexity of subtype
satisfiability over general posets. We present a uniform treatment of
different flavors of subtyping: simple versus recursive types and
structural versus non-structural subtype orders. Our results are
established through a new connection of subtype constraints and modal
logic. As a consequence, we settle a problem left open by Tiuryn and
Wand in 1993.</p></abstract>
</paper>
</li>

258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
<li>
<paper file="http://www.lifl.fr/~boneva/papers/rta2005.pdf">

<title>Automata and Logics for Unranked and Unordered Trees</title>

<author>Iovka Boneva</author>

<author>Jean-Marc Talbot</author>

<comment>20th International Conference on Rewriting Techniques and Applications.</comment>

<abstract><p>In this paper, we consider the monadic second order logic (MSO) and two of its extensions, namely Counting MSO (CMSO) and Presburger MSO (PMSO), interpreted over unranked and unordered trees. We survey classes of tree automata introduced for the logics PMSO and CMSO as well as other related formalisms; we gather results from the literature and sometimes clarify or fill the remaining gaps between those various formalisms. Finally, we complete our study by adapting these classes of automata for capturing precisely the expressiveness of the logic MSO.</p></abstract>
</paper>
</li>

<li>
<paper file="http://www.ps.uni-sb.de/Papers/abstracts/sub-journal.html">

<title>First-Order Theory of Subtyping Constraints</title>

<author>Zhendong Su</author>

<author>Alexander Aiken</author>

<author>Joachim Niehren</author>

<author>Tim Priesnitz</author>

<author>Ralf Treinen</author>

<comment>TOPLAS.  Extended Version of ACM POPL 2002.</comment>

<abstract><p>We investigate the first-order theory of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping.
Our results hold for both simple and recursive types. The undecidability result is shown by a reduction from the Post's Correspondence Problem, and
the decidability results are shown by a reduction to a decision problem on tree automata. In addition, we introduce the notion of a constrained tree automaton to express non-structural subtype entailment.
This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.</p></abstract>
</paper>
</li>

297
298
299
300
301
302
303
<li>
<paper file="https://www.ps.uni-sb.de/Papers/abstracts/cut.html">

<title>Interactive  Learning  of  Node  Selection  Queries  in  Tree  Structured  Documents</title>

<author>Julien  Carme </author>

304
<author> Rémi  Gilleron</author>
305

306
<author> Aurélien  Lemay </author>
307

308
<author> Joachim  Niehren</author>
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326

<comment>IJCAI  Workshop  on  Grammatical  Inference.</comment>

<abstract><p>
 We  present  a  new  learning  process  for  Web  information
    extraction,  that  is  visually  interactive.    Web  documents  are
    considered  as  trees  in  which  wrappers  select  sets  of  nodes.    
    We  start  from  a  recent  algorithm  that  induces  node  selection  
    queries  in  trees  by
    methods  of  grammatical  inference.  We  then  show  how  to  turn  this
    algorithm  into  our  visually  interactive  learning  process,  using
    intelligent  tree  pruning  heuristics.    Experiments  on  realistic  Web
    documents  confirm  excellent  quality  with  very  few  user
    interactions  --  annotations  and  corrections  --  during  wrapper  induction.
 
 </p></abstract>
</paper>
</li>