Static VS dynamic reversibility in CCS. (English) Zbl 1476.68180
Devitt, Simon (ed.) et al., Reversible computation. 8th international conference, RC 2016, Bologna, Italy, July 7–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9720, 36-51 (2016).
Summary: The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Reversible CCS (RCCS), proposed by Danos and Krivine, enacts reversibility by means of memory stacks. Ulidowski and Phillips proposed a general method to reverse a process calculus given in a particular SOS format, by exploiting the idea of making all the operators of a calculus static. CCSK is then derived from CCS with this method. In this paper we show that RCCS is at least as expressive as CCSK.
For the entire collection see [Zbl 1342.68013].
For the entire collection see [Zbl 1342.68013].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
References:
| [1] | Berut, A., Arakelyan, A., Petrosyan, A., Ciliberto, S., Dillenschneider, R., Lutz, E.: Experimental verification of Landauer’ s principle linking information, thermodynamics. Nature 483(7388), 187–189 (2012) · doi:10.1038/nature10872 |
| [2] | Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004) · Zbl 1099.68066 · doi:10.1007/978-3-540-28644-8_19 |
| [3] | Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 398–412. Springer, Heidelberg (2005) · Zbl 1134.68432 · doi:10.1007/11539452_31 |
| [4] | Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014) · doi:10.1007/978-3-642-54804-8_26 |
| [5] | Krivine, J.: A verification technique for reversible process algebra. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 204–217. Springer, Heidelberg (2013) · Zbl 1451.68177 · doi:10.1007/978-3-642-36315-3_17 |
| [6] | Landauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5, 183–191 (1961) · Zbl 1160.68305 · doi:10.1147/rd.53.0183 |
| [7] | Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 370–390. Springer, Heidelberg (2013) · Zbl 1381.68210 · doi:10.1007/978-3-642-37036-6_21 |
| [8] | Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980) · Zbl 0452.68027 · doi:10.1007/3-540-10235-3 |
| [9] | Perumalla, K.S., Park, A.J.: Reverse computation for rollback-based fault tolerance in large parallel systems - evaluating the potential gains and systems effects. Cluster Comput. 17(2), 303–313 (2014) · doi:10.1007/s10586-013-0277-4 |
| [10] | Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 218–232. Springer, Heidelberg (2013) · Zbl 1451.68124 · doi:10.1007/978-3-642-36315-3_18 |
| [11] | Phillips, I.C.C., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1–2), 70–96 (2007) · Zbl 1123.68065 · doi:10.1016/j.jlap.2006.11.002 |
| [12] | Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001) · Zbl 0981.68116 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
