带响应机制的转换系统的细化
计算机科学中的逻辑
2012-07-19 v1
摘要
受属性规范中的响应模式及灵活工作流管理系统应用的启发，我们报告了一项关于模态和混合转换系统的初步研究；其中 must 转换被解释为“最终必须”，且实现中可以包含在运行时解析的 may 行为。我们提出带响应机制的转换系统（TSRs）作为适合此项研究的模型。我们证明了 TSRs 对应于一类受限的混合转换系统，我们称之为动作确定性混合转换系统。我们表明 TSRs 允许对死锁状态和接受状态进行自然定义。随后，我们将混合转换系统的标准细化定义迁移至 TSRs，并证明细化并不保持无死锁性。这引出了安全细化的提议，即那些保持无死锁性的细化。我们通过一个小型药物工作流示例展示了 TSRs 及（安全）细化的使用。
引用
@article{arxiv.1207.4270,
title = {Refinement for Transition Systems with Responses},
author = {Marco Carbone and Thomas Hildebrandt and Gian Perrone and Andrzej Wąsowski},
journal= {arXiv preprint arXiv:1207.4270},
year = {2012}
}
备注
In Proceedings FIT 2012, arXiv:1207.3485