VERIFICATION OF SQUARE COMMUNICATION GRID PROTOCOLS VIA INFINITE PETRI NETS
MetadataShow full item record
A technique of the linear invariants calculation for infinite Petri nets with the regular structure is presented and studied on the example of square communication grids of an arbitrary size. It is proven that the compulsory buffering of the packets inevitably leads to possible blockings of communicating devices. The structure of complex deadlocks involving an arbitrary number of communicating devices caused by both the cycle of blockings and the isolation is studied.