Technical Report CS713

Authors: H. De-Leon and O. Grumberg
PDF - RevisedCS0713.revised.pdf

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification then the original system satisfies it as well. The specification language RTL is a branching-time version of the real-time temporal logic TPTL presented in [AH89]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage of RTL.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1992
To the main CS technical reports page

Computer science department, Technion