Nåbarhetsproblem
Nåbarhet är ett grundläggande problem som förekommer i flera olika sammanhang: samtidiga system i ändliga och oändliga tillstånd , beräkningsmodeller som cellulära automater och petrinät , programanalys , diskreta och kontinuerliga system , tidskritiska system, hybridsystem , omskrivningssystem , probabilistiska och parametriska system och öppna system modellerade som spel .
Generellt kan nåbarhetsproblemet formuleras på följande sätt: Givet ett beräkningssystem (potentiellt oändligt tillstånd) med en uppsättning tillåtna regler eller transformationer, besluta om ett visst tillstånd i ett system är nåbart från ett givet initialtillstånd i systemet.
Varianter av nåbarhetsproblemet kan härröra från ytterligare begränsningar på initiala eller slutliga tillstånd, specifika krav på nåbarhetsvägar såväl som för iterativ nåbarhet eller förändring av frågorna till analys av vinnande strategier i oändliga spel eller oundviklighet av viss dynamik.
Typiskt, för en fast systembeskrivning som ges i någon form (reduktionsregler, ekvationssystem , logiska formler, etc.) består ett nåbarhetsproblem av att kontrollera om en given uppsättning måltillstånd kan nås med utgångspunkt från en fast uppsättning initialtillstånd. Uppsättningen av måltillstånd kan representeras explicit eller via någon implicit representation (t.ex. ett system av ekvationer, en uppsättning minimala element med avseende på någon ordning på tillstånden). Sofistikerade kvantitativa och kvalitativa egenskaper kan ofta reduceras till grundläggande nåbarhetsfrågor. Beslutbarhet och komplexitetsgränser, algoritmiska lösningar och effektiv heuristik är alla viktiga aspekter att beakta i detta sammanhang. Algoritmiska lösningar är ofta baserade på olika kombinationer av utforskningsstrategier, symboliska manipulationer av uppsättningar av tillstånd, nedbrytningsegenskaper eller reduktion till linjära programmeringsproblem , och de drar ofta nytta av approximationer, abstraktioner, accelerationer och extrapolationsheuristiker. Ad hoc-lösningar såväl som lösningar baserade på generella begränsningslösare och deduktionsmotorer kombineras ofta för att balansera effektivitet och flexibilitet.
Varianter av nåbarhetsproblem
Finit explicit graf
Nåbarhetsproblemet i en orienterad graf som beskrivs explicit är NL-komplett. Reingold, i en artikel från 2008, bevisade att nåbarhetsproblemet för en icke-orienterad graf finns i LOGSPACE.
Vid modellkontroll motsvarar nåbarhet en egenskap av livlighet.
Finit implicit graf
I planering , närmare bestämt i klassisk planering, är man intresserad av att veta om man kan uppnå ett tillstånd från ett initialt tillstånd från en handlingsbeskrivning. Beskrivningen av åtgärder definierar en graf över implicita tillstånd, som är av exponentiell storlek i beskrivningens storlek.
Vid symbolisk modellkontroll beskrivs modellen (den underliggande grafen) med hjälp av en symbolisk representation såsom binära beslutsdiagram .
Petri nät
Nåbarhetsproblemet i ett Petri-nät är avgörbart. Sedan 1976 är det känt att detta problem är EXPSPACE-hårt. [ fullständig hänvisning behövs ] Det finns resultat på hur mycket man ska implementera detta problem i praktiken. Under 2018 visade sig problemet vara icke-elementärt.
Öppna problem
Internationell konferens om nåbarhetsproblem (RP)
Serien International Conference on Reachability Problems, tidigare känd som Workshop on Reachability Problems , är en årlig akademisk konferens som samlar forskare från olika discipliner och bakgrunder som är intresserade av nåbarhetsproblem som förekommer i algebraiska strukturer, beräkningsmodeller, hybridsystem, oändliga spel, logik och verifiering. Workshopen försöker fylla gapet mellan resultat som uppnåtts inom olika områden men som delar gemensamma matematiska strukturer eller begreppsmässiga svårigheter.