Technical Reports

A List by Author: Jiøí Sochor

e-mail:

sochor(a)fi.muni.cz

home page:

https://www.fi.muni.cz/usr/sochor/

Partial Order Reduction for State/Event LTL

by Nikola Bene¹, Lubo¹ Brim, Ivana Èerná, Jiøí Sochor, Pavlína Vaøeková, Barbora Zimmerová, July 2008, 21 pages.

FIMU-RS-2008-07. Available as Postscript, PDF.

Abstract:

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.

The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.

Object-oriented Graphics Architectures for Global Illumination

by Jiøí Sochor, Radek Oslej¹ek, December 1998, 17 pages.

FIMU-RS-98-08. Available as Postscript, PDF.

Abstract:

The paper presents several examples of object-oriented graphics architectures derived from OO Testbed for Global Illumination. A new architecture based on explorer-with-map paradigm is described and projected on serial HW architecture of Cohen&Demetrecsu.