Multi-weighted Markov Decision Processes with Reachability Objectives
在本文中，我们感兴趣的是在双加权马尔可夫决策过程中，它既满足百分位数约束的加权可达性条件，并使用加权可达性条件定义的随机变量的期望值的定量约束的合成。这个问题的灵感来自电动汽车充电问题的模型化。我们研究的问题的制图，当一个参数变化，并显示如何部分制图可以通过两个序列的优化问题。讨论了该方法的完备性和可行性。
2018-09-10 cs.LO
Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives
我们认为马尔可夫决策过程（MDP）与$ω$ -定期规格作为奇偶校验的目标。我们考虑的问题，计算的一组几乎肯定获胜的顶点，从那里可以确保目标的概率为1。用于计算奇偶目标的几乎确定获胜集的算法迭代地使用Büchi目标（奇偶目标的特殊情况）的几乎确定获胜集的解。我们首次研究了经典算法的平均情况下的复杂性计算几乎肯定获胜的顶点MDP Büchi目标。我们的贡献如下：首先，我们表明，对于恒定的出度的MDP的预期迭代次数是最多对数和平均情况下的运行时间是线性的（相比最坏情况下的线性迭代次数和二次时间复杂度）。其次，我们表明，一般MDPs的预期迭代次数是恒定的，平均情况下的运行时间是线性的（再次相比，最坏情况下的线性迭代次数和二次时间复杂度）。最后，我们还表明，给定所有的图是同样可能的，经典算法需要超过常数的迭代次数的概率是指数小。
2014-11-19 cs.LO
Qualitative Analysis of Partially-observable Markov Decision Processes
我们研究了部分可观测马尔可夫决策过程（POMDPs）与欧米茄定期目标的观察为基础的战略。基于观察的策略依赖于关于游戏历史的部分信息，即过去的观察序列。我们考虑的定性分析问题：给定一个POMDP与一个欧米伽正则目标，是否有一个基于观察的策略，以达到目标的概率约1（几乎肯定获胜），或与积极的概率（积极获胜）。我们的主要结果是双重的。首先，我们提出了一个完整的图片的计算复杂性的定性分析POMDP的奇偶性目标（一个规范形式来表达ω-经常目标）及其子类。我们的贡献在于建立了几个在文献中不为人知的上限和下限。其次，我们提出了最佳的界限（匹配的上限和下限）的内存所需的纯随机观察为基础的策略，POMDP的奇偶校验目标及其子类的定性分析。
2010-06-09 cs.LO
Multi-objective Optimization of Long-run Average and Total Rewards
本文提出了一种有效的多目标模型检验的长期平均回报（又名：平均支付）和总回报目标，以及它们的组合。我们认为这是马尔可夫自动机，一个组成模型，捕捉传统的马尔可夫决策过程（MDP），以及其连续时间的变体。我们的程序的关键是一个概括的Forejt等人。的方法的总回报MDP的长期和总回报目标的马尔可夫自动机的任意组合。在Storm模型检查器上进行原型实现的实验表明，这两种模型类型的结果都令人鼓舞，并表明基于线性规划的现有多目标长期MDP模型检验的性能得到了大幅提高。
2021-01-07 cs.LO
Multi-Objective Model Checking of Markov Decision Processes
研究并给出了马尔可夫决策过程多目标模型检验问题的有效算法。给定MDP，M，以及给定多个线性时间（ω-正则或LTL）性质φ i，以及概率ri ε[0，1]，i=1，.，k，我们问是否存在控制器的策略σ，使得对于所有i，由σ控制的M的轨迹满足φ i的概率至少为ri。我们提供了一个算法，决定是否存在这样的策略，如果是这样产生它，并运行在时间多项式中的MDP的大小。这种策略可能需要同时使用随机化和内存。我们还考虑了更一般的多目标ω-正则查询，我们激励与应用的假设保证组合推理的概率系统。注意，在不同属性之间可以存在折衷：以高概率满足属性φ 1可能需要以低概率满足φ 2。将其视为多目标优化问题，我们需要关于“权衡曲线”或帕累托曲线的信息，以最大化不同属性的概率。我们证明了在MDP的大小下，可以计算关于时间多项式中的一组ω-正则性质的近似Pareto曲线。我们的定量上限使用LP方法。我们还研究了定性的多目标模型检验问题，我们表明，这些可以通过纯粹的图论方法进行分析，即使策略可能仍然需要随机化和内存。
2008-11-11 cs.CC cs.GT cs.LO
Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
针对马尔可夫决策过程中多目标ω-正则查询，提出独立可验证的证书与证据，扩展改进现有证书推导MILPs找最小见证子系统，特例下用无歧义Büchi自动机获单指数空间算法，实现并验证技术有效性。
2025-08-25 cs.LO
Strategy Complexity of Parity Objectives in Countable MDPs
我们研究可数无限MDP奇偶目标。与有限MDP不同，最优策略不需要存在，如果存在，可能需要无限内存。我们提供了一个完整的图片的确切的策略复杂性的$\varepsilon$ -最优策略（和最优策略，如果它们存在）的所有子类的奇偶校验目标的Mostowski层次结构。根据颜色的数量、MDP的分支度以及是否考虑$\varepsilon$ -最优或最优策略，MD策略、马尔可夫策略或1位马尔可夫策略都是必要且充分的。特别地，1比特马尔可夫策略对于$\varepsilon$ -最优（分别为：最优）策略。
2020-07-07 cs.LO
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
我们考虑马尔可夫决策过程（MDP）与多个极限平均（或平均值支付）的目标。存在两种不同的观点：（i）期望语义，其目标是优化预期的平均收益目标，以及（ii）满意语义，其目标是最大化运行的概率，使得平均收益值保持在给定向量之上。我们考虑优化这两个目标，从而统一现有的语义。准确地说，目标是在确保满足约束的同时优化期望。我们的问题抓住了关于风险规避策略的优化概念（即，保证一定概率）。我们的主要结果如下：首先，我们提出的算法的决策问题，总是多项式的大小MDP。我们还表明，近似的帕累托曲线可以计算在时间多项式的大小的MDP，和近似因子，但指数的维数。其次，我们提出了一个完整的表征的策略复杂性（在内存边界和随机化），需要解决我们的问题。
2017-06-29 cs.LO
Analysis of Timed and Long-Run Objectives for Markov Automata
马尔可夫自动机（MA）扩展了具有随机延迟和概率分支的标记转移系统。标记转换是瞬时的，并产生一个分布状态，而定时转换施加一个随机延迟由指数分布。因此，MA是连续时间马尔可夫链的非确定性变化。MA是组合的，用于为工程框架提供语义，如（动态）故障树，（广义）随机Petri网和架构分析与设计语言（AADL）。本文对并购进行了定量分析。我们考虑三个目标：预期时间，长期平均值和定时（间隔）可达性。预期时间目标集中于确定到达一组状态的最小（或最大）预期时间。长期目标决定了在考虑无限时间范围时处于一组状态的时间比例。定时可达性目标是关于计算在给定时间间隔内到达一组状态的概率。本文介绍了算法的基础和细节及其正确性证明。我们报告的几个案例研究进行了使用原型工具实现的算法，驱动的MAPA建模语言有效地生成MA。
2014-09-09 cs.FL cs.LO
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
本文研究Markov决策过程中多目标可达性、不变性与平均收益查询的可验证性，将线性规划方法改造为认证算法，并生成调度器和子系统见证。
2025-01-10 cs.LO
Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes
University of Antwerp（安特卫普大学）
在本文中，我们考虑的算法，以确定存在的MDP的目标的布尔组合的战略。这些目标是Ω正则性质，需要强制执行，或者肯定，几乎肯定，存在，或非零概率。在这种情况下，相关的策略是随机无限记忆策略：无限记忆和随机化都可能需要最佳发挥。我们提供的算法来解决一般情况下的布尔组合，我们也调查相关的子情况。我们进一步报告这些问题的复杂性界限。
2020-04-28 cs.AI cs.FL cs.GT
Distribution-based objectives for Markov Decision Processes
我们考虑马尔可夫决策过程（MDP）的基于分布的目标。这类目标在全部信息和部分信息之间产生了一个有趣的权衡。与完全观察一样，MDP中的策略可以依赖于系统的状态，但与部分信息类似，策略需要同时考虑所有状态。在本文中，我们专注于两个安全问题，自然出现在这种情况下，即存在和普遍的安全。给定一个MDP A和一个A状态上概率分布的闭凸多面体H，存在安全问题询问H中是否存在某种分布d和A的策略，使得从d开始并重复应用该策略，该分布永远保持在H中。普适安全问题问的是，对于H中的所有分布，是否存在这样一种策略A，使该分布永远保持在H中。我们证明了这两个问题都是可判定的，具有严格的复杂性界限：我们证明了存在安全是PTIME完全的，而普遍安全是co-NP完全的。此外，我们将这些结果与拉宾的概率有限状态自动机（PFA）的存在性和普遍的安全问题进行比较，PFA是部分可观测MDP的子类，具有零观测。与MDPs相比，PFAs的策略不依赖于状态。与PTIME结果形成鲜明对比的是，我们发现PFAs的存在安全性是不可判定的，H具有封闭和开放的边界。另一方面，证明了PFAs的普遍安全性在EXPTIME中是可判定的，具有co-NP下界。最后，我们表明，输入多面体的替代表示使我们能够提高MDP和PFAs的通用安全性的复杂性。
2018-04-25 cs.CC cs.DM cs.LO
Percentile Queries in Multi-Dimensional Markov Decision Processes
具有多维权重的马尔可夫决策过程（MDP）可用于分析具有多个目标的系统，这些目标可能是冲突的，并且需要进行权衡分析。我们研究了百分位查询在这样的MDP的复杂性，并给出算法来合成策略，执行这样的约束。给定一个多维加权MDP和一个定量回报函数$f$，阈值$v_i$（每维一个）和概率阈值$α_i$，我们展示了如何计算一个单一的策略来执行，对于所有维度$i$，结果$ρ$满足$f_i(ρ) \geq v_i$的概率至少是$α_i$。我们考虑经典的定量回报从文献（sup，inf，lim sup，lim inf，平均回报，截断和，贴现和）。我们的工作扩展到定量的情况下，多目标模型检验问题研究Etessami等人。在未加权MDPs。
2016-12-07 cs.LO
Life is Random, Time is Not: Markov Decision Processes with Window Objectives
UMONS — Université de Mons（蒙斯大学）；RWTH Aachen（亚琛工业大学）；F.R.S.-FNRS（比利时科学研究基金会）；LACL — UPEC（巴黎东马恩河谷大学逻辑、算法与复杂性实验室）
本研究将窗口目标扩展到马尔可夫决策过程，解决阈值概率问题，提出通用方法并应用于均值支付和对偶目标，为随机模型中的窗口机制应用奠定基础。
2020-12-10 cs.AI cs.FL cs.GT
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
我们提出了条件风险价值（CVaR）的背景下，马尔可夫链和马尔可夫决策过程的可达性和平均收益的目标。CVaR通过对最差p分位数的期望来量化风险。因此，它可以用来设计风险规避系统。我们不仅考虑CVaR约束，而且还介绍了他们与期望约束和分位数约束（风险价值，VaR）。我们推导出各自的决策问题的计算复杂性上下限和上界，并描述了内存和随机化的策略结构。
2018-05-08 cs.LO
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes
ENS Rennes（雷恩高等师范学院）；ULB - Université libre de Bruxelles（布鲁塞尔自由大学）
Bruyère等人最近引入了超越最坏情况综合问题。[BFRR 14]：它旨在构建系统控制器，该控制器针对对抗性环境提供严格的最坏情况性能保证，同时确保针对环境的随机模型的更高预期性能。我们的工作扩展了[BFRR 14]和后续论文的框架，这些论文专注于定量目标，通过解决$ω$的情况-编码为奇偶目标的正则条件，一种自然的方式来表示系统的功能需求。我们建立的策略，满足所有播放的主要平价目标，同时确保有足够的概率次要的。与定量目标相比，这种设置提出了新的挑战，因为人们无法在不危及系统功能特性的情况下轻松混合不同的策略。我们建立，对于这个问题的所有变体，决定存在的战略在于${\sf NP} \cap {\sf coNP}$，相同的复杂性类的经典奇偶游戏。因此，我们的框架提供了额外的建模能力，同时保持在相同的复杂性类。[BFRR 14] Véronique Bruyère，Emmanuel Filiot，Mickael Randour和Jean-François Raskin。保证满足您的期望：超越量化游戏中的最坏情况合成。在Ernst W. Mayr和Natacha Portier，编辑，第31届计算机科学理论方面国际研讨会，STACS 2014，2014年3月5-8日，法国里昂，LIPICS第25卷，第199-213页。Schloss Dagstuhl - Leibniz - Zentru…
2017-04-27 cs.AI cs.FL cs.GT
Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
本文将CPT引入MC与MDP的序贯风险决策，通过关联多目标可达性分析确立无记忆随机策略的最优性，并给出无限视界MDP的CPT值计算算法及MC特例的多项式算法。
2025-05-14 cs.LO
Probabilistic Systems with LimSup and LimInf Objectives
我们给多项式时间算法计算马尔可夫决策过程（MDP）与limsup和liminf目标的值。一个实值的奖励被分配给每个状态，并且MDP中的无限路径的值是limsup（resp. MDP的值是可以通过解析MDP的决策来实现的无限路径的最大期望值。使用我们的结果MDP，我们表明，回合制随机游戏limsup和liminf目标可以解决NP \cap coNP。
2008-09-09 cs.GT cs.LO
MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
Masaryk University（马萨里克大学）；IST Austria（奥地利科学技术研究所）；University of Oxford（牛津大学）
我们提出了MultiGain，一个工具来合成多个平均回报目标的马尔可夫决策过程（MDP）的策略。我们的模型在PRISM中描述，我们的工具使用PRISM现有的接口和模拟器。我们的工具通过为多个平均收益目标添加新算法来扩展PRISM，并且还提供了以下功能：（i）生成策略并探索它们进行模拟，并检查它们的其他属性;以及（ii）为两个平均收益目标生成近似的帕累托曲线。此外，我们提出了一个新的实用算法分析的MDP与多个平均收益目标下的无记忆策略。
2015-01-13 cs.AI cs.LO
Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives
CNRS（法国国家科学研究中心）；University of Antwerp（安特卫普大学）；Flanders Make（法兰德斯制造研究院）
针对POMDP中omega正则目标的可判定性问题，提出启示机制限制信息损失，将弱启示和强启示两类POMDP的可判定情形归结为有限信念支撑MDP，从而给出精确算法。
2024-12-16 cs.AI cs.LO cs.SY
