Bounded-variable fragments of hybrid logics

被引：0
|
作者：
Schwentick, Thomas [1 ]
Weber, Volker [1 ]
机构：
[1] Univ Dortmund, Fachbereich Informat, D-4600 Dortmund, Germany
来源：
STACS 2007, PROCEEDINGS | 2007年 / 4393卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Hybrid logics extend modal logics by first-order concepts, in particular they allow a limited use of variables. Unfortunately, in general, satisfiability for hybrid formulas is undecidable and model checking is PSPACE-hard. It is shown here that on the linear frame (omega, <), the restrict ion to one name, although expressively complete, has EXPSPACE-complete satisfiability and polynomial time model-checking. For the upper bound, a result of independent interest is found: Non-emptiness for alternating two-way Buchi automata with one pebble is EXPSPACE-complete.
引用
收藏
页码：561 / +
页数：3
相关论文
共 50 条
  • [1] Logics with zero-one laws that are not fragments of bounded-variable infinitary logic
    Stewart, IA
    MATHEMATICAL LOGIC QUARTERLY, 1997, 43 (02) : 158 - 178
  • [2] Compiling Existential-Positive Queries to Bounded-Variable Fragments
    Berkholz, Christoph
    Chen, Hubie
    PROCEEDINGS OF THE 38TH ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS (PODS '19), 2019, : 353 - 364
  • [3] Bounded-variable fixpoint queries are PSPACE-complete
    Dziembowski, S
    COMPUTER SCIENCE LOGIC, 1997, 1258 : 89 - 105
  • [4] BOUNDED-VARIABLE LEAST-SQUARES - AN ALGORITHM AND APPLICATIONS
    STARK, PB
    PARKER, RL
    COMPUTATIONAL STATISTICS, 1995, 10 (02) : 129 - 141
  • [5] A Fast NMPC Approach based on Bounded-Variable Nonlinear Least Squares
    Saraf, Nilay
    Zanon, Mario
    Bemporad, Alberto
    IFAC PAPERSONLINE, 2018, 51 (20): : 337 - 342
  • [6] Bounded-variable Gauss-Newton algorithm for aircraft parameter estimation
    Jategaonkar, RV
    JOURNAL OF AIRCRAFT, 2000, 37 (04): : 742 - 744
  • [7] Relation-Changing Logics as Fragments of Hybrid Logics
    Areces, Carlos
    Fervari, Raul
    Hoffmann, Guillaume
    Martel, Mauricio
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (226): : 16 - 29
  • [8] The long step rule in the bounded-variable dual simplex method: Numerical experiments
    Ekaterina Kostina
    Mathematical Methods of Operations Research, 2002, 55 : 413 - 429
  • [9] An efficient bounded-variable nonlinear least-squares algorithm for embedded MPC
    Saraf, Nilay
    Bemporad, Alberto
    AUTOMATICA, 2022, 141
  • [10] A Bounded-Variable Least-Squares Solver Based on Stable QR Updates
    Saraf, Nilay
    Bemporad, Alberto
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2020, 65 (03) : 1242 - 1247
12345