Colored Petri nets offer a compact and user friendly representation of the traditional Place/Transition (P/T) nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.
Timed CPN model of SMC controller communication subsystem is described. SMC controller operates as central unit in a small distributed control-and-measurement system from LUMEL Zielona Góra. SMC is programmed in ST language available in CPDev design environment. Implementation of the communication subsystem involves communication tasks created during the design stage and executed by SMC taking into account priorities and timeouts.
PL
Opisano model podsystemu komunikacyjnego sterownika SMC, opracowany w czasowych kolorowanych sieciach Petriego. SMC, produkowany przez LUMEL Zielona Góra, przeznaczony jest do działania jako jednostka centralna w niewielkich, rozproszonych systemach kontrolno-pomiarowych. SMC programowany jest w języku ST w środowisku projektowym CPDev. Implementacja podsystemu komunikacyjnego wykorzystuje zadania komunikacyjne tworzone w fazie projektowania i obsługiwane przez SMC cyklicznie, w zależności od priorytetów.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.