Expressiveness and complexity of graph logic

被引:23
作者
Dawar, Anui
Gardner, Philippa
Ghelli, Giorgio [1 ]
机构
[1] Univ Pisa, Dipartimento Informat, Pisa, Italy
[2] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London, England
[3] Univ Cambridge, Comp Lab, Cambridge CB2 3QG, England
基金
英国工程与自然科学研究理事会;
关键词
spatial logics; graphs; complexity; MODEL CHECKING; SPATIAL LOGIC;
D O I
10.1016/j.ic.2006.10.006
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner, and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) logics; the two versions are actually equivalent to FO and MSO on graphs representing strings, However, when the two versions are enriched with mu-style recursion, their expressive power is sharply increased. Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE. (C) 2006 Elsevier Inc. All rights reserved.
引用
收藏
页码:263 / 310
页数:48
相关论文
共 27 条
  • [1] [Anonymous], 2001, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, DOI DOI 10.1007/3-540-45294-X10
  • [2] [Anonymous], 2001, P CSL 01
  • [3] Boneva I, 2005, IEEE S LOG, P280
  • [4] BONEVA I, 2004, 3 IFIP INT C THEOR C
  • [5] Buchi J.R., 1960, Z. Math. Log. Grundl. Math., V6, P66
  • [6] Deciding validity in a spatial logic for trees
    Calcagno, C
    Cardelli, L
    Gordon, AD
    [J]. ACM SIGPLAN NOTICES, 2003, 38 (03) : 62 - 73
  • [7] Cardelli L., 2000, Conference Record of POPL'00: 27th ACM SIGPLAN-SIGACT. Symposium on Principles of Programming Languages. Papers Presented at the Symposium, P365, DOI 10.1145/325694.325742
  • [8] Cardelli L, 2002, LECT NOTES COMPUT SC, V2380, P597
  • [9] CARDELLI L, 2003, IN PRESS MATH STRUCT
  • [10] Model checking mobile ambients
    Charatonik, W
    Dal Zilio, S
    Gordon, AD
    Mukhopadhyay, S
    Talbot, JM
    [J]. THEORETICAL COMPUTER SCIENCE, 2003, 308 (1-3) : 277 - 331