博文
Game Semantics linear logic
||
Contents
1 任务逻辑
[1]
2 Game Semantics
[1] Applying Game Semantics to Compositional Software Modeling and Verification
[2] IN THE BEGINNING WAS GAME SEMANTICS
3 Linear logic
[1-]
1 任务逻辑
面向交互的主体能力描述和推理方法研究
张会 李思昆
计算机研究与发展 43( 8) : 1439~ 1444, 2006
摘要
主体间的交互对主体能力的影响是主体能力描述和推理需要考虑的一个重要因素。 给出了一个面向交互的主体能力描述和推理框架， 该框架将描述逻辑中的知识表示结构和任务逻辑中的任务语义结合起来, 可以显式地描述主体之间的交互关系对主体能力的影响并可提供可判定的推理服务, 建立了一个用于任务可完成性判定的逻辑系统DTL, 并证明了它是可靠、完备和可判定的.
关键词 主体; 能力描述; 任务语义; 描述逻辑
the aim of this paper: 研究如何在主体能力描述和推理过程中显式表示主体之间任务交互关系及其对主体能力影响?
线性逻辑: 搏弈?
任务逻辑: Japaridze
1 面向交互的主体能力描述框架
1.1 语法结构
1.2 语义结构
2 任务的可完成性的判定
2.1 简单任务的可完成性的判定方法
2.2 一般任务的可完成性判定
描述任务逻辑及其应用
张 会 李思昆
摘要
针对任务逻辑存在的两个缺点: ( 1) 不可判定, 无法保证推理过程都能在有限的时间内结束; ( 2) 任务的定义局限于抽象的、逻辑的定义, 无法描述任务的具体属性和任务之间的关系, 将描述性结构引入任务逻辑, 构造了一个可描述具体属性的、可判定的任务逻辑系统) ) ) 描述任务逻辑. 将所构造的逻辑系统应用于具有组织的多主体系统行为建模, 建立了基于描述任务逻辑的多主体组织模型和建模框架, 并且表明应用描述任务逻辑构造应用系统具有表达能力强、结构紧凑的特点.
关键词 任务逻辑; 可判定; 描述语言; 多主体系统; 组织模型
1 引言
描述交互理论: 计算逻辑、进程代数、线性逻辑和任务逻辑.
2 描述任务逻辑
2.1 描述任务逻辑的语法
2.2 描述任务逻辑的语义
2. 3 描述任务逻辑的语构理论
3 基于任务逻辑的多主体组织模型和建模框架
3. 1 基于任务逻辑的多主体组织模型
基于任务逻辑的组织模型如图1 所示
2 Game Semantics
[1-]
Abstract
11.1 Introduction
Applying Game Semantics to Compositional Software Modeling and Verification
Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, and C.-H. Luke Ong
TACAS 2004, LNCS 2988, pp. 421–435, 2004.
Abstract.
We describe a software model checking tool founded on game semantics, highlight the underpinning theoretical results and discuss several case studies. The tool is based on an interpretation algorithm defined compositionally on syntax and thus can also handle open programs. Moreover, the models it produces are equationally fully abstract. These features are essential in the modeling and verification of software components such as modules and turn out to lead to very compact models of programs.
1 Introduction and Background
Game Semantics
several features of Game Semantics:
--
Model checking for state machines
2 A Procedural Programming Language
2.1 Extended Regular Expressions
2.2 Alphabets
2.3 Regular-Language Semantics
2.4 A Warm-up Example
2.5 Full Abstraction
3 Applications to Analysis and Verification
3.1 Tool Support and Case Studies
3.2 Sorting
3.3 ADT Invariants
4 Limitations and Further Research
[2] IN THE BEGINNING WAS GAME SEMANTICS
Giorgi Japaridze
Department of Computing Sciences, Villanova University
giorgi.japaridze@villanova.edu
Department of Computing Sciences, Villanova University
giorgi.japaridze@villanova.edu
Games: Unifying Logic, Language, and Philosophy, 249
Logic, Epistemology, and the Unity of Science 15,
© Springer Science+Business Media B.V. 2009
Logic, Epistemology, and the Unity of Science 15,
© Springer Science+Business Media B.V. 2009
Abstract
This chapter presents an overview of computability logic—the game-semantically
constructed logic of interactive computational tasks and resources. There
is only one non-overview, technical section in it, devoted to a proof of the soundness
of affine logic with respect to the semantics of computability logic.
constructed logic of interactive computational tasks and resources. There
is only one non-overview, technical section in it, devoted to a proof of the soundness
of affine logic with respect to the semantics of computability logic.
11.1 Introduction
3 linear logic
[1-] 线性逻辑、Petri网和并发计算
[2-] 线性逻辑导论
[3-] 一种基于线性逻辑的Petri网分析方法
[4-] Linear logic
Alex Wright
Oct 2010 | vol . 53 | no. 10 | communications of the acm
remark: A novel approach to computational logic is reaching maturity, opening up new vistas in programming languages, proof nets, and security applications.
Jean-Yves Girard: Linear Logic
1 Proof Nets
big-step inference rules vs. small-step inference rules
remark: Active research areas for linear logic include concurrency theory, quantum computing,
game semantics, and implicit computational complexity.
https://blog.sciencenet.cn/blog-468147-432754.html
上一篇：软件工程和分布式计算
下一篇：SOC SOA Web服务
扫一扫，分享此博文