A Model Counter's Guide to Probabilistic Systems

概率自动机与概率一计数器自动机的分支时间性质模型检测

Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata

本文研究概率自动机及概率一计数器自动机对 PCTL 与 PCTL$^*$ 的模型检测，通过归约空性问题并构造行为等价的一计数器自动机，证明两类问题均不可判定。

Approximate Weighted First-Order Model Counting: Exploiting Fast Approximate Model Counters and Symmetry

We study the symmetric weighted first-order model counting task and present ApproxWFOMC, a novel anytime method for efficiently bounding the weighted first-order model count in the presence of an unweighted first-order model counting oracle. The algorithm has applications to inference in a variety of first-order probabilistic representations, such as Markov logic networks and probabilistic logic programs. Crucially for many applications, we make no assumptions on the form of the input sentence. Instead, our algorithm makes use of the symmetry inherent in the problem by imposing cardinality con…

单调多项式系统上牛顿法的上界及概率单计数器自动机的P-时间模型检验

Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata

各类无穷状态递归概率系统分析和模型检验的中心计算问题（包括拟生灭过程、多类型分支过程、随机上下文无关文法、概率下推自动机和递归马尔可夫链）是{ \em终止概率}的计算，并且计算这些概率又归结为计算对应的{ \em单调多项式系统}（MPS）的方程的{ \em最小不动点}（LFP）解，表示为x=P（x）。Etessami和Yannakakis证明了牛顿方法的分解变体对于任何具有非负解的MPS单调收敛于LFP解。随后，Esparza，Kiefer和Luttenberger得到了牛顿方法对某些类型MPS的收敛速度的上界。最近，更好的上限已获得特殊类的MPS。然而，在本文之前，对于任意（不一定是强连接的）MPS，牛顿方法的收敛速度作为输入MPS的编码大小|P|的函数，x=P（x），根本没有上界。在本文中，我们提供了最坏情况下的上界，作为输入编码大小|P|和Σ> 0的函数，对于具有LFP解q^* 的任何MPS，分解牛顿法（即使有舍入）在q^* 的加性误差Σ> 0内收敛所需的迭代次数。我们的上界基本上是最优的几个重要参数。使用我们的上界，并建立在以前的工作，我们获得了第一个P-时间算法（在标准图灵计算模型）的定量模型检验，在所需的精度，离散时间QBD和（等效）概率1-计数器自动机，相对于任何（固定）ω-正则或LTL属性。

概率环境中的系统测量与综合

Measuring and Synthesizing Systems in Probabilistic Environments

通常人们在满足给定规范的不同系统中有一个优先顺序。在关于可能输入的概率假设下，这样的偏好顺序自然地由加权自动机表示，该加权自动机为每个词分配一个值，使得如果系统生成更高的期望值，则系统是优选的。我们解决了以下最优合成问题：给定一个ω-正则规范，一个描述输入分布的马尔可夫链，以及一个衡量系统在给定输入假设下满足给定规范的加权自动机，合成一个优化测量值的系统。对于由平均支付自动机给出的安全规范和措施，最优合成问题相当于在马尔可夫决策过程（MDP）中找到一个策略，该策略对于长期平均奖励目标是最优的，这可以在多项式时间内完成。对于一般的ω-正规规范，解决方案依赖于一个新的，多项式时间的算法计算最优策略的MDP平均回报奇偶性目标。我们的算法生成的最优策略包括两个无记忆策略和一个计数器。该计数器通常没有边界。为了得到一个有限状态系统，我们展示了如何构造一个ε-最优策略，对于任何ε>0，都有一个有界计数器。我们还展示了如何在多项式时间内决定我们是否可以构造一个最优的有限状态系统（即，没有计数器的系统）。我们已经实现了我们的方法，在一个工具，采取定性和定量的规格，并自动构建一个系统，满足定性规格和优化的定量规格，如果这样的系统存在。我们呈现的实验结果显示了以这种方式生成的最佳系统。