Predicate μ-calculus for mobile ambients

被引:8
|
作者
Lin, HM [1 ]
机构
[1] Chinese Acad Sci, Comp Sci Lab, Inst Software, Beijing 100080, Peoples R China
关键词
model checking; mobile ambients; spatial logic; mu-calculus; fixpoints;
D O I
10.1007/s11390-005-0011-7
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Ambient logics have been proposed to describe properties for mobile agents which may evolve over time as well as space. This paper takes a predicate-based approach to extending an ambient logic with recursion, yielding a predicate mu-calculus in which fixpoint formulas are formed using predicate variables. An algorithm is developed for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for model checking a spatial logic with recursion.
引用
收藏
页码:95 / 104
页数:10
相关论文
共 50 条
  • [21] A PREDICATE CALCULUS WITH CONTROL OF DERIVATIONS
    MEY, D
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 440 : 254 - 266
  • [22] Attributive adjectives and the predicate calculus
    BenYami, H
    [J]. PHILOSOPHICAL STUDIES, 1996, 83 (03) : 277 - 289
  • [23] ON THE SIMPLE COMPLETENESS OF THE PREDICATE CALCULUS ■
    高恆珊
    [J]. ScienceinChina,Ser.A., 1964, Ser.A.1964 (02) - 215
  • [24] ON THE SIMPLE COMPLETENESS OF THE PREDICATE CALCULUS ■
    高恆珊
    [J]. Science China Mathematics, 1964, (02) : 213 - 215
  • [25] Virtually timed ambients: A calculus of nested virtualization
    Johnsen, Einar Broch
    Steffen, Martin
    Stumpf, Johanna Beate
    [J]. JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2018, 94 : 109 - 127
  • [26] CCA: a Calculus of Context-aware Ambients
    Siewe, Francois
    Cau, Antonio
    Zedan, Hussein
    [J]. 2009 INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION NETWORKING AND APPLICATIONS WORKSHOPS: WAINA, VOLS 1 AND 2, 2009, : 972 - 977
  • [27] Equational properties of mobile ambients
    Gordon, AD
    Cardelli, L
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 1999, 1578 : 212 - 226
  • [28] Typed Mobile Ambients in Maude
    Rosa-Velardo, Fernando
    Segura, Clara
    Verdejo, Alberto
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 147 (01) : 135 - 161
  • [29] Abstract interpretation of mobile ambients
    Hansen, RR
    Jensen, JG
    Nielson, F
    Nielson, HR
    [J]. STATIC ANALYSIS, 1999, 1694 : 134 - 148
  • [30] RPO semantics for mobile ambients
    Bonchi, Filippo
    Gadducci, Fabio
    Monreale, Giacoma Valentina
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2014, 24 (04)