Performance evaluation and model checking in systems modeled as Hybrid Petri nets

In this paper, an approach for evaluating the performance measures for process description and model checking based on structural properties and constraint information for typical liquid level processes is discussed. For this purpose, a typical three tank system is considered and modeled using Hybrid Petri nets. Based on the model, a Markovian structure is defined and developed. Performance measures such as arrival distance, throughput distance and queue length for places and service distance, service time and utilization for transitions are determined for the developed Markovian structure under various case studies. Finally, conditions for model checking based on constraint information are derived analytically.