Formal Verification of Vessel Scheduling Using Probabilistic Timed Automata

The effective management of time delays in vessel scheduling within the vessel transportation industry poses a complex challenge, as potential delays can lead to shifts in planned routes and increased costs. This paper addresses this issue by proposing a formal probabilistic model for vessel scheduling that considers time constraints and accommodates relevant risk factors contributing to delays. Utilizing Probabilistic Timed Automata (PTAs), our model captures distributed random delays from key risk factors such as weather conditions, mechanical engine readiness, and port congestion in the target vessel scheduling. We then translate PTAs model representation of the target vessel scheduling into PRISM code. Subsequently, the PRISM model checker is employed to simulate and verify the vessel scheduling model’s compliance with specified behavioral properties expressed in Probabilistic Computation Tree Logic (PCTL). This approach facilitates a comprehensive analysis of time-related aspects, aiding in both planning and mitigation of associated risk impacts.