Skip to Main content Skip to Navigation
Conference papers

Animating TLA Specifications

Yassine Mokhtari 1 Stephan Merz
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : TLA (the Temporal Logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, with the intent to facilitate the communication between domain and solution experts in the design of reactive systems.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:41:32 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099016, version 1



Yassine Mokhtari, Stephan Merz. Animating TLA Specifications. International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, pp.92--110. ⟨inria-00099016⟩



Record views