区间马尔可夫决策过程的合成推理

持续时间演算中混合CSP的Hoare式组合推理

Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus

用于混合系统验证的演绎方法因正确性证明中语句的格式而异。基于霍尔三重推理的例子，我们已经研究了几个这样的方法，在混合CSP描述的系统，每个基于不同的断言语言，符号的时间，符号的证明，每个都有其优点和缺点的表达能力，组合性和实用方便。在本文中，我们提出了一种新的方法，基于弱单调时间的语义交织，持续时间演算（DC）与无限区间和一般不动点的逻辑语言，和一个新的意义Hoare类三元组，统一断言和时间条件。我们包括一个证明系统的推理系统的性质写在新的形式的三元组，是完整的相对于DC的有效性。

Mixed Nondeterministic-Probabilistic Interfaces

Interface theories are powerful frameworks supporting incremental and compositional design of systems through refinements and constructs for conjunction, and parallel composition. In this report we present a first Interface Theor -- |Modal Mixed Interfaces -- for systems exhibiting both non-determinism and randomness in their behaviour. The associated component model -- Mixed Markov Decision Processes -- is also novel and subsumes both ordinary Markov Decision Processes and Probabilistic Automata.

标记马尔可夫过程的基于分布的互模拟

Distribution-based bisimulation for labelled Markov processes

在本文中，我们提出了一个（子）分布为基础的互模拟标记马尔可夫过程，并将其与早期的定义状态和事件的互模拟，这两个比较状态。与那些基于状态的互模拟相比，我们的分布互模拟更弱，但更接近于线性性质。我们构建了一个逻辑和一个度量来描述我们的分布互模拟，并讨论了线性，连续性和组成特性。

多目标马尔可夫自动机

Markov Automata with Multiple Objectives

马尔可夫自动机结合了非确定性，概率分支和指数分布延迟。这种连续时间马尔可夫决策过程的组合变体被用于可靠性工程、性能评估和随机调度。到目前为止，它们的核查侧重于单一目标，如（定时）可达性和预期成本。在实践中，这些目标往往是相互依赖的，目的是揭示权衡取舍。我们提出的算法，同时分析几个目标和近似帕累托曲线。这包括，例如，多个（定时）可达性目标或各种预期成本目标。我们还考虑其组合，如在预算内的时间目标-哪些政策保证达到目标状态的最后期限内至少有概率$p$，同时保持允许的平均成本低于阈值？我们采用现有的方法为经典的马尔可夫决策过程。主要的挑战是如何对待利用国家居留时间的政策，即使是为了不定时的目标。实验结果表明了该方法的可行性和可扩展性。

IntervalMDP.jl：针对区间马尔可夫决策过程的加速值迭代

IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes

本文提出 Julia 包 IntervalMDP.jl，利用多线程 CPU 和 GPU 加速值迭代算法，高效支持区间马尔可夫决策过程的概率分析、策略综合与验证，在计算时间和内存消耗上显著优于现有工具。

并发进程的弱马尔可夫互模拟同余和精确CTMC级集结

Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes

我们最近定义了一个弱马尔可夫互模拟等价的集成时间设置，它减少了序列的指数定时的内部行动，个人指数定时的内部行动具有相同的平均持续时间和执行概率的相应序列。这种弱马尔可夫互模拟等价是一个同余序列过程的抽象和原来诱导一个确切的CTMC级聚集在稳态所有考虑的过程。然而，它并不是平行合成的一致性。在本文中，我们展示了如何推广的等价性的方式，一个合理的权衡抽象，组合性和精确性之间实现了并发进程。我们将看到，通过增强并行计算中的抽象能力，可以检索关于并行组合的同余属性，所得到的CTMC级聚合仅对于所考虑过程的某个子集在稳定状态下是精确的。

增广区间马尔可夫链的可达性

Reachability in Augmented Interval Markov Chains

在本文中，我们提出了增广的区间马尔可夫链（AIMCs）：一个概括的熟悉的区间马尔可夫链（IMCs）的不确定的转移概率是另外允许相互依赖。这种新模型保留了IMC所提供的灵活性，用于描述参数不清楚的随机系统，例如由于测量误差，但也允许我们指定具有已知相同概率的转换，从而提供进一步的表达能力。本文的重点是可达性在AIMCs。我们研究了定性、精确定量和近似可达性问题及其自然子问题，并建立了它们复杂性的上界和下界。我们证明了确切的可达性问题是至少作为著名的平方根和问题一样难，但令人惊讶的是，近似版本在于$\mathbf{NP}$，如果底层图是已知的，而限制的确切问题的不确定边缘的常数是在$\mathbf{P}$。最后，我们表明，在图结构的不确定性影响复杂性证明$\mathbf{NP}$ -完整的定性子问题，与一个容易获得的上限$\mathbf{P}$为同一个子问题与已知的图形结构。

组合强化学习的范畴语义

Categorical semantics of compositional reinforcement learning

本文提出基于范畴论的组合强化学习框架，通过MDP范畴的推出操作实现任务组合，并统一安全与对称性概念。

概率自动机的保代价互模拟

Cost Preserving Bisimulations for Probabilistic Automata

概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。

Satisfiability Bounds for $ω$-Regular Properties in Bounded-Parameter Markov Decision Processes

We consider the problem of computing minimum and maximum probabilities of satisfying an $ω$-regular property in a bounded-parameter Markov decision process (BMDP). BMDP arise from Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown. $ω$-regular languages form a large class of properties, expressible as, e.g., Rabin or parity automata, encompassing rich specifications such as linear temporal logic. In a BMDP the probability to satisfy the property depends on the unknown transitions probab…

通过假设-保证推理实现李雅普诺夫函数的组合性

Compositionality of Lyapunov functions via assume-guarantee reasoning

本文提出一个范畴框架，用于安全问题的假设-保证推理，通过将系统视为镜头，为参数化微分方程系统特别适应了假设-保证推理，特别是针对局部输入到状态稳定性（L）ISS李雅普诺夫函数。

通过学习进行马尔可夫决策过程的宽容监督器合成

Permissive Supervisor Synthesis for Markov Decision Processes through Learning

本文提出基于学习和组合模型检查的新型框架，用于在分布式方式下生成宽容的本地监督器，以解决概率系统中的状态空间爆炸问题。