Logik for droner

Jeg er med på flere mailinglister inden for datalogi. Forleden kunne jeg se et jobopslag, som jeg her bringer et uddrag af:

The Department of Computer Science of University of Oxford seeks a
 postdoctoral researcher to work on a 3-year EPSRC project entitled
 `New Foundational Structures for Engineering Multi-UAV Protocols'.
This interdisciplinary project aims to verify autonomous 
Unmanned Aerial Vehicles (UAV's) that not only navigate, but also
communicate with each other. The project aims to span the full
verification lifecycle: from high-level logical specifications, to 
oracle-based test-set reasoning through a bounded model checker, 
to low-level code on our four Pelican UAVs.
The position requires a researcher with a proven track record of
high-quality research in logic and its applications - of particular
relevance are formalisms such as:
- Modal and Epistemic Logics
 - Dynamic Program Logics
 - Probabilistic and Fuzzy logics
Preference will be given to researchers with experience in 
modelling and reasoning about epistemic properties of protocols 
of communicative Multi-Agent Systems.

Det lyder meget tilforladeligt. Hvad handler forskningsprojektet om? Det handler om at verificere software til UAV’er, ubemandede autonome fartøjer. Dvs. ikke et fjernstyret køretøj som “Rullemarie”, men fartøjer, der i større omfang kan handle selv og endda kommunikere selv, så de kan bevæge sig i flok.

Ubemandede autonome fartøjer har civile anvendelser; de kan sendes ind i katastrofezoner som f.eks. områder berørt af jordskælv eller atomulykker.  I omtalen af forskningsbevillingen fra Oxford er det dette civile aspekt, der udelukkende fokuseres på – med Japan som det helt oplagte eksempel på begge slags katastrofezoner.

Men reelt er de mest udbredte anvendelser militære. Det bedst kendte eksempel på UAV’er er de militære droner, som jeg skrev om for nylig. Pelican-dronen, som nævnes i opslaget fra Oxford, har da også militær baggrund ifølge firmaet, der fremstiller dem.

I en artikel i Information i dag kan jeg læse, at 50 lande i dag har indkøbt droner til militære formål, heriblandt Danmark. For mange tror på droner som en af fremtidens fremtrædende våbentyper. Charlotte Aagaard citerer i artiklen seniorforsker Henrik Breitenbauch fra Center for Militære Studier ved Københavns Universitet for at sige:

»Om 10 år vil vi ikke se et eneste bemandet militærfly i luften,« siger han. »Piloter vil være en mærkelig reminiscens fra en svunden tid.«

Droner er meget billigere end kampfly, og ingen piloters liv er på spil. Det bliver med droner muligt at bombe og slå ihjel hjemme fra kontoret.

Det tilsyneladende ukomplicerede jobopslag om modal og epistemisk logik og anvendelser i modeltjek er i virkeligheden et indslag i den nyeste form for krigsførelse, nemlig udviklingen af erstatningen for kampfly (og kamphelikoptere). Interessen for software til UAV’er er ikke ny; jeg husker en datalogi-konference i Aalborg for 11 år siden, hvor en af de indbudte foredragsholdere var en daværende ansat på Aalborg Universitet, der med slet skjult stolthed viste os en film med khakifarvede modelhelikoptere, der kunne flyve i formation takket være software, hans forskningsgruppe havde udviklet. Jeg kom uvilkårligt til at tænke på en berygtet scene fra Dommedag nu; måske var jeg den eneste, der gjorde det.

Hvad skal vores rolle som forskere være i alt dette? Svaret er ikke enkelt. Jeg er meget skeptisk over for militæret og ideen om at løse konflikter med krig, men jeg ved at andre er helt uenige med mig heri. Det vigtige er, at man ikke foregøgler sig selv og andre, at det man laver er værdineutralt eller har entydigt positive konsekvenser. Jeg kommer til tænke på “Om matematik og krig”, en 20 år gammel artikel af Jens Høyrup, der var matematiker og ansat på RUC. Den giver en grundig gennemgang af hvordan forskning i matematik og datalogi (et langt afsnit handler om programmeringssprog) er blevet påvirket af og har påvirket militær teknologi og militær praksis. Høyrup skriver som noget af det sidste:

Enhver i dette miljø tager i praksis parti for den ene eller den anden udnyttelse af sit fag, ved at formidle og bearbejde problemer med rod i det ene eller det andet praksisfelt; ved at opdage eller ikke opdage sin påtænkte rolle i et større samspil; ved at lægge sine forskningsresultater frem offentligt eller kun i fortrolighed for den betalende institution; ved at sælge sin politiske og ideologiske loyalitet til gengæld for bekvemme forskningsmidler eller ved at undgå det; ved i sin undervisning (for matematikeren er jo også ofte universitetslærer) at lade segmenteringen blive til skyklapper, eller ved at kombinere den faglige seriøsitet med bredde og derved give næste generations fagfolk mulighed for at komme ud over bevidst- og samvittighedsløsheden; ved at påtage sig den ene eller anden offentlige rolle i kombination med sin faglige kunnen, eller dække sig ind under matematikkens erkendelsesmæssige neutralitet som gjaldt den matematikeren.

Og dette er i virkeligheden også min holdning. Vi er ikke neutrale som forskere, og vi bør derfor ikke lade som om vi er det. Også vi er en del af samfundet. Hvor ubekvemt det end kan være for os, har alt, hvad vi foretager os, konsekvenser, der godt kan risikere at være ubehagelige og kontroversielle. Nogle konsekvenser kan vi ikke ane, men andre ligger lige for. Forskerne i Oxford er måske selv lidt kede af de oplagte og udbredte militære anvendelser, som deres arbejde er en del af og lægger op til, men de burde stå ved dem. Og jeg ved med mig selv, at jeg ikke på den ene side ville kunne arbejde med dette emne og på den anden side med Amnesty International og andre kritisere de problemer med overholdelsen af international lov, som brugen af militære droner giver sig udslag i.