Together We Know How to Achieve: An Epistemic Logic of Know-How (Extended Abstract)
Vassar College（瓦萨学院）；Lafayette College（拉斐特学院）
达成目标的联盟战略的存在并不一定意味着联盟有足够的信息来知道如何遵循该战略。这也不意味着联合政府知道这种战略的存在。本文研究了分布式知识、联盟策略和联盟“专有技术”策略之间的相互作用。主要的技术成果是一个健全和完整的三模态逻辑系统，描述了这种相互作用的性质。
2017-07-27 cs.AI cs.LO
An Epistemic Foundation for Authentication Logics (Extended Abstract)
Cornell University（康奈尔大学）；University of New South Wales（新南威尔士大学）；Forrester Research（弗雷斯特研究公司）
虽然已经有许多尝试，回到BAN逻辑，将安全协议的推理建立在认知概念的基础上，但它们并不那么成功。可以说，这是由于选择了特定的逻辑。我们提出了一个简单的逻辑，基于知识，时间和概率的模态算子，并表明它能够处理经常被其他方法掩盖的问题，同时足够灵活，可以捕获BAN逻辑中出现的所有更高级别的安全概念。此外，虽然仍然假设知识算子允许无限计算，但它可以通过区分字符串和消息术语来处理计算受限代理无法以自然方式解密消息的事实。我们证明，我们的逻辑可以捕捉BAN逻辑概念，通过提供一个翻译的BAN运营商到我们的逻辑，捕捉信念的概率知识的形式。
2017-07-27 cs.AI cs.CR cs.LO
Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)
我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。
2016-06-24 cs.LO
Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast
知识为基础的程序提供了一个抽象的协议，其中代理人的行动是有关他们的知识状态的描述。本文介绍了如何认识模型检验技术可能会被应用到发现和验证具体的实现基于这个抽象层次的描述。实现的细节取决于协议使用的特定上下文。基于知识的方法使得实现能够相对于这些使用条件进行优化。该方法说明使用扩展的用餐密码协议，匿名广播的安全协议。
2010-04-26 cs.DC cs.LO
Common Knowledge of Abstract Groups
认知逻辑通常讨论个体代理或明确列出的代理组的知识。然而，人们往往希望表达由某一特定属性所指定的代理人群体的知识，如“这是经济学家之间的常识”。我们介绍这样一个逻辑的共同知识，我们的术语抽象组认知逻辑（AGEL）。也就是说，AGEL的特点是一个共同的知识运营商组的代理商给出的概念，在一个单独的代理逻辑，我们保持通用，与一个可能的代理逻辑是ALC。我们发现，AGEL是EXPTIME-完全的，与标准的组认知逻辑的减少建立的下限，并通过一个满足性保持嵌入到完整的$μ$ -演算的上限。进一步的主要结果包括有限的模型属性（不享有充分的$μ$ -演算）和一个完整的公理化。
2022-11-29 cs.AI cs.LO
Reasoning about Knowledge and Strategies under Hierarchical Information
两个不同的语义已被认为是知识的背景下，战略推理，这取决于球员是否知道对方的战略或没有。分布式合成的问题是已知的认知时间规范是不可判定的，后者的语义，已经在系统的层次信息。然而，对于其他的，不知情的语义，这个问题是决定这样的系统。在这项工作中，我们概括了这一结果，通过引入不完美信息的战略逻辑的认知扩展。知识算子的语义是不知情的，并捕获代理，可以改变观察力，当他们改变策略。我们解决了一类“层次实例”的模型检查问题，这提供了一个解决方案，一个巨大的类的战略问题与认知的时间规范层次系统，如分布式综合或合理的综合。
2018-09-03 cs.LO
Revisiting Epistemic Logic with Names
本文回顾了文献[10]中提出的多主体认知逻辑，其中主体和主体集合被抽象的、内涵的“名称”所取代。我们做了三个贡献。首先，我们研究了它的模型理论，提供了足够的互模拟和框架态射的概念，并使用它们来研究逻辑的表达能力和可定义性。其次，我们证明了逻辑具有自然的邻域语义，这反过来又可以证明[10]中的公理化不依赖于可能有争议的知识的内省属性。最后，我们扩展的逻辑与共同的和分布式的知识运营商，并提供了一个健全的和完整的公理化这些扩展。这些结果放在一起，把原来的认知逻辑与名称在一个更现代的背景下，并打开了一扇门的认知现象的逻辑分析组成员是不确定的或可变的。
2021-06-22 cs.LO
AbsSynthe: abstract synthesis from succinct safety specifications
在本文中，我们描述了一个综合算法的安全规格描述为电路。该算法基于不动点计算、抽象和精化，采用二元决策图作为符号数据结构。我们根据SYNT'14研讨会内组织的综合竞赛组织者提供的基准评估我们的工具。
2014-07-21 cs.LO
Abstract Learning Frameworks for Synthesis
我们开发抽象学习框架（ALFs）的综合体现了CEGIS（反例为基础的归纳合成）的战略，近年来已成为广泛适用的原则。我们的框架定义了一个通用的抽象框架的迭代学习，基于一个假设空间，捕捉合成的对象，一个样本空间，形成的空间上进行归纳，和一个概念空间，抽象地定义了语义的学习过程。我们表明，在目前的文献中的各种合成算法可以嵌入在这个一般的框架。在研究这些嵌入的同时，我们还概括了这些实例的一些合成问题，从而产生了使用学习来看待合成问题的新方法。我们还研究了收敛问题的一般框架，并展示了三个食谱收敛在有限的时间。前两个配方概括了现有合成引擎使用的收敛技术。第三种技术是一种更复杂的技术，我们知道它没有现有的实例化，我们将它实例化到具体的综合问题中。
2016-05-20 cs.LO cs.PL
Decidability and Synthesis of Abstract Inductive Invariants
在许多软件和硬件验证系统中，在给定域范围内的归纳不变量的可判定性和综合起着重要的作用。我们认为在这里归纳不变量属于一个抽象域$A$的定义在抽象的解释，即，确保存在的最佳逼近$A$的任何系统属性。在这种情况下，我们研究的可判定性存在的抽象归纳不变量的$A$的过渡系统和相应的算法合成。我们的模型依赖于一些一般性的结果，这些结果将抽象归纳不变量的存在性与过渡系统的传递函数的$A$中的最佳正确逼近的最小不动点及其完备性联系起来。这种方法使我们能够推导出可判定性和合成结果的抽象归纳不变量，适用于著名的基尔达尔的常数传播和卡尔的仿射等式抽象域。此外，我们表明，最近的一般算法合成归纳不变量域的逻辑公式，可以系统地从我们的结果和推广到一系列的算法计算抽象归纳不变量。
2020-04-09 cs.LO cs.PL
Reactive Synthesis Modulo Theories Using Abstraction Refinement
反应式合成从作为时序逻辑公式给出的规范构建系统。传统上，无功综合定义为具有布尔输入和输出变量的系统。最近，新的理论和技术已经被提出来扩展反应合成的数据域，这是需要更复杂的程序。特别是，时间流逻辑（TSL）（Finkbeiner et al. 2019）通过状态变量、更新和未解释的函数扩展了LTL，并被创建用于合成。本文给出了TSL（T）的一个综合方法，它是TSL的理论推广。使用反例引导合成循环和LTL合成程序进行合成。我们的方法翻译TSL（T）规格LTL和提取系统，如果合成成功。另外，分析了与理论不一致的对策。如果反策略是理论一致的，则证明该规范是不可实现的。否则，我们将时间假设和布尔谓词添加到TSL（T）规范中，并开始循环的下一次迭代。我们证明了TSL（T）的综合问题是不可判定的。然而，我们的方法可以成功地合成或显示几个非布尔的例子的不可实现性。
2021-07-30 cs.LO
Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs
TU Wien（维也纳工业大学）
扩展流行的答案集编程（ASP）的范式内省推理能力，在过去的几年里已经收到了越来越多的兴趣。特别注意的是给予形式主义的认识逻辑程序（ELP）的标准规则配备了模态算子，允许表达条件的文字是已知的或可能的，即，分别包含在所有或一些答案集中。因此，ELP提供了多个答案集，称为世界观。迄今为止，使用ELP进行推理问题主要限于标准决策问题（复杂性分析）和世界观的枚举（系统开发）。在本文中，我们采取了下一步，并有助于认知逻辑编程在两个方面：首先，我们建立定量推理ELP，其中接受一定的文字集取决于世界观的数量（比例）是兼容的。其次，我们提出了一个新的系统，能够有效地解决基本的计数问题，需要回答这样的定量推理问题。我们的系统利用基于图形的措施树宽和工程迭代发现和精炼（图形）抽象的ELP程序。在这些抽象之上，我们应用动态规划，结合利用现有的基于搜索的求解器，如（e）clingo的硬组合子问题，在解决过程中出现。事实证明，我们的方法与最近推出的现有系统相比具有竞争力。这项工作正在考虑接受在TPLP。
2021-08-06 cs.AI cs.CC cs.DS
Verification of agent knowledge in dynamic access control policies
我们开发了一种基于解释系统的建模技术，以验证访问控制策略的时间认知属性。这种方法使我们能够检测信息流的动态策略中的漏洞，通过验证的知识，通过阅读和推理系统信息的代理。为了克服实际的限制状态爆炸模型检查的时间认知属性，我们引入了一种新的抽象和细化技术的时间认知安全属性在ACTLK（ACTL知识模态K）和一类有趣的属性，不属于这一类。
2014-01-19 cs.CR cs.LO
Symbolic Abstract Contract Synthesis in a Rewriting Framework
我们提出了一个自动化的技术推断软件合同的程序，写在一个不平凡的片段的C，称为KernelC，支持基于指针的结构和堆操作。从K框架中KernelC的语义定义出发，我们丰富了K最近提供的符号执行设施，具有基于抽象包容的断言合成的新功能。粗略地说，我们定义了一种抽象的符号技术，通过使用同一程序中的其他（观察者）例程来解释（修改器）C函数的执行。我们在自动化工具KindSpec 2.0中实现了我们的技术，该工具通过定义C例程的精确输入/输出行为来生成表达前置和后置条件断言的逻辑公理。
2016-08-19 cs.LO cs.PL
An Abstract Look at Awareness Models and Their Dynamics
本文以觉知模态逻辑为基础，建立其与抽象论证、justification logics、knowing-what 认知逻辑和道义逻辑的联系，刻画觉知集合的若干性质并给出典范公式公理化，进而通过事件模型研究动态更新，证明闭包定理并借助归约公理公理化相应动态逻辑。
2023-07-11 cs.LO
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
我们介绍MCMAS-SLK，一个基于BDD的模型检查器的验证系统对规格表示在一个新的，认知的战略逻辑的变体。我们给出了规约语言的语法和语义，并介绍了一个标记算法的认知和策略逻辑模态。我们提供的检查器，也可以用于合成代理的策略，使系统满足规格的细节。我们评估的执行效率，通过讨论用餐密码协议和蛋糕切割问题的一个变种所获得的结果。
2014-05-16 cs.LO
Interpreting Knowledge-based Programs (Extended Version with Proofs)
知识为基础的程序指定多代理协议与认识的警卫，从代理如何学习和记录的事实或其他代理和环境的信息抽象。他们的解释涉及到一个非单调的相互依赖性之间的评价认识警卫的可达状态和推导的可达状态取决于评价认识警卫。我们申请的技术必须/不能分析发明的同步程序设计语言的解释问题的知识为基础的程序，并证明所产生的建设性的解释是单调的，有一个最小的不动点。我们将我们的方法与现有的解释计划同步和异步程序。最后，我们描述了一个建设性的解释，并说明了几个例子和应用程序的Java内存模型的过程。
2023-01-25 cs.LO cs.PL
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
自主关键系统，如卫星和空间漫游者，必须能够检测故障的发生，以确保正确的操作。此任务由故障检测和识别（FDI）组件执行，这些组件嵌入在这些系统中，并负责通过从传感器读取数据并触发预定义的警报来自动及时地检测故障。设计有效的外国直接投资成分是一个极其困难的问题，也是由于缺乏完整的理论基础，以及精确的规范和验证技术。在本文中，我们提出了第一个正式的方法来设计的FDI组件的离散事件系统，无论是在同步和异步设置。我们提出了一个逻辑语言的规范的外国直接投资的要求，占了广泛的实际案例，并包括新的方面，如最大化和跟踪诊断。该语言配备了一个明确的语义的时间认知逻辑的基础上，并被证明享有适当的属性。我们将讨论如何验证需求，以及如何验证给定的FDI组件是否满足这些需求。我们提出了一种算法，正确的建设FDI组件的合成，并报告的适用性的设计方法的工业案例研究来自航空航天。
2016-02-10 cs.LO
Controller Synthesis for Safety and Reachability via Approximate Bisimulation
Laboratoire Jean Kuntzmann Universit\'e de Grenoble B.P. 53, 38041 Grenoble, France
本文利用近似双模拟抽象方法，针对安全性和可达性规范设计控制器，通过抽象控制器综合与具体化过程保证正确性，并给出与最优控制器的距离估计。
2011-06-16 cs.LO cs.SY eess.SY
Full LTL Synthesis over Infinite-state Arenas
University of Gothenburg（哥德堡大学）；Chalmers University of Technology（查尔姆斯理工大学）；TU Wien（维也纳工业大学）；Dedaub
本研究提出了一种基于布尔抽象的完整LTL目标合成方法，通过CEGAR方法提升无限状态竞技场中的合成效率，优于现有最先进方法。
2025-05-27 cs.FL cs.LO cs.PL
Feedback Refinement Relations for the Synthesis of Symbolic Controllers
University of the Federal Armed Forces Munich（联邦国防军大学）；Technical University of Munich（慕尼黑工业大学）
本文提出了一种抽象和细化方法，用于自动控制器合成以满足通用预定义规范。控制器仅需量化状态信息，通过静态量化器与系统接口，并通过反馈细化关系确保鲁棒性和可证明性。
2017-01-02 cs.LO cs.SY eess.SY
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）；CIFASIS
该研究提出首个针对LTLt的完整静态反应式综合方法，结合布尔抽象与函数综合生成确定性控制器，兼具可预测性、高效性及输出优化能力。
2024-07-12 cs.AI cs.LO cs.SE
sweap: Reactive Synthesis for Infinite-State Integer Problems
Dedaub；TU Wien, Institute of Computer Engineering（维也纳工业大学计算机工程研究所）；University of Gothenburg and Chalmers University of Technology（哥德堡大学与查尔姆斯理工大学）
sweap通过CEGAR方法实现无限状态线性整数算术反应系统合成，支持多种输入形式，具备新型双抽象方法和优化技术，实验表明其性能优于竞争对手。
2026-05-12 cs.FL cs.LO cs.SY
Consistent Update Synthesis via Privatized Beliefs
针对 DEL 全模型更新导致私有通信泄露及局部状态损坏的问题，本文提出私有化智能体簇的动作模型综合方法和点态更新操作，以实现目标公式、信念一致与模型精简。
2024-06-14 cs.LO math.LO
Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints
RWTH Aachen University（亚琛工业大学）
在实际机器人上执行Golog程序通常需要额外的步骤来考虑机器人平台的硬件或软件细节，这些细节可以被公式化为对程序的约束。这些约束通常是时间性的，指的是度量时间，并且需要对抽象Golog程序进行修改。我们描述了如何制定这样的约束的基础上的模态变量的情况演算。这些约束连接抽象程序与平台模型，我们使用时间自动机描述。我们表明，在有限域和完全已知的初始状态的程序，合成的控制器，满足约束，同时保持原程序的效果的问题可以减少到MTL合成。我们这样做是通过构建一个时间自动机的抽象程序和合成MTL控制器从这个自动机，平台模型和约束。我们证明，合成的控制器的执行轨迹是相同的原始程序，可能交错与平台相关的行动，他们满足所有的约束条件，并且它们具有相同的效果作为原始程序的痕迹。通过这样做，我们得到一个可判定的过程来合成一个控制器，满足规格，同时保留原始程序。
2021-02-19 cs.AI cs.LO
