On the Logic of TLA+
Stephan Merz
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
Text on Computing and Informatics
TLA+ is a language intended for the high-level specification of reactive, distributed, and in particular asynchronous systems. Combining the linear-time temporal logic TLA and classical set-theory, it provides an expressive specification formalism and supports assertional verification.
Publié le : 2012-01-26
Classification:  Temporal logic; reactive systems; specification; verification; refinement 
@article{cai460,
     author = {Stephan Merz},
     title = {On the Logic of TLA+},
     journal = {Computing and Informatics},
     volume = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai460}
}

Stephan Merz. On the Logic of TLA+. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai460/