<figure><img src="image_1.png" /></figure>

HAL
open science

# Tallulah, a Tool to Support the Axiomatic Approach to Causal-Consistent Reversibility

William Arnone, Ivan Lanese

► To cite this version:

William Arnone, Ivan Lanese. Tallulah, a Tool to Support the Axiomatic Approach to Causal-Consistent Reversibility. RC 2025 - 17th Conference on Reversible Computation, Jul 2025, Odense, Denmark. pp.1-8, 10.1007/978-3-031-97063-4_1. hal-05399407

HAL Id: hal-05399407

https://inria.hal.science/hal-05399407v1

Submitted on 4 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Tallulah, a Tool to Support the Axiomatic Approach to Causal-Consistent Reversibility *

William Arnone<fnref n="1" /> and Ivan Lanese<fnref n="2" />

**Abstract.** The axiomatic approach to causal-consistent reversibility allows one to prove relevant properties of concurrent reversible formalisms, such as causal consistency, causal safety and causal liveness, by checking a few simple axioms. The approach works on Labeled Transition Systems equipped with a notion of Independence (LTSIs). Even if the axioms are quite simple, verifying them on non-trivial LTSIs is time consuming and involves a few subtleties. We present Tallulah, a tool which allows one to automatically verify various axioms on concrete LTSIs, suggests how to patch the LTSI when some axiom does not hold, and colors the transitions to highlight when they belong to the same event.

## 1 Introduction

Reversible computing attracted interest since 1961, when Landauer showed that reversible computing is a key for developing hardware with low energy consumption [14]. Since then, it has found applications in many areas, including debugging [21,19], simulation [7], robotics [20], and biological modeling [24]. While reversibility in a sequential setting is enabled by recursively undoing the last action, in concurrent systems such an approach is not viable, since there may be no total order of actions, and even if a total order can be found, using it as a basis for reversibility hides relevant causality information. E.g., in debugging of concurrent systems such causality information allows one to reduce the part of code that needs to be inspected when looking for a bug causing a visible misbehavior. This triggered the study of *causal-consistent reversibility* [9], which prescribes that any action can be undone, provided that its consequences, if any, are undone beforehand. Alternatively, this can be described by saying that causally dependent actions are undone in reverse order, while independent actions can be undone in any order. Notably, the classical models and languages for concurrency are not reversible, since during computation they lose information, hence

<footnote n="1">¹ Power Up Team business unit of Doc Creativity Soc. Coop</footnote>

<footnote n="2">² Olas Team, University of Bologna & INRIA, Bologna, Italy</footnote>

<footnote>* This work has been partially supported by the EU Marie Skłodowska-Curie action ReGraDe-CS (No: 101106046), by French ANR project SmartCloud ANR-23-CE25-0012, by PRIN project FREEDA (CUP: I53D23003550006), funded by the frameworks PRIN (MUR, Italy) and Next Generation EU, and by INdAM - GNCS 2024 project MARVEL, code CUP E53C23001670001. We thank the anonymous reviewers for their comments and suggestions.</footnote>
they need to be extended to satisfy causal-consistent reversibility. This resulted
in many works extending various models and languages, including CCS [9,25],
the π-calculus [8], the higher-order π-calculus [15], Klaim [10], Place Transition
nets [22], the programming language Erlang [16] and many others (see also the
survey in [11]). All these extensions use similar yet slightly different techniques to
extend the underlying frameworks, and prove the correctness of their construc-
tions by showing properties such as the causal-consistency theorem [9, Theorem
1] using similar yet ad hoc techniques.

In order to simplify the development of causal-consistent models, and to better understand the relationships among the properties of interest, an *axiomatic approach* has been proposed [17,18], whereby such properties can be proved from a small number of simple axioms. The idea is that proving the axioms is much simpler than proving the properties directly. The approach has been developed in a general setting of Labeled Transition Systems with Independence (LTSIs) [26], which has been shown to be expressive enough to cover many relevant models in the literature [18, Section 7]. The success of the axiomatic approach is shown by the amount of subsequent works which exploited it, such as [12,4,23,6,5,3,13].

While checking the axioms is easier than proving the properties of interest directly, doing so on concrete LTSIs is tedious and error prone, and involves a few subtleties. For this reason we have developed Tallulah, a tool to automatize such checks. More precisely, Tallulah allows one to automatically verify the axioms on concrete finite LTSIs, suggests how to patch the LTSI when some axiom does not hold, and colors the transitions to highlight when they belong to the same event. As evidence of the usefulness of Tallulah, by testing it on the examples in [17], it highlighted a non-trivial error in Example 4.15, triggering a refinement in the theory later presented in [18].

**2 The Axiomatic Approach: a Recap**

While referring to [18] for a detailed description of the axiomatic approach, we
recall here the main elements needed to appreciate the contribution of Tallulah.
The axiomatic approach considers as framework Labeled Transition Systems
with Independence, defined as follows:

**Definition 1 (LTS with Independence).** We say that $(\text{Proc}, \text{Lab}, \rightarrow, \iota)$ is an LTS with Independence (LTSI) where $\text{Proc}$ is the set of states, $\text{Lab}$ the set of labels, $\rightarrow \subseteq \text{Proc} \times \text{Lab} \times \text{Proc}$ a transition relation and $\iota$ (for independence) an irreflexive symmetric binary relation on transitions.

We say two transitions $P_1 \xrightarrow{a} Q_1$ and $P_2 \xrightarrow{b} Q_2$ are *coinitial* iff $P_1 = P_2$ and *cofinal* if $Q_1 = Q_2$.

We are interested in reversible LTSI, obtained by adding a notion of inde-
pendence to combined LTSs defined as follows.

**Definition 2 (Reverse and combined LTS).** *Given an LTS (Proc, Lab, →), let the reverse LTS be (Proc, Lab, ↷), where P ↷→ Q iff Q ↷→ P. It is convenient*
to combine the two LTSs (forward and reverse): let the reverse labels be $Lab = \{a : a \in Lab\}$, and define the combined LTS to be $\rightarrow \subseteq Proc \times (Lab \cup Lab) \times Proc$
by $P \xrightarrow{a} Q$ iff $P \xrightarrow{a} Q$ and $P \xrightarrow{\sim a} Q$ iff $P \xrightarrow{\sim a} Q$.

A main notion is that of *events*, which are equivalence classes of transitions on opposite sides of commuting squares, where a *commuting square* is composed of transitions: $P \xrightarrow{a} Q$, $P \xrightarrow{b} R$, $Q \xrightarrow{b} S$, $R \xrightarrow{a} S$, and their inverses, where all pairs of coinitial transitions are independent (see Figure 1, diagram on the right, in the next section).

We list below the properties from [18] which are supported by Tallulah:

**Square Property (SP):** if there are two coinitial independent transitions (say the transitions from $P$ in the commuting square above), there are two co-final transitions closing the commuting square (the transitions to $S$ in the commuting square above);

**Backward Transitions are Independent (BTI):** any two coinitial backward transitions are independent;

**Well-Foundedness (WF):** there is no infinite sequence of backward transitions, which in a finite LTS means that there are no cycles of backward transitions;

**Coinitial Propagation of Independence (CPI):** if there is independence in a corner of a square, it propagates to all the corners (called Propagation of Coinitial Independence - PCI in [18]);

**Independence Respects Events (IRE):** if two transitions $t_1$ and $t_2$ are independent, the same holds for all transitions in the same event as $t_1$ and $t_2$;

**Coinitial Independence Respects Events (CIRE):** same as IRE, but it is only required if both pairs of transitions are made of coinitial transitions;

**Independence of Events is Coinitial (IEC):** independence of transitions is always justified by independence of coinitial transitions in the same events;

**Independence of Diamonds (ID):** all squares have independence in all corners, hence they are commuting squares;

**Reversing Preserves Independence (RPI):** independence is preserved by reversing any of the transitions.

# 3 Tallulah

The Tallulah tool is written in python3, and it exploits ANTLR for parsing, Graphviz to display finite reversible LTSs (which are seen as directed graphs), and Tkinter for the graphical interface. It is open source, and distributed under the MIT license. It can be found in the dedicated GitHub repository [2]. A first description of the tool appeared in the Bachelor thesis of the first author [1] (in Italian).

As mentioned, Tallulah exploits Graphviz, which allows one to display graphs, but does not allow to describe the independence relation. For this reason, Tallulah actually extends the DOT format used by Graphviz with a description of
<figure><img src="image_3.png" /><figcaption>**Fig. 1.** Commuting square LTSI</figcaption></figure>

the independence relation. This is interpreted as a comment in the DOT format, hence one can use standard tools to visualize the LTSs.

A sample extended DOT file and the corresponding graphic representation are in Figure 1. It defines a commuting square with independence in all corners.

Lines 2-5 describe transitions, while states are implicitly deduced from transitions. Only forward transitions are represented, but we assume that for each forward transition we also have the corresponding backward transition. If `color` information is not provided, Tallulah will add it automatically, assigning the same color to transitions in the same event. Lines 8-11 describe the independence relation. The `>` and `<` symbols clarify the direction of the considered transitions, forwards and backwards respectively.

After opening a DOT file, the main window of the tool opens, with the layout in Figure 2.

On the left, we can see the LTS. On the top-right we can see the list of properties that can be checked, and the button allowing one to check them. On the bottom, we can see all the pairs composing the independence relation.

One can select the properties of interest and check them.

The result of the tool is shown as in Figure 3, where for space reasons we checked only a few properties. When a property does not hold, as in the case of CPI and CIRE in the example, Tallulah suggests possible changes to the graph to enforce it. In particular, for all the properties requiring independence between some transitions (BTI, CPI, IRE, CIRE, ID, RPI) the tool suggests to add the required independence. For SP instead the tool suggests to add the missing transitions. WF fails in finite graphs only if there is a cycle of backward transitions, suggested fixes require to break the cycle by dropping at least one such transition. This would automatically remove the reverse transition as well, and independence pairs involving them, if any. For IEC we have two possibilities, either a pair of coinital transitions in the same events of two independent transitions exists, but independence is missing, or no such pair of coinital tran-
<figure><img src="image_4.png" /><figcaption>Fig. 2. Tallulah screenshot</figcaption></figure>

sitions exists. In the first case the issue can be fixed by adding independence as
needed, while for the second issue no fix is proposed.

The user can select all or part of the suggested changes, and the graph is
updated accordingly.

Notice that in the case of Figure 3 CPI cannot actually be forced: the inde-
pendence relation is irreflexive by definition, but CPI would require to add some
independence between a transition and itself, contradicting irreflexivity. This is
actually the error that the tool revealed in [17, Example 4.15]. The description of
the example there required to add some independence by closing under CPI (and
<figure><img src="image_5.png" /><figcaption>Fig. 3. Tallulah results, screenshot</figcaption></figure>

BTI), and assumed CPI to hold afterwards. By testing the tool on the example, the error message in Figure 3 came out, showing that this was not possible.

## 4 Conclusion and Future Work

Tallulah allows one to check and force properties in finite reversible LTSIs, and in our experience it is a good support to work on the topic. It is nevertheless still quite preliminary, in particular since it only allows one to check some of the axioms and properties listed in [18, Table 1]. In particular, it only considers properties that deal with a limited number of transitions at the time. E.g., SP deals with four transitions at the time at most. Dealing with properties refer-ring to sequences of transitions of unbounded length, such as causal consistency or the various forms of causal safety and causal liveness, would not be trivial since direct application of the definition would lead to divergence, hence smart algorithms would need to be developed. From the software engineering point of view instead adding new properties is simple, since thanks to the modular de-sign of Tallulah each property is defined by a source file on its own (available in the *properties* directory), hence one only needs to add a source file for the new property (implementing the same interface as the available ones), and link its check to the graphical interface by adding an additional checkbox.
References

1. William Arnone. Tallulah: Gestione assiomatica di modelli reversibili. Bachelor's thesis, University of Bologna, 2022.

2. William Arnone and Ivan Lanese. Tallulah github repository. https://github.com/WilliamArnone/Tallulah, 2025.

3. Clément Aubert. The correctness of concurrencies in (reversible) concurrent calculi. *J. Log. Algebraic Methods Program.*, 136:100924, 2024.

4. Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi, and Claudio Sacerdoti Coen. Causal reversibility implies time reversibility. In *QEST 2023*, volume 14287 of LNCS, pages 270-287. Springer, 2023.

5. Marco Bernardo and Claudio Antares Mezzina. Reversibility in process calculi with nondeterminism and probabilities. In *ICTAC 2024*, volume 15373 of LNCS, pages 251-271. Springer, 2024.

6. Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. revtpl: The reversible temporal process language. *Log. Methods Comput. Sci.*, 20(1), 2024.

7. Christopher D. Carothers, Kalyan S. Perumalla, and Richard Fujimoto. Efficient optimistic parallel simulations using reverse computation. *ACM Transactions on Modeling and Computer Simulation*, 9(3):224-253, 1999.

8. Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the reversible $\pi$-calculus. In *LICS*, pages 388-397. IEEE Computer Society, 2013.

9. Vincent Danos and Jean Krivine. Reversible communicating systems. In Philippa Gardner and Nobuko Yoshida, editors, *CONCUR*, volume 3170 of LNCS, pages 292-307. Springer, 2004.

10. Elena Giachino, Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. Causal-consistent rollback in a tuple-based language. *Journal of Logical and Algebraic Methods in Programming*, 88:99-120, 2017.

11. Robert Glück, Ivan Lanese, Claudio Antares Mezzina, Jaroslaw Adam Miszczak, Iain C. C. Phillips, Irek Ulidowski, and Germán Vidal. Towards a taxonomy for reversible computation approaches. In *RC 2023*, volume 13960 of LNCS, pages 24-39. Springer, 2023.

12. Eva Graversen, Iain Phillips, and Nobuko Yoshida. Event structures for the reversible early internal $\pi$-calculus. *J. Log. Algebraic Methods Program.*, 124:100720, 2022.

13. Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, and Giovanni Fabbretti. Reversible debugging of concurrent Erlang programs: Supporting imperative primitives. *J. Log. Algebraic Methods Program.*, 138:100944, 2024.

14. Rolf Landauer. Irreversibility and heat generated in the computing process. *IBM Journal of Research and Development*, 5:183-191, 1961.

15. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversibility in the higher-order $\pi$-calculus. *Theoretical Computer Science*, 625:25-84, 2016.

16. Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. A theory of reversibility for Erlang. *Journal of Logical and Algebraic Methods in Programming*, 100:71-97, 2018.

17. Ivan Lanese, Iain C. C. Phillips, and Irek Ulidowski. An axiomatic approach to reversible computation. In *Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings*, volume 12077 of Lecture Notes in Computer Science, pages 442-461. Springer, 2020.
18. Ivan Lanese, Iain C. C. Phillips, and Irek Ulidowski. An axiomatic theory for reversible computation. *ACM Trans. Comput. Log.*, 25(2):11:1–11:40, 2024.

19. Ivan Lanese, Ulrik Pagh Schultz, and Irek Ulidowski. Reversible computing in debugging of Erlang programs. *IT Prof.*, 24(1):74–80, 2022.

20. Johan Sund Laursen, Ulrik Pagh Schultz, and Lars-Peter Ellekilde. Automatic error recovery in robot assembly operations using reverse execution. In *IROS*, pages 1785–1792. IEEE, 2015.

21. James McNellis, Jordi Mola, and Ken Sykes. Time travel debugging: Root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914, 2017.

22. Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. Reversing place transition nets. *Log. Methods Comput. Sci.*, 16(4), 2020.

23. Shunya Oguchi and Shoji Yuen. CRIL: A concurrent reversible intermediate language. In *EXPRESS/SOS 2023*, volume 387 of *EPTCS*, pages 149–167, 2023.

24. Iain Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and the modelling of the ERK signalling pathway. In *RC 2012*, volume 7581 of *LNCS*, pages 218–232. Springer, 2012.

25. Iain C.C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. *Journal of Logic and Algebraic Programming*, 73(1-2):70–96, 2007.

26. Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. Models of concurrency: Towards a classification. *Theoretical Computer Science*, 170(1-2):297–348, 1996.