Specifying reversibility with TLA^+

DOI10.1016/J.JLAMP.2020.100582MaRDI QIDQ2210867zbMATH OpenOpenAlexFDO

Authors Tatjana Kapus

Publication date 9 November 2020

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2020.100582

zbMATH Keywords

concurrent systemmodel checkingreversible computationtemporal logic of actions

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Systems biology, networks (92C42)

Recommendations

• scientific article; zbMATH DE number 1390334
• Relative expressiveness of calculi for reversible concurrency
• A modular formalization of reversibility for concurrent models and languages
• Concurrent flexible reversibility
• A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway

Cites work

• A compositional semantics for the reversible -calculus
• A modular formalization of reversibility for concurrent models and languages
• A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway
• Causal-consistent reversibility
• CONCUR 2004 - Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• scientific article; zbMATH DE number 5347282 (Why is no real title available?)
• scientific article; zbMATH DE number 3902012 (Why is no real title available?)
• scientific article; zbMATH DE number 3985193 (Why is no real title available?)
• scientific article; zbMATH DE number 1950554 (Why is no real title available?)
• scientific article; zbMATH DE number 4119618 (Why is no real title available?)
• scientific article; zbMATH DE number 2086413 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• LTL is expressively complete for Mazurkiewicz traces
• On separating the EREW and CREW PRAM models
• Reversing algebraic process calculi
• Reversing Higher-Order Pi
• Reversing steps in membrane systems computations
• The existence of refinement mappings
• The PlusCal Algorithm Language

Describes a project that uses

Uses Software

• TLA
• PEPA

This page was built for publication: Specifying reversibility with \(\mathrm{TLA}^+\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2210867)