Formal Techniques for Distributed Objects, Components, and Systems - 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings
Formal Techniques for Distributed Objects, Components, and Systems - 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings
复制标题
分布式对象、组件和系统的形式技术 - 第 42 届 IFIP WG 6.1 国际会议，FORTE 2022，作为第 17 届国际分布式计算技术联合会会议的一部分举行，DisCoTec 2022，意大利卢卡，2022 年 6 月 13-17 日，会议记录
DOI：
10.1007/978-3-031-08679-3_3
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Bocchi L
中科院分区：
文献类型：
--
作者：
Bocchi L
可逆调试器帮助程序员快速找到并发程序中错误行为的原因。这些调试器可以建立在经过充分研究的因果一致性可逆性理论的基础上，该理论允许人们撤消任何操作，只要其后果事先被撤消即可。到目前为止，因果一致的可逆性从未考虑过时间，而时间是现实世界应用中的一个关键方面。在这里，我们通过过程代数研究并发系统中可逆性和时间之间的相互作用。 Hennessy 和 Regan 提出的时间过程语言 (TPL) 是一种易于理解的 CCS 扩展，具有离散时间和超时运算符。我们定义 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathtt {revTPL}$$\end{document}，TPL 的可逆扩展，我们证明它满足因果一致可逆微积分所期望的属性。或者，我们证明 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathtt {revTPL}$$\end{document} 可以解释为可逆 CCS 随时间的扩展。
Reversible debuggers help programmers to quickly find the causes of misbehaviours in concurrent programs. These debuggers can be founded on the well-studied theory of causal-consistent reversibility, which allows one to undo any action provided that its consequences are undone beforehand. Till now, causal-consistent reversibility never considered time, a key aspect in real world applications. Here, we study the interplay between reversibility and time in concurrent systems via a process algebra. The Temporal Process Language (TPL) by Hennessy and Regan is a well-understood extension of CCS with discrete-time and a timeout operator. We define \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathtt {revTPL}$$\end{document}, a reversible extension of TPL, and we show that it satisfies the properties expected from a causal-consistent reversible calculus. We show that, alternatively, \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathtt {revTPL}$$\end{document} can be interpreted as an extension of reversible CCS with time.