Formal Verification Techniques for Reversible Languages

In RC verifying forward computations equipped with distributed backtracking on non-observable actions is equivalent to verifying their causal compression which may be significantly smaller in size and therefore much more efficiently verifiable. Also, classical Linear Temporal Logic (LTL) and unfolding algorithms can be used to model check reversible systems, as an LTL formula with a past operator can be translated in terms of "future" states. This may not be the case with logics such as Computation Tree Logic (CTL) and logics for truly concurrent systems. We plan to investigate new logics for truly concurrent systems with specific operators for causality, consistency and reversible modalities. Model checking will be complemented by runtime monitoring through types. Specifically, for concurrent reversible processes, we will investigate the development of appropriate session type disciplines.

1) Reversible extensions of CTL and logics for true concurrency; 2) Type systems, in particular session types, for reversible languages; 3) Complexity/efficiency analysis of the developed techniques.

M19, AGH, I. Ulidowski, reversible logics; M22, UNURB, C. A. Mezzina, reversible model checking; M36, RUG, J. Perez: types and monitoring.