|
 
|
[PP00] Pre and Post-Agglomerations and LTL Model Checking
Conférence Internationale avec comité de lecture : January 2000, Vol. 1825, pp.387-408,
motcle:
Résumé:
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 of the net and
that simplify significantly the net. However, the author focused only
on classical properties (such that liveness, boundedness, ...) that are
not necessarily useful in practice.
In this paper, we prove that two of these structural reductions
(the pre and post transitions agglomerations) preserve a large set
of properties expressed in linear temporal logics.
Commentaires:
pages 387-408.
BibTeX
| @inproceedings { | |||
| PP00, | |||
| title | = | "{Pre and Post-Agglomerations and LTL Model Checking}", | |
| author | = | " D. Poitrenaud and J. Pradat-Peyre ", | |
| year | = | 2000, | |
| month | = | "January", | |
| volume | = | 1825, | |
| pages | = | "387-408", | |
| note | = | "{pages 387-408.}", | |
| } | |||
