An enumerative approach for analyzing Time Petri Nets

Bernard Berthomieu (1) , Miguel Menasche (1)

1 LAAS - Laboratoire d'analyse et d'architecture des systèmes

This paper is concerned with specifying and proving correct systems in which time appears as a parameter. We model such systems via Merlin's Time Petri Nets. An enumerative analysis technique is introduced for these nets based on the computation of a set of state classes and a reachability relation on the set. State classes are defined in the text and an algorithm is provided for their enumeration. This enumerative approach allows us to derive a finite representation of their behavior for a large family of Time Petri Nets. The analysis method is illustrated by the analysis of a communication protocol.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Bernard Berthomieu, Miguel Menasche. An enumerative approach for analyzing Time Petri Nets. IFIP 9th World Computer Congress, Sep 1983, Paris, France. ⟨hal-04187100⟩