基于广义反应过程的统一时间理论
计算机科学中的逻辑
2018-04-05 v2 形式语言与自动机理论
摘要
Hoare 与 He 的反应过程理论为并发与反应式语言的形式语义提供了统一基础。尽管具有高度适用性，他们的理论局限于那些能将事件历史表达为离散序列的模型。本文展示了如何通过采用抽象迹代数来推广该理论。我们特别表明，该代数使我们也能考虑连续时间迹，从而有助于混合系统的建模。随后，我们利用该代数在通用设定下重构反应过程理论，并证明了顺序与并行过程的特征定律，所有这些均在 Isabelle/HOL 证明助手中进行了机械验证。
引用
@article{arxiv.1712.10213,
title = {Unifying Theories of Time with Generalised Reactive Processes},
author = {Simon Foster and Ana Cavalcanti and Jim Woodcock and Frank Zeyda},
journal= {arXiv preprint arXiv:1712.10213},
year = {2018}
}
备注
7 pages, accepted for Information Processing Letters, 15th February 2018