首页/论文/1403.6563

arXiv 1403.65632014-03cs.LO

角色的完全抽象游戏语义

Fully Abstract Game Semantics for Actors

Yong Wang

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

基于参与者的代数理论和异步$π$演算的博弈语义，给出了参与者博弈语义的完全抽象证明。

英文摘要：

Based on the work on the algebraic theory of actors and game semantics for asynchronous $π$ calculus, we give the full abstraction proof of game semantics for actors.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

抽象机器对话游戏

Abstract machines for dialogue games

抽象的Boehm树的概念已经出现，作为一个面向操作的蒸馏工作的游戏语义，并已在两篇论文中进行了研究。本文重新审视了这个概念，提供了更多的语法支持和更多的例子（如按值调用评估），说明了底层计算设备的通用性。建立了抽象Boehm树评价机制的各种公式之间的精确对应关系。

2007-06-18cs.LO

游戏语义的抽象机器，再访

Abstract machines for game semantics, revisited

我们定义了新的抽象机器的游戏语义，对应于传统的计算机网络，并可以作为一个中间表示编译目标的分布式系统。这是通过两个步骤实现的。首先，我们介绍了HRAM，一个堆和寄存器抽象机，一个传统的计算机的抽象，它可以被构造成HRAM网，一个抽象的点对点网络模型。HRAM是多线程的，并且通过令牌进行子线程通信（参见或跳跃。游戏抽象机（GAM）是在接口级别具有额外结构的HRAM，但没有特殊的操作能力。我们表明，GAM不能天真地组成，但组成必须使用适当的HRAM组合子介导。HRAM足够灵活，可以表示具有状态（非无辜游戏）或并发（非交替游戏）的语言的游戏模型。我们说明了这种技术的潜力，通过实现一个玩具分布式编译器ICA，高阶程序设计语言与共享状态并发，从而显着扩展我们以前的分布式PCF编译器。我们表明，编译是健全的和内存安全的，即没有（分布式或本地）垃圾回收是必要的。

2013-04-15cs.LO

pi的全抽象并发对策

Fully-abstract concurrent games for pi

我们定义了一个语义米尔纳的π演算，有三个主要的新奇。首先，它提供了一个完全抽象的公平测试等价模型，而以前的语义涵盖了双相似性和可能和必须测试等价的变体。其次，它是基于约简语义，而以前的语义是基于标记的转换系统。最后，它具有Hyland-Ong和Nickau意义上的游戏语义色彩。事实上，我们的模型可以被视为一个无辜的预层语义和并发游戏语义。

2013-10-16cs.LO

不动点方程组的抽象、可达技术与对策

Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations

系统的不动点方程在完整的格，组成（混合）最小和最大的不动点方程，允许一个表达一些验证任务，如模型检查各种规格的逻辑或检查共归纳行为等价。在本文中，我们开发了一个理论的近似系统的不动点方程的抽象解释的风格：一个系统在一些具体的域被抽象到一个系统在一个合适的抽象域，与条件，确保抽象的解决方案代表一个声音/完全overapproximation的具体解决方案。有趣的是，最多技术，一个经典的方法，用于共归纳设置，以获得更容易或可行的证明，可以被解释为抽象的方式，他们自然适合我们的框架，并扩展到方程组。此外，依赖于近似理论，我们可以提供一个表征的解决方案的系统的不动点方程在一个合适的奇偶游戏方面的完整的格，概括了一些最近的工作，仅限于连续格。游戏的观点开辟了道路上的飞行算法的发展特点的解决方案，这样的方程系统。

2021-06-18cs.LO

谈判游戏（含摘要）

Negotiation Games (with abstract)

协商是一种以多方协商为原语的并发模型，最近在arXiv：1307.2145，arXiv：1403.4958中引入。我们开始研究这个模型的游戏。我们研究联盟的问题：可以一个给定的联盟的代理人的力量，谈判终止（分别。阻止谈判，使谈判永远进行下去）？联合部队能否确定谈判的结果？我们证明了任意协商的问题是EXPTIME完全的。然后，我们表明，声音和确定性，甚至弱确定性谈判的问题可以解决PTIME。请注意，问题的输入是一个协商，它可以比其状态空间呈指数级更紧凑。

2015-07-29cs.LO

名义通用引用的完全抽象

Full abstraction for nominal general references

游戏语义学已经在制定具有高阶过程和广泛的计算效果的语言的完全抽象语义方面取得了相当大的成功。最近，名义游戏已经提出了建模功能语言的名称。这些都是普通的，有状态的游戏投在理论的名义集开发的皮茨和Gabbay。在这里，我们采取名义游戏更进一步，通过开发一个完全抽象的语义语言与名义的一般参考。

2009-09-11cs.LOcs.PL

更多相关论文收起更多论文

战略博弈中的函数依赖（扩展摘要）

Functional Dependence in Strategic Games (extended abstract)

本文研究了多人策略对策纳什均衡中局中人策略间函数依赖的性质。主要关注的是在支付函数的固定依赖图的上下文中函数依赖的属性。提出了一个描述任意给定图的函数依赖性质的逻辑系统，并证明了该系统是完备的。

2013-03-04cs.GTcs.LO

如何既富有又快乐：结合多人游戏的定量和定性战略推理

How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)

我们提出了一个逻辑框架，结合了对多人博弈中代理人通过优化收益或结果偏好来实现定量目标的能力的博弈论研究，以及对玩家实现玩家定性目标的能力的逻辑分析，即，达到或保持具有期望属性的游戏状态。我们丰富的并发游戏模型与支付的范式游戏与模型的状态，并提出了一个定量扩展的逻辑ATL*，使定量和定性推理相结合。

2013-03-04cs.LOcs.MA

CCS中公平测试的完全抽象

Full abstraction for fair testing in CCS

在以前的工作与Pous，我们定义了一个语义CCS既可以被看作是一个无辜的预层语义和并发游戏语义。它在这里证明，行为等价诱导的CCS过程中，这种语义是完全抽象的公平测试等价。证明依赖于一个新的代数概念，称为操场，它代表了“游戏规则”。从任何操场，两种语言，配备了标记的转换系统，以及它们之间的强大的，功能互模拟。

2013-05-27cs.LO

CCS（扩展版）中公平测试的完整抽象

Full abstraction for fair testing in CCS (expanded version)

在之前与Pous的工作中，我们定义了一种用于CCS的语义，它既可以被视为预层语义的无辜形式，也可以被视为游戏语义的并发形式。我们定义在此设置中的公平测试等价的模拟，我们证明完全抽象的w.r.t.标准公平测试等价性。证明依赖于一个新的代数概念，称为操场，它代表了“游戏规则”。从任何操场，我们得到两种语言配备了标记的转换系统，以及它们之间的强大的，功能互模拟。

2014-11-02cs.LO

游戏的操作语义

Operational Semantics of Games

我们将操作语义引入到游戏中。基于操作语义，建立了一个完整的博弈代数，包括基本博弈代数、并发博弈代数、递归和抽象。在博弈论的支持下，代数可以广泛用于系统（不仅是计算系统）行为的推理。

2019-09-03cs.LO

推理主义博弈语义（扩展摘要）

Inferentialist Game Semantics (Extended Abstract)

University College London（伦敦大学学院）；Institute of Philosophy, University of London（伦敦大学哲学研究所）

该研究探讨推理主义博弈语义，利用类似技术建立基扩展语义（B - eS）与海兰德 - 翁博弈语义的完全抽象关联，并通过4x4数独示例说明语义，为逻辑系统提供了基于证明计算的内涵意义理论。

2026-07-23cs.LOmath.LO

将博弈论扩展形式规范为抽象的5元关系

Specifying a Game-Theoretic Extensive Form as an Abstract 5-ary Relation

本文提出用满足八个公理的5元关系（pentaform）来规范博弈论扩展形式，并构造了pentaform博弈与传统博弈之间的直观双射，同时探讨了其在子博弈和完美回忆等方向的应用。

2024-09-30cs.GTcs.LOecon.TH

简单的游戏语义和Day卷积

Simple game semantics and Day convolution

游戏语义为各种程序设计语言提供了足够的模型，在这些语言中，类型被解释为两个玩家的游戏，程序被解释为策略。Melliès（2018）认为，这种博弈和策略的范畴可以作为弱双范畴上的简单抽象构造的实例来获得。然而，在简单游戏的特殊情况下，他的结构与标准类别略有不同。我们完善的抽象结构使用因式分解系统，并表明，新的建设产生的标准类别的简单的游戏和策略。另一个可能令人惊讶的例子是日的卷积monoidal结构的类别preheaves超过一个严格的monoidal类别。

2018-10-16cs.LOcs.PLmath.CT

Choquet理性和模糊态度的共同信念--扩展摘要

Common Belief in Choquet Rationality and Ambiguity Attitudes -- Extended Abstract

我们考虑有限的游戏在战略形式与Choquet期望效用。使用的概念（毫不含糊地）相信，我们定义Choquet合理性和特征的Choquet合理性和共同的信念，Choquet合理性的普遍能力类型空间中的一个纯粹的可测量的设置。我们还表明，Choquet合理化相当于迭代消除严格占主导地位的行动（不是在原来的游戏，但）在一个扩展的游戏。这允许计算Choquet有理化行动，而不需要首先计算Choquet积分。Choquet期望效用允许我们研究模糊性爱/厌恶的共同信念。我们表明，模糊的爱/厌恶导致更小/更大的Choquet合理化的行动配置文件集。

2019-07-22cs.GTcs.LO

博弈语义中并行性与干扰的解耦

Disentangling Parallelism and Interference in Game Semantics

本文通过构建 IA 的因果博弈语义模型，提出并行无邪性与顺序性条件以分别排除干扰与并行性，实现四项完全抽象结果，首次将 Abramsky 语义立方体计划扩展至顺序确定性领域之外。

2024-09-17cs.LOcs.PL

计算最坏情况执行时间的时间博弈

Timed Games for Computing Worst-Case Execution-Times

在本文中，我们介绍了一个框架计算上限，但准确的WCET的硬件平台的缓存和管道。我们提出的方法包括3个步骤：1）给定一个程序来分析，计算一个等价的（WCET明智的）抽象程序; 2）通过将这个抽象程序与建模架构的时间自动机网络组成一个时间游戏; 3）计算WCET作为在这个游戏中达到获胜状态的最佳时间。我们证明了我们的框架的适用性标准基准的ARM9处理器的指令和数据缓存，并计算WCET与UPPAAL-TiGA。我们还表明，这个框架可以很容易地进行扩展，以考虑在程序执行过程中的处理器的速度的动态变化。%

2010-06-10cs.LOcs.SE