CAESAR Reference Manual

Hubert Garavel

Rapport SPECTRE, C18, Laboratoire de Génie Informatique - Institut IMAG, Grenoble, November 1990

April 2016: This document is now obsolete. Its contents have been moved (and updated) to three manual pages of CADP, the CAESAR, CAESAR.ADT, and LOTOS manual pages.


This report describes a translator from LOTOS to both interpreted Petri nets and finite state automata. This tool provides a way to verify LOTOS programs by model-checking. It applies to a large subset of LOTOS (including value expressions) and can be used in conjunction with other existing tools based on graph equivalences and/or temporal logics.

32 pages (obsolete document)