Industrial production line modeling and reasoning by petri nets

CNMAI2014-0021 Petri Nets are a widely used formalism to execute and analyze concurrent procedures. It takes advantage of an intrinsic support to parallelism and concurrence as well as of the possibility of intuitive graphical interpretation. It can be used for modeling all the behavior of procedures and tracking resources flow. Petri-PDL is a logic formalism capable of making inferences on Petri Nets even in its concurrent dealings. Besides other works evolving reasoning in concurrent systems or those using Petri Nets, Petri-PDL is a decidable, sound and complete formalism that takes advantage of Petri Nets resources. The inspection method used in a VIN (vehicle identification number) validation does not meet the quality requirements demanded by the market. In some cases reported, the inspection is performed manually, by a visual checking operator, which exposes the company to the risk of commercializing a vehicle with differences between its VIN and the vehicle documentation. Due to the emotional factor and specially fatigue, the inspection should not be performed by a person. It requires a technological tool to assist on the transcription of the validating data to the chassis in order to avoid possible problems. This work presentes a new approach based on Petri Nets using Propositional Dynamic Logics to verify whether the model of a low cost system for validating the data transcribed to a chassis is correct – and therefore efficient.