Predicate μ-calculus for mobile ambients

被引：8
|
作者：
Lin, HM [1 ]
机构：
[1] Chinese Acad Sci, Comp Sci Lab, Inst Software, Beijing 100080, Peoples R China
来源：
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2005年 / 20卷 / 01期
关键词：
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 条
  • [1] Predicate μ-Calculus for Mobile Ambients
    Hui-Min Lin
    [J]. Journal of Computer Science and Technology, 2005, 20 : 95 - 104
  • [2] Reflecting mobile ambients into the π-calculus
    Brodo, L
    Degano, P
    Priami, C
    [J]. GLOBAL COMPUTING: PROGRAMMING ENVIRONMENTS, LANGUAGES, SECURITY, AND ANALYSIS OF SYSTEMS, 2003, 2874 : 25 - 56
  • [3] Encoding mobile ambients into the π-calculus
    Ciobanu, Gabriel
    Zakharov, Vladimir A.
    [J]. PERSPECTIVES OF SYSTEMS INFORMATICS, 2007, 4378 : 148 - 165
  • [4] On the Expressiveness of the π-Calculus and the Mobile Ambients
    Brodo, Linda
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 2011, 6486 : 44 - 59
  • [5] On the expressiveness of π-calculus for encoding mobile ambients
    Brodo, Linda
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2018, 28 (02) : 202 - 240
  • [6] Access control for mobile agents: The calculus of boxed ambients
    Bugliesi, M
    Castagna, G
    Crafa, S
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2004, 26 (01): : 57 - 124
  • [7] Maintenance of mobile system ambients using a process calculus
    Ando, T
    Takahashi, K
    Kato, Y
    Shiratori, N
    [J]. COMPUTER NETWORKS, 2000, 32 (02) : 229 - 256
  • [8] Mobile ambients
    Cardelli, L
    Gordon, AD
    [J]. THEORETICAL COMPUTER SCIENCE, 2000, 240 (01) : 177 - 213
  • [9] Mobile ambients
    Cardelli, L
    Gordon, AD
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 1998, 1378 : 140 - 155
  • [10] Investigations into the Predicate Calculus
    Wieckowski, Bartosz
    [J]. STUDIA LOGICA, 2024,
12345