Modal and guarded characterisation theorems over finite transition systems

被引:23
|
作者
Otto, M [1 ]
机构
[1] Tech Univ Darmstadt, Fachbereich Math, D-64289 Darmstadt, Germany
基金
英国工程与自然科学研究理事会;
关键词
finite model theory; modal logic; guarded fragment; bisimulation; preservation; characterisation theorems;
D O I
10.1016/j.apal.2004.04.003
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
We explore the finite model theory of the characterisation theorems for modal and guarded fragments of first-order logic over transition systems and relational structures of width two. A new construction of locally acyclic bisimilar covers provides a useful analogue of the well known treelike unravellings that can be used for the purposes of finite model theory. Together with various other finitary bisimulation respecting model transformations, and Ehrenfeucht-Fraisse game arguments, these covers allow us to upgrade finite approximations for full bisimulation equivalence towards approximations for elementary equivalence. These techniques are used to prove several ramifications of the van Benthem-Rosen characterisation theorem of basic modal logic for refinements of ordinary bisimulation equivalence, both in the sense of classical and of finite model theory. (C) 2004 Elsevier B.V. All rights reserved.
引用
收藏
页码:173 / 205
页数:33
相关论文
共 50 条
  • [21] MODAL SYSTEMS WITH A FINITE NUMBER OF MODALITIES
    莫绍揆
    ScienceinChina,SerA., 1958, Ser.A.1958 (04) : 388 - 412
  • [22] AltaRica 3.0 project: Compile Guarded Transition Systems into Fault Trees
    Prosvirnova, T.
    Rauzy, A.
    SAFETY, RELIABILITY AND RISK ANALYSIS: BEYOND THE HORIZON, 2014, : 1121 - 1128
  • [23] From Featured Transition Systems to Modal Transition Systems with Variability Constraints
    ter Beek, Maurice H.
    Damiani, Ferruccio
    Gnesi, Stefania
    Mazzanti, Franco
    Paolini, Luca
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2015, 9276 : 344 - 359
  • [24] Modal transition system encoding of featured transition systems
    Varshosaz, Mahsa
    Luthmann, Lars
    Mohr, Paul
    Lochau, Malte
    Mousavi, Mohammad Reza
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 106 : 1 - 28
  • [25] Failure Semantics for Modal Transition Systems
    Bujtor, Ferenc
    Vogler, Walter
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2015, 14 (04)
  • [26] Beyond the Classical Modal Transition Systems
    Srba, Jiri
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (87): : 1 - 4
  • [27] Modal transition systems with weight intervals
    Juhl, Line
    Larsen, Kim G.
    Srba, Jiri
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (04): : 408 - 421
  • [28] Coherent modal transition systems refinement
    Basile, Davide
    ter Beek, Maurice H.
    Fantechi, Alessandro
    Gnesi, Stefania
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2024, 138
  • [29] MODAL LOGICS FOR NOMINAL TRANSITION SYSTEMS
    Parrow, Joachim
    Borgstrom, Johannes
    Eriksson, Lars-Henrik
    Gutkovas, Ramunas Forsberg
    Weber, Tjark
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (01) : 6:1 - 6:49
  • [30] Structural theorems on the distance sets over finite fields
    Koh, Doowon
    Pham, Minh Quy
    Pham, Thang
    FORUM MATHEMATICUM, 2023, 35 (04) : 925 - 938