Pre- and Post-agglomerations for LTL Model Checking

12 years 3 months ago
Pre- and Post-agglomerations for LTL Model Checking
One of the most efficient analysis technique is to reduce an original model into a simpler one such that the reduced model has the same properties than the original one. G. Berthelot defined in this thesis some reductions of Petri nets that are based on local structural conditions and that simplify significantly the net. However, the author focused only on the preservation of classical properties (such that liveness, boundedness, ...) that are not necessarily the most useful in practice. In this paper, we prove that two of these structural reductions (the pre and post transitions agglomerations) preserve also a large set of properties expressed in linear-time temporal logics under simple conditions.
Denis Poitrenaud, Jean-François Pradat-Peyr
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where APN
Authors Denis Poitrenaud, Jean-François Pradat-Peyre
Comments (0)