Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4951859 | Science of Computer Programming | 2016 | 17 Pages |
Abstract
We propose a method to exploit the symmetries of a real-time system represented by a Time Petri net for its verification by model-checking. The method handles both markings and timing constraints; it can be used in conjunction with the widely used state classes abstraction, a construction providing a finite representation of the behavior of a Time Petri net preserving its markings and traces. The approach has been implemented and experiments are reported.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat,