Roller, normer og deliberasjon for datamaskiner

Dataprogrammer blir stadig mer kompliserte. Hundretusenvis av linjer med komplisert kode settes sammen for å utføre ofte svært kompliserte beregninger. Samtidig er dataprogrammer blitt veldig viktige for samfunnet. Formell programverifikasjon er et forskningsfelt som utvikler metoder for å bekrefte at dataprogrammer fungerer som vi forventer før vi faktisk slipper programmene ut i virkeligheten. I noen tilfeller er det urimelig dyrt, eller til og med umulig, å teste alle aspekter på forhånd. Lansering av nye CPU-modeller og autonome fartøy på fjerne planeter, er åpenbare eksempler på det.

En fremgangsmåte for å verifisere komplekse systemer er å resonnere om systemene ved hjelp av formell logikk. Noen husker nok noen begreper fra logikk: tautologier og selvmotsigelser, "hvis, og bare hvis", osv. Moderne modallogikk kan også brukes til å resonnere om usikkerheter, tid og interaksjon. I avhandlingen tar Pedersen særlig for seg en familie av logikker for å resonnere om multiagentsystemer. Formelt har multiagentsystemer mange fellestrekk med spillteori som man kanskje kjenner fra økonomi. Slike logikker lar oss resonnere om hvordan systemer oppfører seg basert på hvordan systemets selvstendige komponenter oppfører seg.

En styrke ved disse logikkene er at de er intuitive for mennesker, og det er alltid mennesker som til syvende og sist utfører verifikasjonen. De uttrykker agenters "evner" og "intensjoner", altså på et høyere abstraksjonsnivå enn bare konkrete instruksjoner til de forskjellige komponentene.

I avhandlingen benytter Pedersen metaforen "rolle" for å resonnere om agentenes egenskaper og viser hvordan dette kan utgjøre en forskjell i de beregningsmessige utfordringene man støter på når man verifiserer store systemer. Rollemetaforen vises å være en svært effektiv forenkling. Videre viser Pedersen i avhandlingen sin at forenklingen kan oppheves ved i etterkant å introdusere (metaforiske) normer uten at den beregningsmessige kostnaden øker betydelig.

Personalia:

Truls Pedersen er født i 1981 og har vokst opp i Bergen. Han tok en bachelorgrad og mastergrad i informatikk ved Universitetet i Bergen. I 2009 avsluttet han mastergraden og begynte på doktorgrad i informasjonsvitenskap ved Det samfunnsvitenskapelige fakultet med veiledning fra professor Thomas Ågotnes.