论文标题

跨度(图):开放过渡系统的规范反馈代数

Span(Graph): a Canonical Feedback Algebra of Open Transition Systems

论文作者

Di Lavore, Elena, Gianola, Alessandro, Román, Mario, Sabadini, Nicoletta, Sobociński, Paweł

论文摘要

我们显示了Katis,Sabadini和Walters引入的开放过渡系统的代数跨度(Graph)*满足通用性能。就其本身而言,这是对这种并发模型的典型性的理由。但是,普遍财产本身就是感兴趣的,是反馈与国家之间关系的正式证明。实际上,反馈类别(最初是由卡蒂斯,萨巴迪尼和沃尔特斯提出的,也是弱追踪单类别类别的削弱,并在计算机科学中使用了各种应用。一项在几种不同情况下出现的状态自举技术可以免费提供此类类别。我们显示了以这种方式出现的跨度(图)*,是跨度(SET)的免费反馈类别。鉴于后者可以看作是谓词的代数,因此出现了开放过渡系统的代数 - 大致说明 - 由于引导状态到该代数。最后,我们将反馈类别概括为具有额外结构的状态空间:这将框架从单纯的过渡系统扩展到具有初始和最终状态的自动机。

We show that Span(Graph)*, an algebra for open transition systems introduced by Katis, Sabadini and Walters, satisfies a universal property. By itself, this is a justification of the canonicity of this model of concurrency. However, the universal property is itself of interest, being a formal demonstration of the relationship between feedback and state. Indeed, feedback categories, also originally proposed by Katis, Sabadini and Walters, are a weakening of traced monoidal categories, with various applications in computer science. A state bootstrapping technique, which has appeared in several different contexts, yields free such categories. We show that Span(Graph)* arises in this way, being the free feedback category over Span(Set). Given that the latter can be seen as an algebra of predicates, the algebra of open transition systems thus arises - roughly speaking - as the result of bootstrapping state to that algebra. Finally, we generalize feedback categories endowing state spaces with extra structure: this extends the framework from mere transition systems to automata with initial and final states.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源