Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specification-and those descriptions then proved correct-even when the complete specification cannot be written as a diagram. We also use the diagrams to illustrate proofs.>
No takes yet. Share an insight, caveat, or question.
Leslie Lamport (1995) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: