2017/05/05 by Remigiusz Wisniewski, Remigiusz Wiśniewski, Andrei Karatkevich +5
Computer Science · #Formal Methods in Verification #Petri Nets in System Modeling #Real-Time Systems Scheduling
paper · doi:10.1109/tcst.2017.2692204
openalex publication_date 2017/05/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
This paper shows a novel prototyping technique for concurrent control systems described by interpreted Petri nets. The technique is based on the decomposition of an interpreted Petri net into concurrent sequential automata. In general, minimum decomposition requires runtime that is exponential in the number of Petri net places. We show that in many cases, including the real-life ones, the minimum decomposition problem can be solved in polynomial time. The proposed method allows implementing a concurrent control system using minimal number of sequential components, which requires polynomial time and can be applied to most of the considered cases. The presented concept is illustrated by a real-life industrial example of a beverage production and distribution machine implemented in a field programmable gate array.