Specifying reversibility with \(\mathrm{TLA}^+\)

DOI10.1016/j.jlamp.2020.100582zbMath1462.68125OpenAlexW3042946137MaRDI QIDQ2210867

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

model checkingreversible computationconcurrent systemtemporal logic of actions

Mathematics Subject Classification ID

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

Uses Software

• TLA
• PEPA

Cites Work

• The existence of refinement mappings
• On separating the EREW and CREW PRAM models
• LTL is expressively complete for Mazurkiewicz traces
• Reversing steps in membrane systems computations
• Reversing algebraic process calculi
• The PlusCal Algorithm Language
• A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway
• Reversing Higher-Order Pi
• A Compositional Semantics for the Reversible p-Calculus
• CONCUR 2004 - Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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