Modeling Synchronization Problems: From Composed Petri Nets to Provable Linear Sequents

Ján Perháč, Daniel Mihályi, Valerie Novitzká · Acta Polytechnica Hungarica · 2017

Component-based programming has become a popular and frequently used method for software development, prepared from independent components by a composition.Our paper presents an illustration of how a composition of components can cause the emergence of new problems that should be solved, in order to obtain the desired results.We introduce a transformation of Petri nets to corresponding provable sequents of linear logic and then we show how a composition of simple Petri nets causes arising of synchronization problems.Transformation to provable linear sequents that ensures a verified behavior for such composed systems.

Read the paper · More papers on PaperTik