无限有限状态标记迁移系统族上的CTL*模型检验（技术报告）
计算机科学中的逻辑
2026-01-23 v1
摘要
我们研究了在CTL*中编写的时序性质上对无限有限状态标记迁移系统族进行模型检验的算法。这类族例如作为高度可配置系统或软件产品线的模型出现。我们使用上下文无关图语法对族进行建模。然后我们开发了一种在语法产生式规则上组合式工作的状态标记算法，该算法仅对规则应用的上下文具有有限信息。结果是建模相同族但具有扩展标签的图语法。我们利用该语法来决定一个族的所有、部分或（无穷）多个成员是否满足给定的时序性质。我们实现了算法并展示了早期实验。
引用
@article{arxiv.2601.15756,
title = {CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)},
author = {Roberto Pettinau and Christoph Matheja},
journal= {arXiv preprint arXiv:2601.15756},
year = {2026}
}
备注
Technical Report of a paper accepted at TACAS 2026