Deliverable D13
Deliverable D13
Timed and Stochastic Well-formed colored nets (SWNs) have been introduced as a good modeling tool for complex systems with inherently high degrees of symmetry. Analysis and simulation algorithms allow the automatic exploitation of model symmetries to improve their efficiency. Fairly strong constraints are posed over the color definition syntax in order to support such automatic symmetry exploitation as compared to other high level Petri net formalisms, so that an assessment of their actual usability in real cases is needed. Inspite of their aggregation power, SWNs sometime yield models whose underlying Markov Chain (MC) is still too large to be analyzed on conventional workstations. In these cases, bounds on the performance indexes of the model can be computed using the concept of quasi-lumpable Markov chains, i.e., a MC that can be made lumpable by relatively small perturbation to the transition rates. In this paper we discuss the solution techniques that are peculiar of the Markovian analysis of SWNs. In particular, the different types of state aggregations that can be applied either at the net level or during the generation of the state space are presented. Some of these methods have been implemented within the GreatSPN modelling and evaluation package leading to its extension to the colored version. The extension of the tool is also described. Several models of parallel computer architectures are included in order to show not only that the formalism is adequate for this class of applications, but also how the different types of symmetries can be mapped into the allowed specification formalism. From this set of case studies we conclude that SWNs are an ``intermediate level'' formalism, closer to the application domain than P/T nets, yet requiring some ingenuity and experience from the modeler in order to exploit their (high) potential.