可达性约束下接受规约的商运算
形式语言与自动机理论
2014-11-25 v1
摘要
商运算是组合的对偶操作，在规约理论中至关重要，因为它允许综合缺失的规约，从而实现增量式设计。本文研究一种基于标记接受规约（MAS）的规约理论，该规约是 enriched 了由接受集编码的可变性信息以及状态上可达性约束的自动机。我们为 MAS 定义了一个可靠且完备的商运算，从而通过构造确保可达性性质。
引用
@article{arxiv.1411.6463,
title = {Quotient of Acceptance Specifications under Reachability Constraints},
author = {Guillaume Verdier and Jean-Baptiste Raclet},
journal= {arXiv preprint arXiv:1411.6463},
year = {2014}
}