Energiautomater, energifunktioner og Kleene-algebra

Abstract

Forfatterne til denne artikel har, sammen med mange gode kolleger, i en del år arbejdet med såkaldte energiproblemer. Disse handler om, at man i en formel model ønsker at bestemme, om der findes en endelig eller uendelig eksekvering under hvilken en given energivariabel aldrig bliver negativ. Den formelle model kan være en vægtet tidsautomat, en endelig automat som er annoteret med energifunktioner eller lignende. Fælles for alle disse modeller er, at det har vist sig ualmindeligt svært at løse sådanne energiproblemer og at teknikker fra Kleene-algebra har været en stor hjælp. 

Formålet med denne artikel er at give et overblik over nylig forskning i energiproblemer (for første gang på dansk) samt at udvide anvendelsen af Kleene-algebra i et forsøg på at lukke et åbent problem fra artiklen som startede hele dette område.