计算弱-MSO 可定义树集的度量
形式语言与自动机理论
2025-12-22 v2
摘要
本工作解决计算可识别无限树集合概率度量的问题。提供了一个算法，用于计算由弱交替自动机可识别（或等价地可定义于弱单一次二阶逻辑）的树语言的概率度量。该度量为均匀硬币翻转度量，或更一般地由分支随机过程生成。虽然该树语言类别小于所有规则树语言，但特别包括了可定义于弱单一次算子演算或时序逻辑 CTL 的语言。因此，新的算法可能增强概率模型检查的工具箱。
引用
@article{arxiv.2410.13479,
title = {Computing measures of weak-MSO definable sets of trees},
author = {Damian Niwiński and Marcin Przybyłko and Michał Skrzypczak},
journal= {arXiv preprint arXiv:2410.13479},
year = {2025}
}
备注
An ArXiv version of a paper from ICALP 2020