Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our main focus is to develop the theory underlying PrIC3. Alongside, we present a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Robust Almost-Sure Reachability in Multi-Environment MDPs
本文研究 MEMDP 中对所有环境鲁棒满足几乎必然可达性的策略合成问题，证明其存在性判定为 PSPACE 完全，并实现算法在多个基准上验证有效性。
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
本文提出了一种高效计算最优条件可达性的方法，适用于无环马尔可夫决策过程，并在抽象-细化框架中分析大量马尔可夫链，展示了在贝叶斯网络分析、概率程序和运行时监控中的有效性。
Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of reactive probabilistic systems. We explore XPL, an extension to GPL allowing the semantics of nondeterminism present in Markov decision processes (MDPs). XPL is expressive enough that a number of independently studied problems--- such as termination of Recursive MDPs (RMDPs), PCTL* model checking of MDPs, and reachability for Branching MDPs--- can all be cast as model checking over XPL. Termination of multi-exit RMDPs is undecidable; thus, model checking in XPL is undecidable…
We study qualitative multi-objective reachability problems for Ordered Branching Markov Decision Processes (OBMDPs), or equivalently context-free MDPs, building on prior results for single-target reachability on Branching Markov Decision Processes (BMDPs). We provide two separate algorithms for "almost-sure" and "limit-sure" multi-target reachability for OBMDPs. Specifically, given an OBMDP, $\mathcal{A}$, given a starting non-terminal, and given a set of target non-terminals $K$ of size $k = |K|$, our first algorithm decides whether the supremum probability, of generating a tree that contains…
Q-Learning for Reachability in MEC-Free MDPs
本文提出Quasar，首个无模型Q学习算法，用于无最大端分量MDP的可达性，通过时序差分更新实现渐近最优，内存从O(|S|^2|A|)降至O(|S||A|)，样本效率显著优于基于模型方法。
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
本文提出基于初等不动点理论的证书，用于马尔可夫决策过程的可达性与期望奖励模型检查，并在Isabelle/HOL中形式化验证，增强Storm模型检查器生成证书，实现基准集的首次正式认证。
Certifying Almost-Sure Reachability in Unknown MDPs
本文针对未知MDP，研究仅通过采样访问验证已有策略的几乎必然可达性，在非零转移概率下界p_min限制下可学习带PAC保证的证书，实验显示该条件偏保守。
Exploiting Adjoints in Property Directed Reachability Analysis
本文提出两种格论框架下的性质导向可达性新算法，分别利用伴随和下集处理安全不变量与反例，并应用于马尔可夫决策过程的定量可达性分析。
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably p…
We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph …
Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-in…
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster-Tarski and Kleene theorems. We introduce four concrete instances of LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
本文针对弦图组合描述的 MDP，提出利用子 MDP 上形成 Pareto 曲线的调度器进行局部优化，并设计高效声音近似算法，在 Storm 上验证了其可扩展性。
The goal of the thesis is to leverage fast graph algorithms and modern algorithmic techniques for problems in model checking and synthesis on graphs, MDPs, and game graphs. The results include symbolic algorithms, a well-known class of algorithms in model checking that trades limited access to the input model for an efficient representation. In particular, we present the following results: Algorithms for game graphs with mean-payoff Büchi objectives and mean-payoff coBüchi objectives which match one of the best running time bounds for mean-payoff objectives. A near-linear time randomized algor…
Property Directed Reachability with Extended Resolution
本文提出 PdrER，一种基于扩展归结的 Pdr 推广算法，利用更强的证明系统构造更短证明与更紧凑不变量，在硬件模型检测竞赛基准上显著优于 Pdr，推动强证明系统在模型检测中的实用化。
In 2015, it was shown that reachability for arbitrary directed graphs can be updated by first-order formulas after inserting or deleting single edges. Later, in 2018, this was extended for changes of size $\frac{\log n}{\log \log n}$, where $n$ is the size of the graph. Changes of polylogarithmic size can be handled when also majority quantifiers may be used. In this paper we extend these results by showing that, for changes of polylogarithmic size, first-order update formulas suffice for maintaining (1) undirected reachability, and (2) directed reachability under insertions. For classes of di…
Beyond Lemma Sharing -- Novel Parallelization Strategies for Property Directed Reachability
针对PDR并行化可扩展性难题，提出抢占式传播和ARPOS两种新策略，并在rIC3上验证，显著优于经典引理共享。
Incremental Property Directed Reachability
本文提出增量式属性定向可达性算法IPDR，复用增量SAT求解器的先前验证结果，支持增量约束与松弛，在电路铺石和并行程序问题上性能优于Z3的SPACER，可大量复用实例间子句。
Certificate-Aware Property-Directed Reachability
CAPDR是一种带证书的属性导向可达性方法，通过联合优化运行时间、证书大小和检查时间，提升硬件安全验证效率。
A Supervisory Control Algorithm Based on Property-Directed Reachability
本文提出基于属性导向可达性模型检查算法的控制器合成算法，用于离散事件系统中安全且最小限制的控制器设计，并通过实验验证其在形式化监督控制器合成中的潜力。
In recent work, the second and third authors introduced a technique for reachability checking in 1-bounded Petri nets, based on wiring decompositions, which are expressions in a fragment of the compositional algebra of nets with boundaries. Here we extend the technique to the full algebra and introduce the related structural property of decomposition width on directed hypergraphs. Small decomposition width is necessary for the applicability of the reachability checking algorithm. We give examples of families of nets with constant decomposition width and develop the underlying theory of decompo…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。