161
1 INTRODUCTION
Navigation regulations such as the official collision
regulations of the International Maritime
Organization (IMO Colregs) are an essential
instrument for safety in navigation. Some situations
may require further rules and general
recommendations may be implemented to foster
sensiblenavigationbehavior,e.g.,withrespecttofuel
efficiency.Allthese
regulationsneedtobeobeyed—
which can be a very demanding task in complex
situations. By augmenting bridge systems such as
ECDIS and autopilots to understand navigation
regulations we can supportcrews, reducing the risk
ofregulationviolations.Tostartwith,thisrequiresan
implementation of navigation regulations that is
known
tobecorrect.
We argue for a declarative, logic‐based approach
to represent navigation regulations. Logics offer
precise semantics for reasoning and they build a
common basis for software verifica tion. The use of
suchformalmethodsduringsoftwaredevelopmentis
acommonrequirementforhigherstandardsofsafety‐
critical software.
However, logics are usually based
onprimitiveconceptsanditrequiresoverlycomplex
statements to represent everyday concepts such as
“oncomingtraffic”.Trying to formalizea non‐trivial
set of navigation regulations with a simple logic
inevitably leads to incomprehensible formalizations
thatareerror‐pronetoalignwithnavigationsoftware,
rendering
effectiveness of the overall approach
questionable.
Thecontributionofthispaperistoshowhowthe
oppositionofprimitiveconceptsinlogicontheone‐
handandabstractconceptsinnavigationregulations
ontheotherhandcanbeovercome.Tothisend, we
develop an abstract logic, a so‐called
qualitative
spatio‐temporallogic,whichcanadequatelyrepresent
navigation concepts. They allow comprehensible
representations specifically suited for navigation
problems.Qualitativespatiallogicsasstudiedinthe
fieldof Artificial Intelligence (AI) are acknowledged
Towards Safe Navigation by Formalizing Navigation
Rules
A.Kreutzmann,D.Wolter,F.Dylla&J.H.Lee
CognitiveSystemsGroup,UniversityofBremen,Bremen,Germany
ABSTRACT:Onecrucialaspectofsa
f
enavigationistoobeyallnavigationregulationsapplicable,inparticular
thecollisionregulationsissuedbytheInternationalMaritimeOrganization(IMOColregs).Therefore,decision
supportsystemsfornavigationneedtorespectColregsandthisfeatureshouldbeverifia blycorrect.Wetackle
compliancyofnavigationregulationsfromaperspectiveofsoftwareverifica tion.
Onecommonapproachisto
use formal logic, but it requires to bridge a wide gap between navigation concepts and simple logic. We
introduceanoveldomainspecificationlanguagebasedonaspatio‐temporallogicthatallows ustoovercome
thisgap.Weareabletocapturecomplexnavigationconcepts
inaneasilycomprehensiblerepresentationthat
candirectlybeutilizedbyvariousbridgesystemsandthatallows forsoftwareverification.
http://www.transnav.eu
the International Journal
on Marine Navigation
and Safety of Sea Transportation
Volume 7
Number 2
June 2013
DOI:10.12716/1001.07.02.01
162
fortheirabilitytograspconceptsofhumancognition.
We thus can connect formal logic to concepts of
human cognition, obta ining formalizations with
precise logic semantics that can be understood and
even adapted by navigators, not only by computer
scienceexperts.Theseformalizationsareuniversalin
the sense that the
very same representation can be
used in a variety of tasks: to display regulation
violations in ECDIS, to enforce rule‐compliant path‐
planning in autopilots, and above all to support the
softwaredevelopmentprocessbyverification.
This paper is organized as follows. We give
references to related work, then we
present our
qualitative spatial logic. We outline how navigation
formalizations in this logic can be integrated with
various navigation tasks using logic‐based software
tools. Finally, we show how logic reasoning
developed for our logic can be employed in
verificationand to revealproblemswith software or
withtheregulationsthemselves.
Thepaperconcludes
byadiscussionandoutlooksection.
2 BACKGROUND
Sophisticated bridge system can be considered as
decision support systems (DSS) as they aim to
support crew in navigation decisions. Various
computer science techniques have been applied to
devise such systems. Smierzchalski & Michalewicz
(2000) and Szłapczynski (2010)
demonstrate how
evolutionary algorithms can be applied for collision
freenavigationevenincaseofmulti‐shipencounter.
Arelatedapproachhasbeen pursuedbyMohamed‐
Seghir (2012) using a combination of branch‐and‐
bound and genetic algorithms.Both approaches aim
to determine a cost‐optimal path, but they cannot
guarantee
torespectofficialregulations,i.e.,itcanbe
illegal and even dangerous to follow a path
computed. It is thus necessary to integrate a
representationof Colregs inorder to obtaindecision
support that complies to official regulations. As
reported by Pietrzykowski & Uriasz (2010), various
approaches to represent knowledge
contained in
navigation regulations like Colregs have been
applied.Theirapproach aims at combining different
techniques, but does not handle situations in which
multiplevesselsaremutuallysubjecttoregulationsat
the same time. By contrast, Banas & Breitsprecher
(2011)arguefortheuseoflogicrule‐basedsystemsas
framework
for representing navigation regulations.
Theyclaimlogictoprovidethebestmeanstotackle
requirements on a DSS for navigation identified,
namely reproducible and verifiable results,
integration of informal knowledge, easy update or
extensionofknowledge,regulationprioritization,and
comprehensibility of the representation. Indeed, the
use of formal methods based
on logic is a common
means to foster reliability of safety‐critical software
likeaDSSfornavigation.Weadoptthemotivationof
Banas & Breitsprecher to employ logic for
formalization. Our primary focus is to adequately
capture the complex spatio‐temporal concepts
involved in navigation regulations. We improve on
previous
work by devising an advanced logic
framework that incorporates sophisticated spatial
reasoning. This allows us to better meet the
aforementioned criteria for bridge systems, in
particularwithrespecttothesafety‐criticalaspectof
verifiability of the software and with respect to
comprehensibilityoftherepresentation.
Developingaformalizationof
Colregsone has to
face several design criteria which are somewhat
competing. Any formalization of Colregs has to
bridgethegapfromtheofficialregulationsdenotedin
natural language to a verified formal framework on
whichthesystemisbased.Acommonapproachisto
developadomainlanguagewhichabstracts
fromthe
formalframework andoffersconceptsandtechniques
close to the application domain. Of course, the
mappingfromdomainlanguagetotheformalsystem
must be transparent and verifiable itself to avoid
introducingerrorsinthetranslation.Tothisend,our
approach utilizes a formal framework that already
incorporates
many abstract concepts necessary to
represent navigation regulations. This allows us to
obtainatransparentmappingfromdomainlanguage
to underlying logic. Moreover, bridge systems can
benefitfromtheunderlyingformalframework,given
the framework provides sophisticated reasoning
mechanisms that are capable of tackling navigation
tasks. As we demonstrate, reasoning methods
of
qualitative spatio‐temporal logics are well‐suited to
meetthisgoal.
2.1 Qualitativespatio‐temporallogics
Qualitative spatial and temporal reasoning is an
established field of research dealing with
representation and reasoning about spatio‐temporal
knowledgein anabstracted, i.e. qualitative,manner.
Qualitative approaches are symbolic and symbols
serve
to represent concepts like “left” rather than
usingnumerical values that measure directions. The
aim of qualitative approaches is to capture the
important distinctions that make a difference for a
taskathandwhileabstractingfromirrelevantdetails.
Qualitative spatial and temporal reasoning
provides different methods of reasoning, most
notably methods
that can decide whether a given
symbolic description of a scene is consistent, i.e.,
whetheritcanberealizedbyaphysicalconfiguration.
For example, the three temporal statements about
events A,B, and C, namely “A occurs before B”, “B
occurs before C”, and “C occurs before A”, are not
jointlyrealizableastimeevolveslinearly.Qualitative
reasoning provides techniques to reason about
variousaspectofspaceandtime(Cohn&Renz,2007)
and specialized reasoning tools are available, e.g.,
SparQ(Wolter&Wallgrün,2012).
Recently, qualitative approaches have been
studied in conjunction with logics, thus coining the
term spatio‐temporal
logic. These logics are formed
by “any formal language interpreted over a class of
structuresfeaturinggeometricalentitiesorrelations”
(Aielloetal.,2007,Chapter 1).The logic itselfis not
restricted,i.e.,itmaybeafragmentoffirstorderlogic
or any higher‐order logic. In this paper
we are
concerned with a combination of a modal logic of
linear time with a qualitative approach to
representing directional knowledge presented in
Section3.3.
163
3 FORMALIZINGNAVIGATIONREGULATIONS
FORUSEINBRIDGESYSTEMS
The key question in designing an appropriate
formalizationiswhataretheindividual components
that make up a set of navigation regulations? Since
weformalizeasafety‐criticalsystemwemustensure
that these components need a clear linkage to the
primitivesintheunderlyinglogic.
At the core of a regulation we can identify the
navigation behavior. Navigation behaviors come in
twoflavors.Firstly,wehavenavigationbehaviorsas
instructed behaviors: the regulation defines which
actions are allowed to perform. Secondly, we find
navigation behaviors setting the context in which
a
specific regulation is applicable, for example, with
respect to the vessels’ relative course. While both
flavors share many commonalities, there exist
decisive differences. Onemust ensurethat acontext
descriptioncan be evaluated at any point in timeto
allowinstructedbehaviorstobeperformedassoonas
aregulation
isapplicable.If,bycontrast,thecontext
wouldbeallowedtorefertothefuture,onecouldnot
tell whether one’s current situation matches the
context. We say that a context is a discernible
navigation behavior, i.e., a pattern of actions and
events that can be recognized by an observer.
Analogously, instructed behaviors are restricted to
only talk about future actions. In other words,
regulationsareoftheform“ifyouapproachtheport,
reducespeed”ratherthan“ifyoucrashedintoaquay
wall,youshouldhavereduced speedinfirstplace”.
Althoughcontextandinstructedbehavioraredistinct,
we
canapplyacommonframeworkofrepresentation
tobothofthem.
Assecondcomponentofregulationsweidentifya
valuation of liability. As soon as a regulation is
applicable, its instructed behavior defines which
actionsareallowed.Asapplicabilityofaregulationis
subjecttochange,weintroducetheterm
valuationof
liabilitytoindicatewhethera navigationbehavioris
applicable and how it relates to competing
regulations. The Colregs regulations have different
liabilityandtheirliabilitymightchangedependingon
other regulations currently applicable. For example,
the regulations state that (Rule 13,d): “Any
subsequentalterationofthebearingbetweenthe
two
[overtaking] vessels shall not make the overtaking
vessel a crossing vessel withinthe meaningof these
rulesorrelieveherofthedutyofkeepingclearofthe
overtakenvesseluntilsheisfinallypastandclear.”In
this example, certain behaviors (being a crossing
vessel)aretemporarilyforbidden
whilevesselsarein
the context of overtaking one another. While
inhibitingcertainbehaviorscaneasilybeformalized,
a true modeling of rule precedence and conflict
resolutionisachallengingaspectinitsownrightand
outside the scope of this paper. For time being, we
simplysaythatavaluation
maytakeeitherthevalue
applicableornotapplicable.
Insummary,asetofnavigationregulationscanbe
formalized as a mapping from the set of navigation
behaviors describing the context to a valuation of
liability of navigation behaviors that state which
behaviorsareallowedtotakeplace.Ourterminology
isclosetothatofrulesintheclassicalsenseoflogicin
computer science: an antecedence leading to
consequence.
Throughout the remainder of this paper we use
Colregs Rule 12,a,i (sailing vessels) as a running
example to illustrate our approach. Let us start by
looking at the example of how Rule 12 can be
formalizedinourapproachshowninFigure1.
officialrule(naturallanguage):
When two sailing vessels are approaching one
another,soastoinvolveriskofcollision,oneofthem
shallkeepoutofthewayoftheotherasfollows:
(i) when each has the wind on a different side, the
vessel which hasthe wind on
the port side shall
keepoutofthewayoftheother.
formalization(modelinglanguage):
(rule12_i
:context (AND (is_sailing_vessel ?X)
(is_sailing_vessel ?Y)
(is_approaching ?X ?Y)
(is_approaching ?Y ?X)
(COULD (collide ?X ?Y))
(wind_on ?X PORT)
(wind_on ?Y STARBOARD))
:behavior (AND (give_way ?X)
(keep_course ?Y)))
Figure1. From Colregs (top) to regulation formalization
(bottom).Theformalizationdescribescontextandrequired
behaviorin a declarative manner;?Xand ?Y are variables
thatstandforvessels.
As can be seen, we have chosen a simple syntax
using parentheses for grouping. The context and
instructedbehaviorpartofaregulationareindicated
byrespectivelabels.Theformalizationonlyexplicitly
states one case of having “the wind on a different
side” which eases readability, as the other case is
symmetricalandachievedbyswappingthevariables.
Observethattheformalizationutilizestermslike “is
approaching”or“keepcourse”thatareverycloseto
thenaturallanguageusedinColregs.Atthispointit
is important to note that these terms are logic
concepts which need a clear grounding in
spatio‐
temporal knowledge about the world. Assuming a
reasonable interpretation of these terms, the
formalization can easily be checked against the
official Colregs by any domain expert, e.g., trained
helmsmanor navalexpert.Let us now look intothe
technicaldetailsofhowtheseconceptsaregrounded
in the logic and
how logic reasoning can be
performed.
3.1 Aspatio‐temporallogicforformalizingnavigation
behaviors
We give a brief introduction of the modal logic
underlyingourformalization. Since the key focus of
this paper is not discussing the logic itself but to
demonstrate its applications as well as the domain
dependentlanguageestablishedontopofit,weonly
introducethelogicinformally.
Forourapproachwedevelopedaso‐calledmulti‐
modal logic. Like any modal logic, this logic is a
164
generalization of propositional logic which is
equipped with the concept of different states, also
called worlds. Truth of a formula is evaluated with
respect to a specific state. For example, the logic
primitive“sailsSet”maybetrue inone state, but
falseinanother.Allpossiblestatesconstitute
theso‐
calleduniverseandindividualstates areconnectedby
specificrelationscalledmodals.Typically,auniverse
isassumedtobegivenandtobefinite(Blackburnet
al.,2006,Chapter1).Auniverseandasetofmodals
togetherwiththeinformationaboutwhichstateofthe
universemakes
whichlogical primitivestrue forma
modelofamodallogic.
A prominent example for a modal is time: one
statemayrepresentthecircumstancesatatimepoint
t
i and the connected state talks about the next
moment in time t
i+1. As navigation regulations are
groundedintimeandspaceweemploytwomodals
(thus we have a multi‐modal logic): one modal
capturesthecourseoftimeandanotheronecaptures
possiblespatialchanges.Thespatialmodalwillallow
us to talk about possible changes of the states and,
e.g.,
to express the possibility of collision as a logic
primitive.Technicallyspeaking,weadopttherelation
of conceptual neighborhood defined in qualitative
spatial reasoning; two states are conceptually
neighboredifonestatecanbecontinouslychangedto
another(Dylla,2009).Themodelforourlogicisthus
a set of
such states along with their temporal
ordering,spatial structure, andvaluation of all logic
primitives. Essentially, our logic is a spatially
enhanced generalization of the well‐established
LinearTemporalLogic(Pnueli,1977).
Forconvenience,wewrite,e.g.,sailsSet(X),to
denotethelogicprimitiveholdingthetruthvaluethat
correspondsto
whethervesselXhassails setornot.
Returningtoourpreviousexample(Rule12i),itcan
bewritteninlogicnotationasfollows:
(1 )
,:
,,(1)
,(1)
,,(1)
(1 )
Sailboat X Sailboat Y a
XY Vessels
A
pproaching X Y Approaching X Y b
cn Collsion X Y c
WindOn X port WindOn Y starboard d
GiveWay X KeepCourse Y e
Notethatourlogicisalreadyclosetothemodeling
language;sowemeetthedemandofeasytranslation
fromdomainlanguageto logic. Inthisexamplecn
in line 1c stands for a conceptual change which can
leadintoastatewhereXandYcollide.Theinstructed
behavior (line 1e in the formula) is written as
implicationofthepreconditions1a–1d.Alsonotethat
some spatial relations such as Approaching used
aboveareinfactindependentformulasthemselvesas
we will explain in the following. As a regulation is
applicable to all vessels, the simple logic form
“context
instructed behavior” needs to be stated
explicitlyforalllogicprimitivesrepresentingvessels.
Thisis achieved by combining sub‐formulas forany
choice of X and Y by the logic conjunction “or”. By
buildingamodelinglanguageatopthislogiclayerwe
canensurethatallregulationformalizationsadhere
to
thispatternoflogicformulas.
3.2 Adomainlanguagefornavigationregulations
Inthissectionweexplainhowourdomainlanguage
isbuildatopthespatio‐temporallogicoutlinedabove.
We describe how the key notions of context and
instructed behavior are expressed and how spatial
andtemporalknowledgecan
berepresented.
Thesetof primitive symbols used bythelogic is
divided, identifying the subset of discernible
primitives. Discernible primitives can directly be
observedbyothers(likesailsSet(X),forexample)
whereas other primitives may not. We employ this
distinction such that it can be checked whether a
navigation behavior
can be recognized by
observation: specifications of navigation behaviors
allowforrecognitioniftheyonlyinvolvediscernible
primitives.Thecontextcomprisesasetofnavigation
behaviours. In order to decide whether a context
formalization matches a given situation we require
the context to only involve discernible behaviours.
Moreover, formalization of
contexts is restricted to
onlytalkaboutnow,thepast,andthingspossiblein
future.Thiscaneasilybeaccomplishedbyrestricting
the set of modal operators allowed in the
formalization.Thus, we inhibitthe use ofuniversal‐
qualifiedexpressionsinthispartoftheformalization.
Withrespecttoinstructedbehavior
thereisonlyone
requirement:itmustnotrefertopastactions.Thisis
also achieved by disallowing the respective modal
operatorsintheformula.Allinallweobtainthatall
parts of a regulation are logic formulas, each class
withaspecificallyrestrictedsyntax.
,:
X
Y context instructed behavior
In summary, our system translates all rules into
thepatternasshownintheprevioussection.Thekey
feature of our approach is its seamless integration
withqualitativespatiallogicsthatallowsustodefine
arichrepertoireofspatialrelations.
3.3 Spatio‐temporalprimitives
InformalizingColregsitis
essentialtoformalizethe
manifold spatio‐temporal concepts referenced in the
regulations. The key building block of the spatial
formalization is a set of qualitative spatial relations
that capture directional information as presented in
(Wolteretal.,2011).Thismodeling is asector‐based
model presented in (Moratz, 2006) (see Figure
2)
which allows us to derive most important spatial
concepts. Essentially, the model allows directional
sectorstobedefinedthatarealignedwithrespectto
position and orientation of an observer. While the
number of sectors can be chosen arbitrarily to
accommodate for any desired resolution, we restrict
the presentation
here due to space constraints to
showingonlytheeight‐sectorvariant.Intheexample
showninFigure2(A),thepositionofBisinsector0
withrespectto A and viceversa—A andB arethus
orientedtooneanother.Figure2(B)showshowthe
model can
be used to describe the wind. The vessel
depictedhasthewindofportsideasthewindcomes
fromsector2.Analogously,thesamemodelservesto
state which is the right side to pass by a buoy, see
Figure 2 (C). Here, the white area reresents a
waterway.
165
Figure2.IllustrationformalizingthespatialconceptsunderlyingColregs.
(A) (B) (C)
Figure3.Depictionofcollsionavoidancepatterns(i.e.,interpretationsoftherules)forpairofvesselsasfoundintextbooks
onnavigation.Adashedlineindicatesthatthevesselhastogivewaywhileasolidlinemeansthatthevesselshouldkeep
course.Inthedepictedconfiguration,thesecollision
avoidancepatternsarecontradictingoneanother.
Exhaustingtheexpressivityofatemporallogicwe
can also exploit these spatial relations to define
dynamicnavigationbehavior.Forexample, theterm
“head‐oncourse”canbedefinedbysayingthatatone
time point two vessels are oriented towards one
another(seeabove),whileinthenexttime
pointthey
are still oriented the same way but that both have
advanced towards one another. A’s position at time
pointt
n+1isahead ofwhere Awas attimepointtn,
i.e.,Aatt
n+1iswithinsector0asseenfromAattime
point t
n —see Figure 2 (D) for illustration. It is the
modaloperatorsofatemporallogicthatgrantsusthe
expressivity to relate A’s position between different
pointsintime.
3.4 Modelcheckingwithspatio‐temporallogics
Generallyspeaking,givenamodelMandastatewin
M and a
formulaϕ, the task of model checking in
modallogicistodeterminewhetherwalongwithM
satisfiesthe formulaϕ. Specificallyin the context of
ourspatio‐temporallogic,modelcheckingisthetask
of searching for a sequence of spatio‐temporal
transitions starting with the input state w
of vessels
which makes regualtionϕtrue with respect to the
model M of the spatio‐temporal logic described in
Section 3.1. By means of the combination of model
checkingwithmethodsfromqualitativereasoningwe
are able to reason about whether given input states
arecriticalwithrespecttosafety.
The important feature of modal logics is that
model checking can be realized efficiently. In our
system we utilize the state of the art model checker
PRISM(Kwiatkowskaet al.,2011) whichrequires us
to provide a set of states to check. PRISM either
returns that all states satisfy the given
formula or it
providesuswithacounter‐examplethatfalsifiesthe
formula.
In order to generate all possible states in our
spatio‐temporallogic,qualitativespatialreasoningis
required. For example, consider the statement
“WindOn(X, port) WindOn(X, starboard)” which is
of course not satisfiable. However, from the
perspectiveofapuremodallogicmodelcheckerthe
formulaisjustthesameas“ab”andthusthereis
noreasonwhyaand bshouldnotholdatthe same
time. This is where spatio‐temporal reasoning is
requiredtoruleoutconfigurationswhicharespatially
ortemporally notpossible. To this end, we combine
ourspatio‐temporalreasoningsystemSparQ(Wolter
&Wallgrün,2010)tocheckallcandidatesofstatesfor
theirspatialandtemporalconsistency.
In the following section we show how various
practical problems can be supported with the two
reasoning tasks on the
logic level only: model
checking of formulas in our spatio‐temporal logic
(PRISM) and consistency checking of qualitative
spatialconfigurations(SparQ).
4 REASONINGFORSAFENAVIGATION
We now demonstrate how a formalization of
navigationregulationsservesthreemajorapplications
in bridge systems: recognition of regulation
compliant/violating behavior, regulation compliant
planning,
andverificationofregulationspecifications.
166
4.1 Identifyingregulationcompliancyandregulation
violations
Observingthenavigationbehavioraroundone’sown
position, a natural question to ask is: do all other
vesselscomplywiththeregulationsorissomevessel
violating a regulation? In the domain of safe sea
navigation a system assisting in the detection of
regulationviolatingbehaviorofotherscanbeofgreat
importance to a bridge crew. By alerting the bridge
crewofsuchviolationsappropriatepreparationscan
be made. Assuming that observations of the
surrounding navigation behavior are available (e.g.,
extracted from AIS data or radar), we apply model
checking of the
Colregs formalization to the
observations as follows: From the formalization of
Colregswehavethecorrespondinglogicformulasϕ=
ϕ
1,ϕ2,...,ϕmwhichwecombinebylogicconjunction
“and”:ϕ
1ϕ2...ϕm.Doingsoweobtainasingle
formulaϕthat represents the complete body of
navigationregulations.Observedbehaviorconstitutes
thesetofstates,eachsnapshotoftimedefinesitsown
valuation of logic primitives. For example, at time
pointt
nwehavethatApproaching(X,Y),whileat
the next time point t
n+1 we already have
TurningAwayFrom(X, Y) and it holds that
TurningAwayFrom(X, Y)Approaching(X, Y). If
and only if the set of states obtained from
observations provides a model for the logic formula
ϕ,theobservedbehavioriscompliantwithColregs.If
modelcheckingfails,acounter‐exampleisgenerated.
Thiscounter‐examplefalsifiesϕandidentifieswhich
vessels/actionsdidnotcomplywiththeregulations.
We demonstrated feasibility of this method in a
previous study using a different domain, showing
that the approach works even on noisy and
incomplete sensor data (Kreutzmann et al., 2012). A
smallscalewarehousewassimulatedin
alaboratory
andarobotobservedthewarehouse,gathering partial
observations.Theobservationswerematchedagainst
a set of logistic movement patterns—which can be
consideredasaformofnavigationregulations.Based
on these partial observations, a matching between
real‐worldobservationsandabstractmodelcouldbe
established,i.e., compliancy
with some logisticrules
wasverified.
4.2 Regulationcompliantplanning
Incomplexsituationssuchascrowedwaterwayslike
the English Channel, planning routes that are
regulation compliant but avoid detours can be a
demandingtask.Anautopilotsystemcouldfactorin
routes of other vessels and inhibit the planning
procedureto
outputroutesthatareknownorlikelyto
violate regulations. This enables the vessel to avoid
unnecessary evasive maneuvers and thereby save
fuel. Kolendo et al. (2011) have demonstrated that
randomizedplannersareappropriateforcomputing
collision‐free routes. In (Wolter et al., 2011) we
demonstratedhowthisapproachcan
beadvancedto
ensureregulationcompliantplanning.Weextendthe
state‐of‐the‐art para digm of randomized roadmap
planners to acknowledge navigation regulations as
side constraint in planning. This also augments
existing work on randomized planning by a
verificationcomponent.
In essence, the approach is similar to that of
recognizing regulation
‐violating navigation behavior
discussed above. While planning takes place, all
partial plans considered by the planner are checked
for their regulation‐compliancy using the very same
technique as explained before. Whenever a partial
plan is identified to violate some regulation, it is
discarded and the planner has to search for
an
alternativeroute.
4.3 Verificationofregulationspecifications
When developing safety‐critical software all
development steps should be verifia ble. Moreover,
softwaredevelopersneedtobesupportedtoidentify
problems with their software. To this end, we are
currentlydevelopinga tooltosupporttheverifica tion
ofnavigationsoftwarebasedonthe
formalizationof
navigation regulations. Following the concept of
Proof‐Carrying Code (Necula, 1997), developers can
declare complex assertions in their software. For
example,thecommandtoincreaseenginespeedmay
beguardedbyanassertionthatnoobstacleisinfront
ofthevessel.
Suchatoolisparticularlyvaluable
whenworking
with Colregs‐compliant navigation. Regulations like
theColregshavemostlybeendevelopedwithrespect
todefiningrightofwayforjusttwovesselsatatime.
Thus,incomplexsituationamultitudeofregulations
may be applicable at the same time. Regulations
might even contradict themselves or endanger a
collision if strictly followed. We can support a
knowledge engineer by providing a set of useful
verification methods. Given aset of regulations, our
tool provides the necessary means to check that
regulations are non‐overlapping, i.e., there are no
situations in which different regulations are
contradicting one another. See
Figure 4 for a
screenshot of the tool checking regulations for
problems.Thetoolalsoallowsustocheckwhetherall
(critical) situations are covered by some rule, i.e.,
whether a set of rules is complete. One important
feature of the tool is that it does not only identify
conflicts of
regulations, but it can also generate an
exemplary configuration that triggers the conflict.
Here we use spatial reasoning to generate a
prototypical pictogram that depicts the conflict (see
Figure 4, top right). The position of the boom
indicates direction of the local wind. Conflicting
regulationsareparticularlypresentifan
autonomous
navigation systems implements its own regulations
for special maneuvers, which might interfere with
Colregs. Consider the commonly recommended
evading actions in the form of collision avoidance
patterns as presented in text books for navigation
(Dreyer, 2012, e.g.) as shown in Figure 3. In the
situationdepictedinFigure3,the
vesselontheright
hastheconflictofkeepingcourseandgivewayatthe
sametime.Furtherthetopleftvesselshouldturnport
andstarboardatthesametime.Whileeachcollision
avoidancepattern onitsown is sensible, taking into
account the specific requirements such as wind
direction,theyfailtocombineinsomesituations,e.g.,
multi‐shipencounters. Our toolisabletodetect this
inconsistency solely by reasoning about the rule
definitionsasshowninFigure4.
167
Figure4. Screenshot of the reasoning tool that automatically detects a rule conflict and generates a visualization of the
conflictingsituation.
5 SUMMARYANDOUTLOOK
Adhering to navigation regulations is an important
factor in safe navigation. In order to allow bridge
systemstoincorporateregulationssuchasColregsin
a verifia bly correct manner, a formalization of
navigation regulations is required. In this paper we
show that a spatio‐temporal logic provides a
solid
basisforformalizingColregs.Weproposeaneasyto
understand domain language built atop a spatio‐
temporal logic. Logic reasoning enables automated
tools to check formalizations for correctness. This
enables software developers for bridge systems to
verifytheirsoftware,meetinghighstandardsof safe
softwaredesign.Ourapproachis
applicabletoawide
rangeofnavigationregulationsandcanevenhelpto
develop new ones (see, for example Kemp, 2009).
Thereby,wecanprovide ananswertoalongstanding
problem that “there is no possibility of testing new
proposals [for Colregs] before they are introduced.”
(Kemp,2007).Moreover,aformalization
ofColregsin
our spatio‐temporal logic can also be utilized in
navigationsystemsdirectly:autopilotscandetermine
routesthatareknowntocomplywithColregsorchart
displayscanidentifyviolationsofColregsandsignal
appropriate warnings. We develop a software tool
based on the concept of proof‐carrying
code that
enables software developers to verify their software
with respect to a formalization of Colregs. In future
work, we aim to apply this tool to real navigation
software in order to improve safety in navigation
technology.
ACKNOWLEDGEMENTS
This work is carried out in context of the
Transregional Collaborative Research Center
Spatial
Cognition,projectR3‐[Q‐Shape].Financialsupportby
the Deutsche Forschungsgemeinschaft (DFG) is
gratefullyacknowledged.
REFERENCES
Aiello,M.,Pratt‐Hartmann,I.&vanBenthem,J.(ed.)2007.
HandbookofSpatialLogics.Berlin:Springer.
Banas,P.&Breitsprecher,M.2011.Knowledgebaseinthe
interpretationprocessofthecollisionregulationsatsea.
TransNav—InternationalJournalonMarineNavigationand
SafetyofSeaTransportation,5(3):359–364,Gdynia:Poland.
Blackburn, P.,
van Benthem, J. & Wolter, F. (ed.) 2006.
HandbookofModalLogic,NewYork:Elsevier.
Cohn,A.&Renz,J.2007.QualitativeSpatialRepresentation
and Reasoning. In van Harmelen, F., Lifschitz, V. &
Porter, B. (ed.), Handbook of Knowledge Representation,
551–596,NewYork:Elsevier.
Dreyer, R. 2012. Sportküstenschifferschein &
Sportbootführerschein See (in German). Bielefeld: Delius
Klasing.
Dylla,F.2009.QualitativeSpatialReasoningforNavigating
Agents, In Gottfried, B. & Aghajan, H. (ed.), Behaviour
Montoring and Interpretation—Ambient Assisted Living.
Amsterdam:IOSPress.
Kemp, J.F. 2007. The Colregs and the Princess Alice.
TransNav—InternationalJournalonMarineNavigationand
SafetyofSea
Transportation,1(1):57–61
Kemp,J.F.2009.BehaviourPatternsinCrossingSituations.
TransNav—InternationalJournalonMarineNavigationand
SafetyofSeaTransportation,3(1):75–79
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.
168
Kolendo P., Smierzchalski R., Jaworski B. 2011.
Experimental Research on Evolutionary Path Planning
Algorithm with Fitness Function Scaling for Collision
Scenarios. TransNav—International Journal on Marine
NavigationandSafetyofSeaTransportation,5(4):489–495
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).Thebranch‐and‐boundmethod
andgeneticalgorithminavoidanceofships 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
ConferenceonAI2006.Amsterdam:IOSPress.
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.NewYork:ACM.
Pietrzykowski, Z. & Uriasz, J. 2010. Knowledge
representationinashipʹsnavigationaldecisionsupport
system. TransNav—International Journal on Marine
Navigation and Safety of Sea Transportation, 4(3):359–
364.Gdynia:Poland.
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:IEEEComputerSociety.
Smierzchalski, R. & Michalewicz, Z. (2000). Modeling of
shiptrajectoryincollisionsituationsbyanevolutionary
algorithm.InTrans.Evol.Comp,4(3):227–241.
Szłapczynski, R. 2010. Evolutionary Sets of Cooperating
Tra‐jectories in Multi‐Ship Encounter Situations—Use
Cases. TransNav—International Journal on Marine
Navigation and Safety of Sea Transportation, 4(2):191–
196,Gdynia:Poland
Wolter, D., Kreutzmann, A. & Dylla, F. (2011). Rule‐
Compliant Navigation With Qualitative Spatial
Reasoning, In Schlaefer, A., Blaurock, O. (ed.), Robotic
Sailing—Proceedingsofthe4thInternationalRoboticSailing
Conference,141–155,Berlin:Springer.
Wolter, D.
& Wallgrün, J. (2012). Qualitative Spatial
Reasoning for Applications: New Challenges and the
SparQToolbox.InHazarika,S.(ed.), Qualitative Spatio‐
TemporalRepresentationandReasoning—Trends andFuture
Directions,336–362.Hershey:IGIGlobal.
