Wojciech Penczek

Model-Checking
for a Fragment of Event Structure Logic

820

Abstract

A finite representation of the event structure corresponding to the behaviour of a program is suggested. The algorithm of linear complexity using this representation for model checking of the formulas of Discrete Event Structure Logic without past modalities is given. A method of building finite representations of event structures in an efficient way by applying partial order reductions is provided.