认知时序规范的去 Safra 化综合
计算机科学中的逻辑
2014-05-05 v1
摘要
本文针对在具有环境状态不完全信息的单代理系统上，以线性时序单代理认知逻辑 KLTL（或 ）给出的规范，探讨其综合问题。Van der Meyden 和 Vardi 已证明该问题是 2Exptime 完全的。然而，他们的过程依赖于复杂的自动机构造，由于使用了类 Safra 确定化， notoriously 难以高效实现。我们针对 KLTL 的一个大片断提出了一种“去 Safra 化”的综合过程。该构造首先利用信息集构造将综合问题转化为检查通用 co-B"{u}chi 树自动机空性的问题。随后，我们构建了一个安全博弈，该博弈可利用底层自动机的结构，通过基于反链的符号技术求解。该技术已被实现并应用于若干案例研究。
引用
@article{arxiv.1405.0424,
title = {Safraless Synthesis for Epistemic Temporal Specifications},
author = {Rodica Bozianu and Catalin Dima and Emmanuel Filiot},
journal= {arXiv preprint arXiv:1405.0424},
year = {2014}
}