Parameter Synthesis for Markov Models: Faster Than Ever
我们提出了一个简单的技术来验证概率模型的转移概率是参数。关键是用极值的非确定性选择来代替参数转换。使用现成的平均值分析所得到的无参数模型产生参数空间中区域概率的（可细化的）下限和上限。该技术优于现有的分析参数马尔可夫链的几个数量级的运行时间和可扩展性。它的美妙之处在于它适用于各种概率模型。它特别提供了第一个健全的和可行的方法进行参数综合的马尔可夫决策过程。
2016-05-26 cs.LO
An Efficient Formula Synthesis Method with Past Signal Temporal Logic
在这项工作中，我们提出了一种新的方法来找到时间属性，导致意想不到的行为标记数据集。我们表示这些属性在过去的时间信号时序逻辑（ptSTL）。首先，我们提出了一种新的方法来寻找模板ptSTL公式的参数，扩展了单调性为基础的参数合成的结果。所提出的方法优化了一个给定的单调准则，同时限制了错误。然后，我们采用的参数综合方法在迭代无指导公式综合框架。特别是，我们结合优化的公式迭代地描述标记的事件的原因，而边界的错误。我们说明了两个例子的建议框架。
2019-04-16 cs.LO
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
带抑制弧的参数时间Petri网（PITPN）允许参数在触发范围内，从而支持时间系统的灵活性。本文提出并证明了PITPN的一种具体的和符号化的重写逻辑语义。我们将展示如何使用Maude结合SMT解决方案，为PITPN提供完善的正式分析。我们开发了一个新的通用折叠符号可达性的方法，终止时的参数状态类图的PITPN是有限的。我们解释了几乎所有的形式分析和参数合成支持的国家的最先进的PITPN工具Roméo可以在Maude与SMT。此外，我们还支持从参数化初始标记进行分析和参数合成，以及使用用户定义的执行策略进行完整的LTL模型检验和分析。在三个基准上的实验表明，我们的方法在许多情况下优于Roméo。
2023-03-15 cs.LO
Parameterized Infinite-State Reactive Synthesis
该研究提出一种反例引导的参数化无限状态系统综合方法，结合反合一与语法引导综合实现程序泛化与证明构造，经扩展文献示例与新问题验证了方法的有效性。
2025-08-01 cs.LO
Parameter Synthesis in Markov Models: A Gentle Survey
本文综述了参数马尔可夫模型的分析，其转移标记的功能在一个有限的参数集。这些模型是无数具体概率模型的符号表示，每个模型都是通过实例化参数获得的。我们考虑给定逻辑规范$φ$的各种分析问题：给定参数值区域内的所有参数实例是否满足$φ$？哪些实例化满足$φ$，哪些不满足？以及如何准确或近似地描述所有这些实例？我们解决了理论复杂性结果，并描述了最先进算法的主要思想，这些算法在过去十年中实现了令人印象深刻的飞跃，使具有数百万个状态和数千个参数的模型能够完全自动化分析。
2022-07-14 cs.LO
Parametric Systems: Verification and Synthesis
在本文中，我们研究的可能性，使用层次推理，符号消除和模型生成的参数系统的验证，其中参数可以是常数或函数。我们的目标是自动提供保证，这样的系统满足一定的安全性或不变性条件。我们分析的可能性，自动生成这样的保证，在参数的约束的形式。我们用几个例子来说明我们的方法
2019-10-11 cs.LO
Minimal-Time Synthesis for Parametric Timed Automata
参数时间自动机（PTA）通过允许时钟约束中的参数来扩展时间自动机。这样的形式主义是有用的，例如推理时，在一个定时系统中的未知延迟。使用现有技术，用户可以合成允许系统到达指定目标位置的参数约束，而不管内部时钟已经过去了多少时间。我们专注于综合参数，不仅达到目标位置，但我们也解决了以下问题：什么是最短的时间到达目标位置？对于哪些参数值，我们可以实现这一点？我们分析了这个问题，并提出了一个算法来解决它。我们还讨论了最小化一个特定的参数值，仍然达到目标，并提供解决方案。我们实证研究这些算法的性能在一个基准集的PTA和最小时间可达性合成是更有效的计算比标准的合成算法的可达性。
2019-02-08 cs.LO
Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
Université Sorbonne Paris Nord（索邦巴黎北大学）；Institut Universitaire de France (IUF)（法国大学研究院）；Nantes Université, École Centrale Nantes, CNRS, LS2N（南特大学，中央理工-南特学院，法国国家科学研究中心，LS2N）
本文提出了一种参数外推方法，用于在有界参数域内合成参数估值集，确保可达性和无避免性，同时保持与参考估值的无时行为。
2026-04-27 cs.LO
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
LIPN CNRS UMR 7030 Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心联合研究实验室）；Pohang University of Science and Technology（韩国科学技术院）；University of Oslo（奥斯陆大学）
本文提出了一种用于参数时间Petri网的形式化分析与参数综合框架，利用重写逻辑与SMT求解器实现精确语义分析，通过符号可达性方法实现参数综合，实验表明方法在多个方面优于现有工具。
2024-09-12 cs.LO
Proceedings Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters
本卷包含复杂系统合成游戏研讨会（CASSING '16）和第三届复杂参数合成国际研讨会（SynCoP'16）的联合会议记录。研讨会在荷兰埃因霍温举行，作为第19届欧洲软件理论与实践联合会议（ETAPS'16）的附属活动。这两个研讨会在主题和目标受众方面密切相关，他们分享了Giorgio Delzanno的联合邀请演讲。
2016-07-31 cs.LO cs.SE
LTL Parameter Synthesis of Parametric Timed Automata
参数时间自动机的参数综合问题是不可判定的，即使是非常简单的可达性。在本文中，我们引入了参数估值的限制下，参数综合问题是可判定的LTL性能。所研究的有界整数参数综合问题可以使用所有可能的参数赋值的显式枚举来解决。我们提出了一种替代的符号区域为基础的方法，这个问题的结果在一个更快的计算。我们的技术扩展了基于自动机的LTL模型检验的时间自动机的方法的思想。为了证明我们的方法的有用性，我们提供了实验评估和比较我们的方法与显式枚举技术。
2016-03-04 cs.FL cs.LO
Distributed Synthesis for Parameterized Temporal Logics
我们认为，在参数化的时间逻辑，如PROMPT-LTL，它扩展LTL的时间运营商配备了参数，约束其范围的规范的分布式实现的合成。对于单过程综合，这是公认的，这样的参数扩展不会增加最坏情况下的复杂性。对于同步分布式系统，我们表明，尽管是更强大的，PROMPT-LTL的可实现性问题并不比它的LTL对应。对于异步系统，我们必须表达调度假设，因此考虑一个假设保证合成问题。由于异步分布式综合对于LTL已经是不可判定的，我们给出了基于有界综合的PROMPT-LTL假设保证综合问题的半判定过程。最后，我们证明了我们的结果扩展到更强的逻辑PLTL和PLDL。
2018-02-26 cs.GT cs.LO
Parameterized Synthesis with Safety Properties
参数化综合为参数化系统构造正确的、可验证的控制器提供了一种解决方法。这种系统在实践中自然发生（例如，以分布式协议的形式，其中进程的数量在设计时通常是未知的，并且协议必须工作而不管进程的数量）。在本文中，我们提出了一种新的学习为基础的方法来综合反应控制器的参数化系统的安全规格。我们使用的框架，定期模型检验建模的合成问题作为一个无限持续时间的两个玩家的游戏，并显示如何可以利用Angluin的著名的L* 算法学习正确的设计控制器。这种方法的结果是在一个合成过程中，概念上比现有的合成方法更简单的完整性保证，只要一个获胜的策略可以表示为一个正规的集合。我们已经实现了我们的算法在一个工具，称为L*-PSynth，并已证明其性能的基准范围内，包括机器人运动规划和分布式协议。尽管L*-PSynth很简单，但它与用于合成参数化系统的最先进的工具竞争得很好（在许多情况下甚至优于）。
2020-09-28 cs.FL cs.LO
Revisiting Parameter Synthesis for One-Counter Automata
研究了带参数的单计数器自动机的参数综合问题。单计数器自动机是将经典的有限状态自动机扩展为一个计数器，该计数器的值可以在非负整数范围内变化，并且可以测试为零。通过引入一组称为参数的整数值变量，可以进一步使适用于计数器的更新和测试参数化。这样的自动机的合成问题问是否存在一个参数的估值，使所有的无限运行的自动机满足一些欧米茄正则性质。Lechner证明了这个问题（的补充）可以被编码在具有可除性的Presburger算术的一个受限的交替片段中。在这项工作中（i），我们认为，所说的片段，称为AERPADPLUS，不幸的是不可判定的。然而，通过仔细重新编码的问题到一个可判定的限制AERPADPLUS，（ii）我们证明了合成问题是可判定的一般和N2 EXP的几个固定的Ω-经常性。最后，（iii）我们给出了一个多项式空间算法的特殊情况下的问题，参数只能用于测试，而不是更新，计数器。
2021-10-19 cs.FL cs.LO
On Reduction and Synthesis of Petri's Cycloids
University of Hamburg（汉堡大学）
本文提出了一种基于彼得里网结构的环形线参数综合方法，用于高效判断环形线同构性。
2026-08-18 cs.DC cs.LO
On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency (Technical Report)
$τ$ -合成问题在于判定给定的有向标记图$A$是否同构于$τ$型布尔Petri网$N$的可达图。在肯定决策的情况下，应构建$N$。对于许多布尔类型的网，问题是NP完全的。本文论述了一个特殊的变形$τ$ -合成的目标净$N$施加限制：我们调查\emph{dependency $d$-restricted $τ$-synthesis (DR$τ$S)}的每个地方的$N$可以影响和最多的$d$过渡的影响。对于类型$τ$，如果$τ$ -合成是NP完全的，则DR $τ$ S也是NP完全的。在本文中，我们表明，由$d$参数化的DR $τ$ S在XP中。此外，我们证明了它是$W[2]$ -硬，对于许多布尔类型，允许无条件的相互作用$set$和$reset$。
2020-07-24 cs.CC cs.LO
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions
系统生物学中的一个中心问题是确定参数值，使得生物模型满足某些行为约束（\eg，时间序列）。在本文中，我们专注于混合（连续/离散）模型的参数合成，因为许多生物系统可以拥有多个操作模式，在每个模式中具有特定的连续动态。这些生物系统自然地被建模为混合自动机，通常具有非线性连续动力学。然而，混合自动机是出了名的难以分析-即使是简单的可达性混合系统的线性微分动力学是一个不可判定的问题。在本文中，我们提出了一个参数综合框架的基础上$δ$ -完全决策过程，回避不可判定性。我们证明了我们的方法对两个高度非线性混合模型的心脏细胞动作电位。结果表明，我们的参数合成框架是方便和有效的，它使我们能够选择一个合适的模型来研究和确定与心脏疾病相关的关键参数范围。
2014-09-10 cs.CE cs.LO q-bio.QM
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Distributed PROMPT-LTL Synthesis
我们认为，在提示线性时序逻辑（PROMPT-LTL），它扩展了LTL的时间运营商配备了参数，约束其范围的规范的分布式实现的合成。对于单过程综合，这是公认的，这样的参数扩展不会增加最坏情况下的复杂性。对于同步系统，我们表明，尽管是更强大的，分布式的可实现性问题的PROMPT-LTL并不比它的LTL对应。对于异步系统，我们必须考虑一个假设保证合成问题，因为我们必须表达调度假设。由于异步分布式综合对于LTL已经是不可判定的，我们给出了基于有界综合的PROMPT-LTL假设保证综合问题的半判定过程。
2016-09-14 cs.GT cs.LO
Convex Optimization for Parameter Synthesis in MDPs
Radboud University Nijmegen（拉德堡德大学（奈梅亨））；University of California at Berkeley（加州大学伯克利分校）；RWTH Aachen University（亚琛工业大学）
概率模型检验的目的是证明马尔可夫决策过程是否满足时态逻辑规范。基本方法依赖于一个通常不切实际的假设，即MDP是精确已知的。因此，参数MDP（pMDP）扩展MDP的转移概率，是在未指定的参数的函数。参数合成问题是计算这些未指定参数的实例化，使得所得MDP满足时态逻辑规范。我们制定的参数综合问题作为一个二次约束二次规划（QCQP），这是非凸的，是NP-难解决的一般。我们开发了两种方法，迭代获得局部最优解。第一种方法利用所谓的凸-凹过程（CCP），第二种方法利用顺序凸规划（SCP）方法。通过融合凸优化和概率模型检测的思想，与黑盒CCP和SCP相比，该技术将运行时间和可扩展性提高了多个数量级。我们展示了卫星防撞问题的方法，数十万个国家和数万个参数和它们的可扩展性在广泛的常用基准。
2021-06-30 cs.AI cs.LO math.OC
Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
RWTH Aachen University（亚琛工业大学）；Radboud University（拉德堡德大学）；Albert-Ludwigs-Universität Freiburg（弗赖堡大学）
研究了部分可观测马尔可夫决策过程中的宽容有限状态控制器，通过参数综合法实现正确性保证，实验表明性能与知名POMDP求解器相当。
2018-07-17 cs.LO cs.SY eess.SY
Parameter Synthesis Problems for one parametric clock Timed Automata
RISE, Southwest University（西南大学 RISE）；Department of Computer Science and Informatioin Systems, Birkbeck, University of London（伦敦大学伯贝克学院计算机科学与信息系统系）；LMAM & School of Mathematical Sciences, Peking University（北京大学数学科学学院 LMAM）；State Key Laboratory of Computer Science, Institute of Software, CAS（中国科学院软件研究所 计算机科学国家重点实验室）；CISS, CS, Aalborg University（奥尔堡大学计算机科学与工程系 CISS）
本文研究了一类参数时钟时序自动机的参数合成问题，通过线性表达式和参数多项式不等式约束，确定参数估值的可行区域以满足特定属性。
2018-09-15 cs.FL cs.LO cs.SY
Parameter Synthesis for Markov Models: Covering the Parameter Space
针对马尔可夫模型概率参数未知的问题，提出参数化离散时间马尔可夫链与马尔可夫决策过程的三类分析算法，实现对应工具并通过多领域基准完成广泛实验评估。
2023-11-07 cs.LO cs.SY eess.SY
