*For the most recent entries see the
Petri Nets Newsletter.*

## A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols.

Gallasch, Guy;
Billington, Jonathan
In:
Valmari (Ed.) , Springer-Verlag: *LNCS, Vol 3925: Model Checking Software*, pages 201-218.
2006.

Abstract:
The Stop-and-Wait protocol (SWP) has two (unbounded) parameters: the
maximum sequence number (MaxSeqNo) and the maximum number of
retransmissions (MaxRetrans). This paper presents an algebraic method for
checking such a system requires considering an infinite family of models,
one for each combination of parameter values, and thus an infinite family
of state spaces (reachability graphs). These reachability graphs are
represented symbolically by a set of algebraic formulas in MaxSeqNo and
MaxRetrans. This result is significant as it provides a complete
characterisation of the infinite set of reachability graphs of our SWP
model in both parameters, allowing properties to be verified for the
infinite class. Verification of a number of properties is described.

Keywords:
Stop and Wait Protocols: Infinite Families of Systems: Parametric
Reachability Graphs: Coloured Petri Nets.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*