Modular Petri net modeling of the Spanish health system

This paper presents a modular Petri net approach for modeling a health system. In particular, the Spanish national health system is considered as case study. After a global description of the health system structure, it is shown that it can be composed by different modules with inputs and outputs. Each module can be modeled separately and the procedure consists in two steps: (1) model the medical protocols as state-machine Petri nets and (2) add the (shared) medical resources. The global model is obtained by composing these modules by fusing the input and output places and adding information on the population. It is proved that by following these procedure, the obtained Petri net system is a S⁴PR. Finally, it is shown how the model can be exploited in order to check different properties of the system.