Automated Controller Synthesis for non-Deterministic Piecewise-Affine Hybrid Systems

I fremtidig rumbaseret forskning stiger behovet for nøjagtige målinger i sådan en grad at
en enkelt satellit på visse missioner ikke længere vil være i stand til at bære instrumenter
af den nødvendige størrelse. En af de mest lovende ideer til at overkomme dette problem
er satellitformationer hvor nøjagtig positionsregulering kan bruges til at skabe meget store
virtuelle apparaturer eller meget følsomme interferometriske målinger.
Satellitformationskontrol skaber en hel ny række udfordringer inden for rumfartøjskontrol,
som kræver udvikling inden for aktuatorer, sensorer, kommunikation og kontrolalgoritmer.
En af disse udfordringer opstår på grund af den øgede kompleksitet som
duplikeringen af kontrolsystemerne til multiple satellitter medfører. Denne duplikation af
komponenter og undersystemer øger sandsynligheden for at en komponent fejler således
at formationskontrollen påvirkes, men duplikationen øger også redundansen i formationen.
Kombineret med at det er urealistisk dyrt at reparere en satellit i kredsløb, så er
motivationen for at designe fejltolerante regulatorer specifikt til satellitformationer stor.
Denne afhandling bruger en hybrid systems model af en satellitformation med mulighed
for aktuator fejl som et motiverende eksempel for udviklingen af en automatiseret
kontrolsyntesemetode til stykvist-affine hybride systemer (SAHS). Metoden åbner ikke
kun op for fremtidig forskning i fejltolerant kontrol af satellitformationer, men kan også
blive brugt til at syntetisere regulatorer til en læng række af systemer hvor eksterne begivenheder
kan påvirke systemets dynamik.
Syntesemetoden bygger på en abstraktion af det hybride system til et diskret spil, at
finde en vindende strategi til spillet således at en “Computation Tree Logic” specifikation
bliver overholdt, samt raffinering af den resulterende løsning til en tabel over stykvistaffine
regulatorer.
Metoden er blevet implementeret i PAHSCTRL Matlab værktøjskassen ved brug af
linere-matrix-uligheds “feasibility” beregninger til at finde den diskrete abstraktion, UppAal
Tiga til løsning af det diskrete spil og linear optimering for at raffinere regulatorer.
Den præsenterede metode har nogle begrænsninger. Den bygger på fuld tilstandsinformation
og kan derfor ikke håndtere sensorfejl, og den beregningsmæssige komplexitet
af metoden vokser eksponentielt med tilstandsrummets dimension. Den sidste af de to
begrænsninger er delvist afhjulpet af at beregninger udføres a priori og det faktum at
beregningstiden skalerer næsten lineært med antallet af tilgængelige beregningsenheder.
Slutteligt, må de fleste realistiske systemmodeller transformeres for at komme på
SAHS form, hvilket sædvanligvis involverer partitionering af tilstandsrummet i polytoper.
Erfaring har vist at den specifikke partitionering af tilstandsrummet let kan påvirke den
diskrete spilabstraktion. og yderlige forskning i partitionsmetoder er derfor nødvendig
for at den foreslåede metode bliver generelt anvendelig.