移动智能体的形式化研究.pdf

收藏

编号:20181207061551326113    类型:共享资源    大小:111.19KB    格式:PDF    上传时间:2019-02-16
  
5
金币
关 键 词:
的形式化 智能体 PDF 形式化 智能体的 的形式化研究
资源描述:
文 章 编 号 : 1?0?0?1?-?2?4?8?6?( 2?0?0?0?) 0?6?-?0?0?4?7?-?0?5? 移 动 智 能 体 的 形 式 化 研 究 !? 吴 泉 源 , 吴 刚 , 王 怀 民 ( 国 防 科 技 大 学 计 算 机 学 院 , 湖 南 长 沙 4?1?0?0?7?3?) 摘 要 : 移 动 智 能 体 是 当 前 分 布 计 算 领 域 的 研 究 热 点 之 一 , 但 是 其 理 论 研 究 还 处 于 一 个 很 不 成 熟 的 阶 段 。 文 中 阐 述 了 对 移 动 智 能 体 作 形 式 化 研 究 的 必 要 性 , 介 绍 了 当 前 的 研 究 现 状 , 分 析 了 其 中 的 不 足 , 并 进 一 步 给 出 了 对 后 续 工 作 的 展 望 。 关 键 词 : 移 动 智 能 体 ; 并 发 模 型 ; 进 程 代 数 ; !?演 算 中 图 分 类 号 : T?P?3?1?1?文 献 标 识 码 : A? R?e?S?e?a?r?c?h? O?n? F?O?r?m?a?l? M?O?d?e?l? O?f? M?O?b?i?l?e? A?g?e?n?t? W?U? O?u?a?n?-?Y?u?a?n?, W?U? G?a?n?g?, W?A?N?G? H?u?a?i?-?M?i?n? ( C?O?I?I?e?g?e? O?f? C?O?m?p?u?t?e?r?, N?a?t?i?O?n?a?I? U?n?i?v?e?r?s?i?t?y? O?f? D?e?f?e?n?c?e? T?e?c?h?n?O?I?O?g?y?, C?h?a?n?g?s?h?a? 4?1?0?0?7?3?) A?b?S?t?r?a?c?t?: M?O?b?i?I?e? a?g?e?n?t? r?e?c?e?i?v?e?s? m?u?c?h? a?t?t?e?n?t?i?O?n? r?e?c?e?n?t?I?y? i?n? t?h?e? d?i?s?t?r?i?b?u?t?e?d? c?O?m?p?u?t?i?n?g? f?i?e?I?d?.? B?u?t? t?h?e? r?e?s?e?a?r?c?h? O?n? i?t?s? f?O?r?m?a?I? m?O?d?e?I? i?s? i?m?m?a?t?u?r?e?.? T?h?e? n?e?c?e?s?s?i?t?y? O?f? t?h?e? f?O?r?m?a?I? r?e?s?e?a?r?c?h? O?f? m?O?b?i?I?e? a?g?e?n?t? i?s? a?n?a?I?y?Z?e?d? f?i?r?s?t?I?y?.? T?h?e?n? w?e? i?n?t?r?O?d?u?c?e? s?e?v?e?r?a?I? r?e?p?r?e?s?e?n?t?a?t?i?v?e? f?O?r?m?a?I? m?O?d?-? e?I?s?, a?n?a?I?y?Z?e? t?h?e?i?r? d?r?a?w?b?a?c?k?s?, a?n?d? p?r?e?s?e?n?t? t?h?e? p?r?O?s?p?e?c?t?s? f?O?r? t?h?e? f?u?t?u?r?e? w?O?r?k?.? K?e?y? w?O?r?d?S?: m?O?b?i?I?e? a?g?e?n?t?; c?O?n?c?u?r?r?e?n?t? m?O?d?e?I?; p?r?O?c?e?s?s? a?I?g?e?b?r?a?; !?-?c?a?I?c?u?I?u?s? 2?0? 世 纪 9?0? 年 代 以 来 , 随 着 全 球 通 信 网 与 I?n?t?e?r?n?e?t? 的 蓬 勃 发 展 , 以 及 网 络 技 术 的 逐 渐 成 熟 , 分 布 式 计 算 系 统 ( D?i?s?t?r?i?b?u?t?e?d? C?O?m?p?u?t?i?n?g? S?y?s?t?e?m?) 已 经 成 为 计 算 机 科 学 领 域 的 一 项 关 键 性 主 流 技 术 和 一 种 重 要 的 计 算 范 型 。 随 着 应 用 的 不 断 深 入 , 分 布 式 系 统 也 变 得 日 趋 复 杂 和 庞 大 , 提 出 一 个 合 理 的 抽 象 概 念 模 型 来 刻 画 分 布 式 计 算 系 统 中 的 计 算 实 体 对 于 应 用 的 设 计 与 实 现 是 极 为 重 要 的 。 于 是 人 们 引 入 了 智 能 体 ( A?g?e?n?t?) 的 概 念 。 一 个 软 件 A?g?e?n?t? 可 以 定 义 为 一 个 能 够 与 环 境 交 互 并 作 出 反 应 的 自 主 软 件 实 体 , 其 主 要 特 性 包 括 自 主 性 、 交 互 性 和 反 应 性 。 移 动 智 能 体 ( M?O?b?i?I?e? A?g?e?n?t?) 作 为 一 种 特 殊 的 A?g?e?n?t?, 也 是 作 为 一 种 新 型 的 分 布 计 算 模 式 , 近 年 来 得 到 了 广 泛 的 关 注 与 研 究 [ 1?, 2?, 3?, 4?] 。 在 移 动 智 能 体 计 算 模 式 下 , A?g?e?n?t? 通 过 在 网 络 中 的 自 主 移 动 与 运 行 来 完 成 任 务 , 并 使 得 大 多 数 的 交 互 行 为 在 本 地 发 生 。 人 们 普 遍 希 望 能 借 助 移 动 智 能 体 计 算 模 型 实 现 分 布 式 应 用 从 局 域 网 平 台 向 大 规 模 ( L?a?r?g?e?-?s?c?a?I?e?) 的 网 络 计 算 平 台 的 转 移 。 如 图 1? 所 示 , 一 个 移 动 智 能 体 是 一 个 活 动 的 、 自 主 的 计 算 实 体 , 能 从 异 构 网 络 中 的 一 台 机 器 移 动 到 另 一 台 上 执 行 。 一 般 认 为 , 智 能 体 的 迁 移 包 括 了 相 应 代 码 、 数 据 和 运 行 时 状 态 的 移 动 。 根 据 A?g?e?n?t? 的 概 念 描 述 , 一 个 移 动 智 能 体 至 少 应 包 括 自 主 性 、 交 互 性 、 反 应 性 和 移 动 性 这 些 特 性 。 自 主 性 使 得 智 能 体 可 以 不 受 外 在 的 直 接 干 预 而 独 立 运 行 ; 交 互 性 使 之 能 与 包 括 人 、 设 备 和 其 他 智 能 体 在 内 的 实 体 进 行 通 讯 ; 反 应 性 使 之 能 对 环 境 的 改 变 作 出 及 时 的 反 应 ; 移 动 性 使 得 智 能 体 能 在 运 行 时 实 现 异 构 网 络 上 的 自 主 迁 移 。 1?移 动 智 能 体 形 式 化 研 究 的 必 要 性 分 布 计 算 系 统 的 实 现 要 求 必 须 是 可 靠 且 易 于 维 护 的 , 这 就 需 要 相 应 的 理 论 指 导 以 及 严 格 的 形 式 化 开 发 方 法 和 工 具 的 支 持 。 随 着 分 布 计 算 技 术 的 不 断 发 展 及 其 应 用 的 不 断 深 入 , 分 布 计 算 系 统 的 开 发 面 临 着 许 多 理 论 课 题 , 主 要 体 现 在 : 如 何 获 取 、 规 范 和 分 析 分 布 计 算 系 统 的 需 求 ; 如 何 基 于 某 种 抽 象 的 国 防 科 技 大 学 学 报 第 2?2? 卷 第 6? 期 J?O?U?R?N?A?L? O?F? N?A?T?I?O?N?A?L? U?N?I?V?E?R?S?I?T?Y? O?F? D?E?F?E?N?S?E? T?E?C?H?N?O?L?O?G?Y?V?O?I?.?2?2? N?O?.?6? 2?0?0?0? !?收 稿 日 期 : 2?0?0?0?-?0?6?-?2?0? 基 金 项 目 : 国 家 自 然 科 学 基 金 ( 6?9?8?3?3?0?3?0?) , 国 家 8?6?3? 计 划 项 目 ( 8?6?3?-?3?0?6?-?Z?D?0?2?-?0?1?-?2?) 作 者 简 介 : 吴 泉 源 ( 1?9?4?2?-?) , 男 , 教 授 , 博 士 生 导 师 。 图 l? M?O?b?i?1?e? a?g?e?D?t? 计 算 模 式 F?i?g?.?l?M?O?b?i?1?e? a?g?e?D?t? c?O?m?p?u?t?i?D?g? m?O?c?e?1? 计 算 模 型 来 指 导 分 布 计 算 系 统 的 设 计 。 等 等 。 为 了 规 范 分 布 计 算 系 统 中 的 各 个 计 算 实 体 、 描 述 计 算 实 体 之 间 的 合 作 方 式 和 交 互 行 为 , 人 们 引 入 了 A?g?e?D?t? 这 样 一 个 合 理 的 抽 象 概 念 模 型 , 并 展 开 了 对 A?g?e?D?t? 的 形 式 化 研 究 , 旨 在 获 取 分 布 计 算 系 统 的 特 性 , 以 指 导 基 于 A?g?e?D?t? 的 分 布 计 算 系 统 的 设 计 与 开 发 。 l?9?9?3? 年 , Y?O?a?V? S?1?O?1?a?m? 在 杂 志 《 A?r?t?i?f?i?c?i?a?1? I?D?t?e?1?1?i?g?e?D?c?e?》 上 发 表 了 题 为 “ A?g?e?D?t?-?0?r?i?e?D?t?e?c? P?r?O?g?r?a?m?m?i?D?g?” 的 文 章 [ 5?] , A?0?P? 是 一 种 以 计 算 的 社 会 观 为 基 础 的 新 型 程 序 设 计 语 言 。 S?1?O?1?a?m? 认 为 一 个 完 整 的 A?0?P? 系 统 应 包 括 以 下 三 个 主 要 成 分 : ( l?) 一 种 约 束 的 形 式 化 语 言 , 具 有 清 晰 的 语 法 和 语 义 来 定 义 A?g?e?D?t? 的 认 知 状 态 ; ( 2?) 一 种 解 释 型 的 程 序 设 计 语 言 , 用 于 定 义 A?g?e?D?t? 以 及 对 A?g?e?D?t? 进 行 编 程 , 并 具 有 请 求 、 通 知 等 通 讯 原 语 , 其 语 义 应 忠 实 于 认 知 状 态 的 语 义 ; ( 3?) 一 个 A?g?e?D?t? 的 生 成 器 ( A?g?e?D?t?i?f?i?e?r?) 。 从 理 论 的 角 度 来 看 , 并 发 模 型 被 认 为 是 分 布 式 计 算 的 形 式 化 基 础 。 研 究 人 员 在 规 约 模 型 、 逻 辑 模 型 、 进 程 代 数 、 P?e?t?r?i? 网 等 不 同 的 体 系 下 分 别 对 基 于 A?g?e?D?t? 的 分 布 式 计 算 进 行 了 形 式 化 研 究 , 包 括 一 阶 分 枝 时 序 逻 辑 [ 6?] 、 异 步 多 体 的 !?演 算 [ 7?] 等 等 。 移 动 智 能 体 ( M?O?b?i?1?e? A?g?e?D?t?) 作 为 分 布 式 计 算 中 的 新 生 事 物 , 其 计 算 实 体 在 网 络 环 境 下 的 可 移 动 性 为 基 于 并 发 模 型 的 形 式 化 研 究 带 来 了 新 课 题 。 但 是 这 方 面 的 理 论 研 究 还 处 于 一 个 很 不 成 熟 的 研 究 阶 段 , 导 致 了 已 有 的 移 动 智 能 体 系 统 缺 乏 理 论 的 指 导 , 各 自 在 移 动 智 能 体 系 统 的 应 用 、 安 全 、 可 用 性 、 异 构 性 等 方 面 有 着 不 同 的 假 设 前 提 , 缺 乏 一 个 统 一 的 术 语 规 范 和 公 共 的 方 法 学 框 架 。 近 期 出 现 了 许 多 支 持 移 动 应 用 的 编 程 语 言 , 包 括 J?a?V?a? 和 一 些 面 向 移 动 智 能 体 计 算 模 型 的 原 型 语 言 。 J?a?V?a? 使 得 客 户 可 以 从 其 它 站 点 上 下 载 自 包 含 的 程 序 作 本 地 执 行 , 但 并 不 能 直 接 支 持 移 动 智 能 体 的 计 算 模 型 ; 而 那 些 原 型 语 言 , 包 括 F?a?c?i?1?e? [ 8?] , 0?b?1?i?g? [ 9?] , C?M?L? [ l?0?] 和 T?e?1?e?S?c?r?i?p?t? [ l?l?] 等 , 虽 然 直 接 面 向 移 动 计 算 设 计 , 但 并 没 有 坚 实 的 形 式 化 模 型 作 基 础 , 各 自 以 不 同 的 方 式 实 现 了 迁 移 机 制 , 使 得 各 自 的 移 动 语 义 很 难 界 定 , 相 互 之 间 很 难 比 较 与 互 模 拟 。 因 而 , 我 们 需 要 一 个 抽 象 的 语 义 框 架 , 使 得 人 们 可 以 更 好 地 理 解 和 形 式 化 面 向 移 动 计 算 的 编 程 语 言 , 并 以 此 作 为 设 计 和 实 现 分 布 式 编 程 语 言 及 移 动 计 算 应 用 的 形 式 化 基 础 。 !?移 动 智 能 体 形 式 化 研 究 的 现 状 作 为 分 布 式 计 算 的 形 式 化 基 础 , 并 发 模 型 也 就 当 然 地 成 为 研 究 移 动 智 能 体 理 论 模 型 的 起 点 。 已 有 的 研 究 工 作 基 本 上 是 从 某 个 较 成 熟 的 形 式 系 统 出 发 , 针 对 移 动 智 能 体 计 算 中 计 算 实 体 的 可 移 动 特 征 作 了 相 应 的 扩 展 , 使 之 能 够 有 效 地 表 达 并 发 对 象 的 移 动 特 性 。 大 致 可 以 将 它 们 分 成 三 类 : · 归 约 模 型 。 Y?O?D?e?Z?a?w?a? 实 验 室 的 “?c?i?S?t? 演 算 [ l?2?] 是 在 传 值 ( c?a?1?1?-?b?y?-?V?a?1?u?e?) “?演 算 基 础 上 所 作 的 分 布 式 扩 展 。 计 算 实 体 的 语 法 被 定 义 为 e?: : =? P? \? 8? ? \? x? \?!?x?.? e? \? e?e? \? ? 其 中 x? 是 一 个 变 量 ; !?x?.? e? 是 一 个 抽 象 ; e?e? 是 一 个 应 用 ; P? 表 示 运 行 环 境 , 类 似 于 T?e?1?e?S?c?r?i?p?t? 中 P?1?a?c?e? 的 概 念 ; ?表 示 一 个 a?g?e?D?t?; 而 a?g?e?D?t? 的 迁 移 用 8? ? P? 来 表 示 , P? 为 移 动 的 目 的 地 , 在 执 行 了 8? ? 表 达 8?4? 国 防 科 技 大 学 学 报 2?0?0?0? 年 第 6? 期 式 之 后 , a?g?e?n?t? 的 后 续 部 分 将 移 动 到 p? 继 续 执 行 。 为 了 能 够 表 达 多 个 移 动 语 言 系 统 中 的 不 同 数 据 移 动 机 制 , !?d?i?s?t? 演 算 还 定 义 了 六 种 数 据 移 动 类 型 : c?O?p?y?、 r?e?s?i?d?e?n?t?、 c?a?r?r?y?、 p?r?O?p?e?r?、 t?a?k?e?a?w?a?y?、 u?b?i?g?。 !?d?i?s?t?演 算 能 描 述 A?g?e?n?t? 移 动 机 制 和 一 些 其 它 的 分 布 计 算 机 制 , 诸 如 同 步 、 远 程 引 用 等 。 通 过 对 O?b?l?i?g?、 T?e?l?e?s?c?r?i?p?t?、 ?a?v?a? 和 F?A?C?I?L?E? 等 移 动 智 能 体 语 言 系 统 的 形 式 化 描 述 , !?d?i?s?t? 演 算 还 试 图 为 它 们 之 间 的 互 模 拟 提 供 支 持 。 但 由 于 !?演 算 本 身 描 述 的 是 串 行 计 算 且 又 不 支 持 面 向 对 象 的 描 述 , 为 实 现 对 异 步 通 信 和 对 象 实 体 的 描 述 , !?d?i?s?t? 演 算 引 入 了 许 多 复 杂 的 结 构 , 在 一 定 程 度 上 丧 失 了 !?演 算 包 括 简 洁 性 在 内 的 许 多 特 性 。 · 时 序 逻 辑 模 型 。 U?N?I?T?Y? [ l?3?] 是 一 种 以 时 序 逻 辑 为 基 础 的 基 于 状 态 的 形 式 化 方 法 , 但 标 准 的 U?N?I?T?Y? 由 于 只 能 表 达 计 算 实 体 的 静 态 结 构 , 并 不 适 合 于 处 理 移 动 计 算 系 统 中 的 问 题 。 M?c?C?a?n?n?、 R?O?m?a?n? 等 人 便 在 U?N?I?T?Y? 的 基 础 上 作 了 相 应 扩 展 , 以 支 持 可 动 态 重 配 置 的 分 布 式 系 统 的 分 析 与 建 模 , 并 称 之 为 M?O?b?i?l?e? U?N?I?T?Y? [ l?4?] 。 M?O?b?i?l?e? U?N?I?T?Y? 提 供 了 一 组 形 式 化 的 符 号 , 以 捕 获 移 动 行 为 和 移 动 结 点 之 间 的 瞬 时 交 互 , 并 包 含 有 一 个 断 言 式 的 验 证 逻 辑 , 用 于 推 理 移 动 计 算 系 统 的 特 性 。 一 个 用 M?O?b?i?l?e? U?N?I?T?Y? 描 述 的 系 统 由 三 个 部 分 组 成 [ l?5?] : D?e?c?l?a?r?e? 部 分 、 C?O?m?p?O?n?e?n?t? 部 分 和 I?n?t?e?r?a?c?t?i?O?n? 部 分 。 D?e?c?l?a?r?e? 部 分 描 述 了 程 序 组 件 中 的 变 量 及 其 类 型 , 包 括 刻 画 位 置 的 变 量 ; C?O?m?p?O?n?e?n?t? 部 分 对 程 序 中 变 量 作 实 例 化 操 作 ; I?n?t?e?r?a?c?t?i?O?n? 部 分 给 出 了 程 序 组 件 实 例 的 瞬 时 交 互 描 述 。 M?O?b?i?l?e? U?N?I?T?Y? 描 述 的 移 动 计 算 系 统 是 在 程 序 组 件 之 间 的 瞬 时 连 接 条 件 下 进 行 操 作 的 , 连 接 由 当 前 的 位 置 决 定 , 因 此 位 置 便 成 为 该 模 型 中 的 重 要 概 念 。 但 是 模 型 并 没 有 对 位 置 变 量 做 类 型 限 制 , 它 可 以 是 离 散 或 连 续 的 , 也 可 以 是 移 动 平 台 的 物 理 坐 标 或 移 动 a?g?e?n?t? 所 在 的 网 络 。 进 程 通 过 设 置 位 置 变 量 非 显 式 地 刻 划 移 动 , 形 如 !?: =? N?e?w?L?O?c?( !?) , 该 函 数 将 返 回 一 个 新 位 置 , 并 表 示 进 程 将 迁 移 到 此 新 位 置 继 续 执 行 。 然 而 , M?O?b?i?l?e? U?N?I?T?Y? 研 究 的 初 衷 是 为 了 解 决 移 动 通 讯 环 境 下 由 于 硬 件 设 备 的 移 动 而 引 发 的 计 算 组 件 交 互 关 系 的 重 配 置 , 以 及 由 于 移 动 网 络 链 路 的 易 断 接 而 引 发 的 交 互 重 建 等 问 题 。 并 不 是 针 对 移 动 智 能 体 这 样 的 软 件 实 体 移 动 而 设 计 的 。 P?i?c?c?O? 在 文 献 [ l?6?] 中 研 究 了 将 M?O?b?i?l?e? U?N?I?T?Y? 用 于 移 动 智 能 体 形 式 化 表 示 的 可 行 性 , 认 为 M?O?b?i?l?e? U?N?I?T?Y? 作 为 一 个 形 式 系 统 , 并 没 有 限 制 移 动 实 体 的 具 体 定 位 , 也 并 不 排 除 对 位 置 空 间 这 一 概 念 更 为 抽 象 的 理 解 。 因 而 , 可 以 用 之 来 描 述 移 动 智 能 体 计 算 模 型 , 并 能 利 用 M?O?b?i?l?e? U?N?I?T?Y? 的 验 证 逻 辑 来 证 明 移 动 智 能 体 应 用 程 序 的 正 确 性 。 · 进 程 代 数 。 移 动 智 能 体 的 形 式 化 研 究 中 最 活 跃 的 一 组 , 是 从 进 程 代 数 入 手 的 。 包 括 D?“? !?演 算 [ l?7?] 、 分 布 式 ?O?i?n? 演 算 [ l?8?] 、 D?“?演 算 [ l?9?] 、 K?L?A?I?M? [ 2?O?] 及 A?m?a?d?i?O? 的 一 些 工 作 [ 2?l?, 2?2?] 等 。 “?演 算 [ 2?3?] 作 为 一 种 并 发 计 算 的 理 论 模 型 , 通 过 少 量 的 结 构 为 并 发 计 算 提 供 了 强 大 的 描 述 能 力 和 简 洁 的 语 义 说 明 。 但 是 并 发 计 算 与 分 布 式 计 算 之 间 有 着 许 多 不 同 , 尤 其 对 于 分 布 式 移 动 计 算 系 统 而 言 , “?演 算 存 在 许 多 不 足 。 例 如 移 动 智 能 体 系 统 中 计 算 实 体 的 移 动 是 一 个 异 步 的 过 程 , 而 典 型 “?演 算 中 原 子 性 的 非 本 地 交 互 是 用 基 于 会 合 的 同 步 通 信 来 描 述 的 ; 再 例 如 “?演 算 中 没 有 显 式 的 位 置 概 念 , 不 便 于 描 述 运 行 实 体 的 自 主 移 动 , 等 等 。 因 而 , 许 多 研 究 工 作 都 通 过 对 “?演 算 的 分 布 式 扩 展 来 实 现 了 对 移 动 计 算 的 有 效 表 述 。 ( l?) ~?e?n?n?e?s?s?y? 的 D?“?演 算 。 在 通 用 的 P?O?l?y?a?d?i?c?“?演 算 [ 7?] 的 基 础 上 , 他 引 入 了 显 式 的 位 置 概 念 , 并 扩 展 了 位 置 之 间 的 移 动 原 语 及 新 位 置 的 创 建 原 语 。 在 D?“?演 算 中 , 异 步 的 消 息 传 递 与 A?g?e?n?t? 的 显 式 移 动 被 统 一 为 一 种 形 式 , 任 何 异 步 的 消 息 传 递 均 通 过 子 A?g?e?n?t? 的 移 动 加 上 本 地 的 同 步 通 讯 来 实 现 。 ( 2?) 分 布 式 ?O?i?n? 演 算 。 ?O?i?n? 演 算 是 F?O?u?r?n?e?t? 等 人 提 出 的 一 个 “?演 算 的 异 步 化 变 种 , 它 不 仅 有 着 和 “?演 算 相 同 的 表 达 能 力 , 而 且 具 有 更 好 的 位 置 表 达 能 力 和 静 态 限 域 规 则 , 适 合 于 对 分 布 式 系 统 的 描 述 。 在 此 基 础 上 , F?O?u?r?n?e?t? 又 通 过 扩 展 显 式 的 位 置 概 念 和 移 动 原 语 , 得 到 了 分 布 式 ?O?i?n? 演 算 , 使 之 有 能 力 表 达 M?O?b?i?l?e? A?g?e?n?t? 在 物 理 站 点 之 间 的 移 动 行 为 , 并 试 图 以 此 作 为 分 布 式 编 程 语 言 的 基 础 。 其 中 , M?O?b?i?l?e? A?g?e?n?t? 用 位 置 来 表 示 , 并 利 用 树 型 结 构 的 子 位 置 描 述 了 子 A?g?e?n?t? 的 概 念 。 在 分 布 式 ?O?i?n? 演 算 中 , 异 步 消 息 与 A?g?e?n?t? 的 移 动 是 通 过 不 同 的 原 语 操 作 来 实 现 的 , 它 还 提 供 了 一 个 简 单 的 失 败 模 型 , 使 得 一 个 位 置 的 失 败 能 被 其 它 正 在 运 行 的 位 置 检 测 到 , 并 允 许 失 败 的 恢 复 过 程 。 ( 3?) D?“? !?演 算 ( 分 布 式 B?l?u?e? 演 算 ) 。 B?l?u?e? 演 算 ( “? !?) [ 2?4?] 是 一 个 结 合 了 !?演 算 特 点 的 “?演 算 异 步 扩 展 。 S?i?l?v?a?n?O? 在 此 基 础 上 又 引 入 了 位 置 、 带 有 位 置 的 进 程 以 及 代 码 传 递 的 原 语 , 得 到 了 一 个 简 单 的 B?l?u?e? 演 算 之 分 布 式 变 种 — — — D?“? !?演 9?4? 吴 泉 源 等 : 移 动 智 能 体 的 形 式 化 研 究 算 。 其 研 究 目 的 是 探 讨 并 发 对 象 的 移 动 特 性 能 否 与 对 象 的 其 它 特 性 ( 如 同 步 约 束 等 ) 相 正 交 的 定 义 。 N?i?c?O?1?a?、 F?e?r?r?a?r?i? 和 P?u?g?1?i?e?S?e? 的 K?L?A?I?M? 也 是 为 描 述 智 能 体 的 交 互 与 移 动 而 开 发 的 。 与 上 述 基 于 !?演 算 的 形 式 系 统 不 同 , 它 是 一 个 基 于 L?i?H?c?a? [ 2?5?] 的 变 种 , 可 以 看 作 一 个 异 步 、 高 阶 的 进 程 演 算 。 其 基 本 操 作 来 源 于 多 元 组 空 间 概 念 下 的 L?i?H?c?a?, 并 在 此 基 础 上 扩 展 了 显 式 的 结 点 位 置 信 息 与 一 组 借 鉴 于 C?C?S? 的 原 语 操 作 。 同 时 , K?L?A?I?M? 的 类 型 系 统 也 被 开 发 出 来 以 控 制 移 动 智 能 体 对 资 源 的 访 问 权 限 。 面 向 网 络 计 算 编 程 的 一 个 核 心 问 题 就 是 安 全 性 , 如 数 据 的 保 密 与 完 整 性 问 题 。 在 一 个 开 放 的 分 布 式 系 统 中 , 我 们 不 能 保 证 网 络 上 的 A?g?e?H?t? 都 是 善 意 的 , 因 而 防 止 恶 意 的 A?g?e?H?t? 访 问 或 修 改 私 人 数 据 便 十 分 重 要 , 接 受 移 动 A?g?e?H?t? 的 站 点 必 须 能 够 检 测 A?g?e?H?t? 的 行 为 , 以 确 保 其 不 会 对 本 地 系 统 造 成 破 坏 。 当 然 , 动 态 地 对 A?g?e?H?t? 作 身 份 鉴 别 和 权 限 控 制 可 以 达 到 目 的 , 可 是 在 分 布 式 系 统 中 试 图 每 个 资 源 的 每 次 使 用 都 进 行 动 态 的 认 证 是 很 不 可 取 的 , 这 将 大 大 降 低 系 统 的 性 能 。 因 此 , 许 多 研 究 将 安 全 问 题 集 成 到 形 式 化 系 统 中 , 通 过 类 型 系 统 的 静 态 分 析 来 直 接 推 导 安 全 方 面 的 性 质 , 保 证 对 系 统 资 源 的 安 全 访 问 。 例 如 , 有 许 多 基 于 通 道 的 分 布 式 !?演 算 类 型 系 统 [ 2?6?, 2?l?, 2?7?] 被 开 发 了 出 来 。 在 文 献 [ 2?6?] 中 , P?i?e?r?c?e? 和 S?a?H?g?i?O?r?g?i? 定 义 了 一 个 !?演 算 的 类 型 系 统 以 限 制 通 道 上 的 读 写 能 力 ; A?m?a?c?i?O? 在 文 献 [ 2?l?] 中 给 出 的 类 型 系 统 保 证 了 某 个 通 道 名 只 能 在 全 局 的 一 个 位 置 上 的 定 义 ; K?O?D?a?y?a?S?1?i? 在 文 献 [ 2?7?] 中 给 出 的 类 型 系 统 能 保 证 在 某 一 通 道 上 传 输 的 线 性 特 征 。 K?L?A?I?M? 的 类 型 系 统 [ 2?8?] 则 是 基 于 元 组 空 间 定 义 的 , 与 上 述 基 于 !?演 算 的 类 型 系 统 相 比 , 其 资 源 控 制 的 粒 度 更 大 。 !?进 一 步 的 工 作 展 望 上 述 的 形 式 系 统 都 为 移 动 智 能 体 系 统 提 供 了 不 同 程 度 的 理 论 基 础 , 总 体 的 构 造 思 想 也 大 致 相 同 , 如 均 提 供 了 显 式 的 位 置 概 念 和 A?g?e?H?t? 的 移 动 原 语 。 但 是 各 自 在 实 现 过 程 中 却 有 许 多 不 同 , 从 上 述 的 分 析 已 可 看 出 一 二 ; 各 自 的 研 究 深 度 也 参 差 不 齐 , 许 多 进 一 步 的 开 发 与 完 善 工 作 仍 需 进 行 。 以 H?e?H?H?e?S?S?y? 的 D?!?演 算 为 例 , 由 于 开 发 的 初 衷 是 为 了 提 供 一 个 分 布 式 !?演 算 的 类 型 系 统 , 以 保 证 A?g?e?H?t? 在 获 得 权 限 之 前 不 能 对 资 源 进 行 非 法 存 取 , 因 而 D?!?演 算 中 混 杂 了 许 多 与 类 型 相 关 的 概 念 与 标 识 , 增 加 了 读 者 理 解 的 难 度 。 同 时 为 了 简 化 工 作 , 它 没 有 考 虑 通 道 上 的 一 组 线 性 传 递 引 发 的 原 子 性 问 题 , 在 其 类 型 系 统 中 也 不 允 许 递 归 类 型 的 出 现 , 而 没 有 递 归 类 型 , 许 多 有 趣 的 系 统 结 构 均 无 法 描 述 , 如 涉 及 表 、 树 等 数 据 类 型 的 系 统 。 本 文 认 为 进 程 代 数 是 对 移 动 智 能 体 作 形 式 化 研 究 的 有 力 武 器 , 具 有 良 好 的 研 究 前 景 。 利 用 它 可 以 提 供 一 个 有 效 的 模 型 , 对 移 动 智 能 体 系 统 作 形 式 化 描 述 , 并 且 可 以 推 演 计 算 , 验 证 实 现 的 正 确 性 。 因 此 , 在 进 一 步 的 工 作 中 , 将 采 用 进 程 代 数 的 手 段 , 通 过 对 P?O?1?y?a?c?i?c?!?演 算 的 变 种 与 扩 充 , 得 到 一 个 异 步 ( A?S?y?H?c?1?r?O?H?i?S?m?) 、 高 阶 ( H?i?g?1?-?0?r?c?e?r?) 的 !?演 算 来 作 为 移 动 智 能 体 系 统 的 形 式 化 基 础 , 并 给 出 它 的 类 型 系 统 , 以 推 导 移 动 计 算 中 的 安 全 问 题 。 具 体 措 施 包 括 : · 异 步 化 变 种 。 移 动 智 能 体 系 统 中 计 算 实 体 的 迁 移 是 一 个 异 步 的 过 程 , 对 于 它 的 形 式 化 描 述 也 应 基 于 异 步 的 并 发 演 算 。 而 P?O?1?y?a?c?i?c?!?演 算 本 身 是 一 种 基 于 同 步 交 互 的 形 式 系 统 , 需 要 对 之 作 异 步 化 变 种 。 · 位 置 概 念 与 移 动 原 语 的 引 入 。 !?演 算 有 一 个 平 行 的 进 程 空 间 , 所 有 进 程 都 处 于 同 一 层 次 , 利 用 共 享 通 道 实 现 交 互 。 但 在 移 动 智 能 体 系 统 中 , A?g?e?H?t? 是 与 位 置 绑 定 的 , 并 能 在 位 置 之 间 作 自 主 移 动 , 通 道 也 具 有 不 同 的 作 用 范 围 。 因 此 , 需 要 引 入 位 置 的 概 念 及 显 式 的 移 动 操 作 原 语 。 · 高 阶 变 种 。 虽 然 !?演 算 有 能 力 表 述 基 本 的 高 阶 演 算 , 如 “?演 算 。 但 是 !?演 算 只 能 传 递 对 计 算 实 体 的 引 用 , 不 能 传 递 计 算 实 体 本 身 。 而 高 阶 的 进 程 演 算 能 提 供 对 在 通 道 上 传 递 活 跃 实 体 这 一 概 念 的 理 解 , 此 时 传 递 实 体 的 通 道 可 能 跨 越 不 同 的 位 置 和 安 全 界 限 。 因 此 , 有 必 要 对 !?演 算 作 高 阶 的 变 种 。 这 样 也 就 可 以 直 接 讨 论 移 动 计 算 系 统 中 的 一 些 其 他 问 题 。 例 如 , 在 整 个 计 算 实 体 移 动 时 , 如 何 处 理 标 识 的 闭 包 与 范 围 约 束 。 · 类 型 系 统 。 为 了 在 编 译 时 作 有 关 类 型 的 自 动 检 测 , 保 证 对 系 统 资 源 的 安 全 访 问 , 编 程 语 言 应 该 有 一 个 好 的 类 型 系 统 。 因 此 , 我 们 将 在 上 述 异 步 、 高 阶 !?演 算 的 基 础 上 , 引 入 一 组 类 型 ( 包 括 可 递 归 0?5? 国 防 科 技 大 学 学 报 2?0?0?0? 年 第 6? 期 类 型 ) , 及 类 型 之 间 的 相 互 关 系 , 然 后 给 出 其 类 型 系 统 , 并 讨 论 它 的 完 备 性 问 题 。 !?结 论 为 了 研 究 移 动 智 能 体 系 统 模 型 , 更 好 地 开 发 移 动 应 用 系 统 , 必 须 做 相 关 的 形 式 化 研 究 。 本 文 着 重 介 绍 了 当 前 有 代 表 性 的 研 究 成 果 , 包 括 !?d?i?s?t? 演 算 、 M?O?b?i?I?e? U?N?I?T?Y?、 分 布 式 “?演 算 等 等 。 并 分 析 了 其 中 的 不 足 , 进 一 步 给 出 了 对 后 续 工 作 的 展 望 。 希 望 能 以 此 作 为 移 动 智 能 体 形 式 化 研 究 的 基 础 。 参 考 文 献 : [ l?] H?a?r?r?i?s?O?n? C? G?, C?h?e?s?s? D? M?, K?e?r?s?h?e?n?b?a?u?m? A?.? M?O?b?i?I?e? A?g?e?n?t?s?: A?r?e? T?h?e?y? a? G?O?O?d? I?d?e?a?? [ R?] .? I?B?M? R?e?s?e?a?r?c?h? R?e?p?O?r?t?, R?C?l?9?8?8?7?, l?9?9?4?.? [ 2?] O?b?j?e?c?t?S?p?a?c?e? V?O?y?a?g?e?r?[ E?B?] .? O?b?j?e?c?t?S?p?a?c?e? I?n?c?.?, h?t?t?p?: /? /?w?w?w?.?O?b?j?e?c?t?s?p?a?c?e?.?c?O?m?/?v?O?y?a?g?e?r?/?, l?9?9?7?.? [ 3?] T?h?e? I?B?M? A?g?I?e?t?s? w?O?r?k?b?e?n?c?h?[ E?B?] .? I?B?M? C?O?r?p?.?, h?t?t?p?: /? /?w?w?w
展开阅读全文
  皮皮文库所有资源均是用户自行上传分享,仅供网友学习交流,未经上传用户书面授权,请勿作他用。
0条评论

还可以输入200字符

暂无评论,赶快抢占沙发吧。

关于本文
本文标题:移动智能体的形式化研究.pdf
链接地址:http://www.ppdoc.com/p-10938388.html
关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服客服 - 联系我们

copyright@ 2008-2018 皮皮文库网站版权所有
经营许可证编号:京ICP备12026657号-3 

收起
展开