Animating TLA specifications

DOI10.1007/3-540-48242-3_7MaRDI QIDQ4938420zbMATH OpenFDO

Authors Yassine Mokhtari, Stephan Merz

Publication date 23 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48242-3_7

zbMATH Keywords

linear temporal logicreactive systemstemporal logic of actions

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 910717
• scientific article; zbMATH DE number 1390334
• scientific article; zbMATH DE number 3982506
• Abstract animator for temporal specifications: Application to TLA
• scientific article; zbMATH DE number 2185692

Cited in

(5)

• scientific article; zbMATH DE number 2185692 (Why is no real title available?)
• scientific article; zbMATH DE number 1949599 (Why is no real title available?)
• scientific article; zbMATH DE number 910717 (Why is no real title available?)
• Formal specification and verification
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications

This page was built for publication: Animating TLA specifications

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