Towards Safe Navigation by Formalizing Navigation Rules

ABSTRACT: One crucial aspect of safe navigation is to obey all navigation regulations applicable, in particular the collision regulations issued by the International Maritime Organization (IMO Colregs). Therefore, decision support systems for navigation need to respect Colregs and this feature should be verifiably correct. We tackle compliancy of navigation regulations from a perspective of software verification. One common approach is to use formal logic, but it requires to bridge a wide gap between navigation concepts and simple logic. We introduce a novel domain specification language based on a spatio-temporal logic that allows us to overcome this gap. We are able to capture complex navigation concepts in an easily comprehensible representation that can direcly be utilized by various bridge systems and that allows for software verification.

KEYWORDS: Safety of Navigation, Colregs, Collision Regulations, Navigation Rules, Spatio-temporal Logics, Bridge Systems, Domain Language, Artificial Intelligence (AI)

REFERENCES

Aiello, M., Pratt-Hartmann, I. & van Benthem, J. (ed.) 2007. Handbook of Spatial Logics. Berlin: Springer.

Banaś P., Breitsprecher M.: Knowledge Base in the Interpretation Process of the Collision Regulations at Sea. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 5, No. 3, pp. 359-364, 2011

Blackburn, P., van Benthem, J. & Wolter, F. (ed.) 2006. Handbook of Modal Logic, New York: Elsevier.

Cohn, A. & Renz, J. 2007. Qualitative Spatial Representation and Reasoning. In van Harmelen, F., Lifschitz, V. & Porter, B. (ed.), Handbook of Knowledge Representation, 551–596, New York: Elsevier.

Dreyer, R. 2012. Sportküstenschifferschein & Sportbootführerschein See (in German). Bielefeld: Delius Klasing.

Dylla, F. 2009. Qualitative Spatial Reasoning for Navigating Agents, In Gottfried, B. & Aghajan, H. (ed.), Behaviour Montoring and Interpretation—Ambient Assisted Living. Amsterdam: IOS Press.

Kemp J.F.: The Colregs and the Princess Alice. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 1, No. 1, pp. 57-61, 2007

Kemp J.F.: Behaviour Patterns in Crossing Situations. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 3, No. 1, pp. 75-79, 2009

Kreutzmann, A., Colonius, I., Wolter, D., Dylla, F., Frommberger, L. & Freksa, C. 2012. Temporal logic for process specification and recognition. Intelligent Service Robotics. 1–14.

Kolendo P., Śmierzchalski R., Jaworski B.: Experimental Research on Evolutionary Path Planning Algorithm with Fitness Function Scaling for Collision Scenarios. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 5, No. 4, pp. 489-495, 2011

Kwiatkowska, M., Norman, G. & Parker, D. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Gopalakrishnan, G. and Qadeer, S. (ed.), Proceedings of 23rd International Conference on Computer Aided Verification, Berlin: Springer.

Mohamed-Seghir, M. (2012). The branch-and-bound method and genetic algorithm in avoidance of ships collisions in fuzzy environment. Polish Maritime Research, 19(S1):45–49.

Moratz, R. (2006). Representing relative direction as a binary relation of oriented points. In Brewka, G., Coradeschi, S., Perini, A. & Traverso, P. (ed.), European Conference on AI 2006. Amsterdam: IOS Press.

Necula, G. C. (1997). Proof-carrying code. In P. Lee, F. Hengelein & N.D. Jones (ed.), Proceedings of the 24th ACM SIGPLAN—SIGACT Symposium on Principles of Programming Languages, POPL ’97. New York: ACM.

Pietrzykowski Z., Uriasz J.: Knowledge Representation in a Ship's Navigational Decision Support System. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 4, No. 3, pp. 265-270, 2010

Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 46–57. Los Alamitos: IEEE Computer Society.

Smierzchalski, R. & Michalewicz, Z. (2000). Modeling of ship trajectory in collision situations by an evolutionary algorithm. In Trans. Evol. Comp, 4(3):227–241.

Szłapczyński R.: Evolutionary Sets of Cooperating Trajectories in Multi-Ship Encounter Situations - Use Cases. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 4, No. 2, pp. 191-196, 2010

Wolter, D., Kreutzmann, A. & Dylla, F. (2011). Rule-Compliant Navigation With Qualitative Spatial Reasoning, In Schlaefer, A., Blaurock, O. (ed.), Robotic Sailing—Proceedings of the 4th International Robotic Sailing Conference, 141–155, Berlin: Springer.

Wolter, D. & Wallgrün, J. (2012). Qualitative Spatial Reasoning for Applications: New Challenges and the SparQ Toolbox. In Hazarika, S. (ed.), Qualitative Spatio-Temporal Representationand Reasoning—Trends and Future Directions, 336–362. Hershey: IGI Global.

Citation note:

Kreutzmann A., Wolter D., Dylla F., Lee J.H.: Towards Safe Navigation by Formalizing Navigation Rules. TransNav, the International Journal on Marine Navigation and Safety of Sea Transportation, Vol. 7, No. 2, doi:10.12716/1001.07.02.01, pp. 161-168, 2013

BibTeX EndNote

File downloaded 1641 times