面向无穷迹与活性的 Büchi 类型
计算机科学中的逻辑
2014-01-22 v1 编程语言
摘要
我们开发了一种基于 Büchi 自动机的新型类型与效应系统，以捕获由一种允许非确定性选择和无穷递归的小型语言所产生的有限和无穷迹。有两个关键的技术贡献：(a) 基于策略 Büchi 自动机定义的等价关系的抽象，即 Büchi 抽象；(b) 一种正确捕获无穷迹的新型类型与效应系统。我们展示了 Büchi 抽象如何融入抽象解释框架，并证明了其可靠性与完备性。
引用
@article{arxiv.1401.5107,
title = {B\"uchi Types for Infinite Traces and Liveness},
author = {Martin Hofmann and Wei Chen},
journal= {arXiv preprint arXiv:1401.5107},
year = {2014}
}