分层工件系统的验证
数据库
2016-04-05 v1
摘要
数据驱动的工作流（其中IBM的业务工件(Business Artifacts)是一个典型代表）已在实践中成功部署，被工业标准所采纳，并在学术界催生了大量研究，这些研究主要集中于静态分析。本工作通过考虑比以往工作更丰富、更现实的模型，在工件验证问题上取得了显著进展，该模型融合了IBM成功的Guard-Stage-Milestone模型的核心要素。具体而言，该模型具有任务层次结构、并发性以及更丰富的工件数据。它还允许数据库主键与外键依赖，以及算术约束。结果表明了验证的可判定性并确立了其复杂度，运用了包括向量加法系统(Vector Addition Systems)的层次结构以及针对我们上下文定制的量词消去变体等新技术。
引用
@article{arxiv.1604.00967,
title = {Verification of Hierarchical Artifact Systems},
author = {Alin Deutsch and Yuliang Li and Victor Vianu},
journal= {arXiv preprint arXiv:1604.00967},
year = {2016}
}
备注
Full version of the accepted PODS paper