Probabilistic Verification Beyond Context-Freeness
Probabilistic Verification Beyond Context-Freeness
复制标题
超越上下文无关的概率验证
DOI：
10.1145/3531130.3533351
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Li G
中科院分区：
文献类型：
--
作者：
Li G
概率下推自动机(递归状态机)是一种广为人知的概率计算模型，与许多关于终止(时间)和线性时间模型检验的可判定问题相关。高阶递归方案是分析高阶计算的一种重要形式，最近的研究表明，对于高阶递归方案的概率变体，即使是确定一个方案是否几乎必然终止的基本问题也是不可判定的。在这些结果的推动下，我们研究了受限概率树-堆栈自动机(RPTSA)，它在不确定性环境下刻画了上下文无关语言的适当扩展，即多上下文无关语言。我们证明了几个验证问题，如几乎确定终止、正几乎确定终止和ω-正则模型检验，对于这类问题是可判定的，在高阶递归方案的水平上，这对应于能够验证MAHOR的概率版本(这是高阶递归方案的乘法-加法版本)。MAHOR推广了一阶递推格式，是二阶格式不可比的。
Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems concerning termination (time) and linear-time model checking. Higher-order recursion schemes (HORS) are a prominent formalism for the analysis of higher-order computation.Recent studies showed that, for the probabilistic variant of HORS, even the basic problem of determining whether a scheme terminates almost surely is undecidable. Moreover, the undecidability already holds for order-2 schemes (order-1 schemes are known to correspond to pushdown automata).Motivated by these results, we study restricted probabilistic tree-stack automata (rPTSA), which in the nondeterministic setting are known to characterise a proper extension of context-free languages, namely, the multiple context-free languages. We show that several verification problems, such as almost-sure termination, positive almost-sure termination and ω-regular model checking are decidable for this class.At the level of higher-order recursion schemes, this corresponds to being able to verify a probabilistic version of MAHORS (which are a multiplicative-additive version of higher-order recursion schemes). MAHORS extend order-1 recursion schemes and are incomparable with order-2 schemes.
登录
查看更多内容
DOI：
--
发表时间：
2009
期刊：
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
影响因子：
--
作者：
Naoki Kobayashi;Types and Higher-Order
通讯作者：
Types and Higher-Order
论线性递归方案的表现力
DOI：
--
发表时间：
2019
期刊：
International Symposium on Mathematical Foundations of Computer Science
影响因子：
--
作者：
P. Clairambault;A. Murawski
通讯作者：
A. Murawski
可折叠下推自动机和递归方案
DOI：
10.1145/3091122
发表时间：
2008
期刊：
2008 23rd Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
M. Hague;A. Murawski;C. Ong;O. Serre
通讯作者：
O. Serre
DOI：
10.1145/3453483.3454111
发表时间：
2021-04
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Raven Beutner;Luke Ong
通讯作者：
Raven Beutner;Luke Ong
多种上下文无关语言的自动机表征
DOI：
--
发表时间：
2016
期刊：
International Conference on Developments in Language Theory
影响因子：
--
作者：
Tobias Denkinger
通讯作者：
Tobias Denkinger