Signalautomat

Inom automatteori , ett område inom datavetenskap , är en signalautomat en finit automat utökad med en finit uppsättning klockor med verkligt värde. Under körning av en signalautomat ökar klockvärdena alla med samma hastighet. Längs automatens övergångar kan klockvärden jämföras med heltal. Dessa jämförelser bildar skydd som kan aktivera eller inaktivera övergångar och genom att göra det begränsar automatens möjliga beteenden. Vidare kan klockor återställas.

Exempel

Innan man formellt definierar vad en signalautomat är kommer ett exempel att ges. Låt oss betrakta språket för signaler, över ett binärt alfabet , som innehåller signalerna så att:

  • visas i singulära intervall. Det vill säga uppsättningen av tider är diskret, och
  • visas minst en gång under varje intervall med längd ett.

Detta språk kan accepteras av automaten på bilden i närheten.

En signalautomat som säkerställer att A håller diskret och minst en gång per tidsenhet

När det gäller finita automater, representerar inkommande pilar initiala platser och dubbel cirkel representerar accepterande platser. Men i motsats till finita automater förekommer bokstäver på platser och inte i övergång. Detta beror på att bokstäver sänds ut kontinuerligt och övergångar tas diskret. Symbolen representerar en klocka . Denna klocka gör det möjligt att mäta tiden sedan senaste gången då sändes ut. Således säkerställer sänds ut diskret. Och säkerställer att inte mer än en tidsenhet kan passera utan att inträffar.

Formell definition

Signalautomat

Formellt är en signalautomat en tuppel som består av följande komponenter:

  • är en ändlig mängd som kallas alfabetet eller åtgärderna för .
  • är en ändlig mängd . Elementen i kallas platserna eller tillstånden för .
  • är en ändlig mängd som kallas klockorna för .
  • är uppsättningen startplatser.
  • är uppsättningen av accepterande platser.
  • som associerar en bokstav till varje plats.
  • som associerar en klockrestriktioner till varje plats, och
  • är en uppsättning kanter som kallas övergångar av , där
    • är kraftmängden för .

En kant från är en övergång från platser till som återställer klockorna för .

Förlängt tillstånd

Ett par med en plats och en klockvärdering kallas antingen ett utökat tillstånd eller ett tillstånd .

Observera att ordet tillstånd alltså är tvetydigt, eftersom det, beroende på författaren, kan betyda antingen ett par eller ett element av . För tydlighetens skull kommer denna artikel att använda termen plats för element i och termen utökad plats för par.

Här ligger en av de största skillnaderna mellan signalautomater och finita automater . I en ändlig automat, vid någon punkt av exekveringen, beskrivs tillståndet helt av antalet lästa bokstäver och av ett ändligt antal möjliga värden, som egentligen kallas "tillstånd". Det betyder att, givet ett tillstånd och ett suffix av ordet som ska läsas, bestäms återstoden av körningen helt. Alltså ordet "ändlig" i namnet "ändlig automat". Men, som det förklaras i avsnittet "kör" nedan, för att återuppta används klockor för att bestämma vilka övergångar som kan tas. För att veta tillståndet för automaten måste du alltså både nu på vilken plats du befinner dig och klockvärderingen.

Springa

När det gäller finita automater är en körning i huvudsak en sekvens av platser, så att det finns en övergång mellan två platser. Två skillnader måste dock betonas. Bokstaven bestäms inte av övergången utan av platserna; detta beror på att bokstäverna sänds ut kontinuerligt medan övergångar tas diskret. Det går en tid när man befinner sig på en plats; klockbegränsningarna som anger en plats eller dess efterföljare kan begränsa tiden som spenderas på en enda plats.

En körning är en sekvens av formen vissa begränsningar. Innan dessa begränsningar anges, introduceras några notationer. Sekvenserna är diskreta men representerar kontinuerliga händelser. En kontinuerlig version av sekvenserna , , introduceras nu. Låt integral och sedan

  • låt vara lika med ,
  • låt vara med är den nedre gränsen för intervallet ,
  • låt .

De begränsningar som uppfylls av körning är, för varje integral och reell:

  • ,
  • ,
  • ,
  • .

Signalen som definieras av denna körning är funktionen definierad ovan. Det sägs att körningen definierad ovan är en körning för signalen .

Begreppet att acceptera körning definieras som i finita automater för finita ord och som i Büchi automata för oändliga ord. Det vill säga om är ändlig av längden , så accepterar körningen om . Om ordet är oändligt, så accepterar körningen om och endast om det finns ett oändligt antal positioner så att .

Accepterade signaler och språk

En signal sägs accepteras av en signalautomat om det finns en körning av accepterar det. Uppsättningen signaler som accepteras av kallas språket som accepteras av och betecknas med .

Deterministisk signalautomat

Som i fallet med finita och Büchi-automater kan en signalautomat vara deterministisk eller icke-deterministisk. Intuitivt, att vara deterministisk med samma betydelse i vart och ett av dessa fall. Det betyder att uppsättningen startplatser är en singelton, och att, givet ett utökat tillstånd och en bokstav , det bara finns ett möjligt utökat tillstånd som kan nås från genom att läsa . Närmare bestämt, antingen är det möjligt att stanna på platsen längre, eller så finns det högst en möjlig efterträdarplats.

Formellt kan detta definieras enligt följande:

  • är en singelton
  • för varje plats , för varje övergång de två följande zoner är osammanhängande:
    • zonen som definieras av klockrestriktionen ,
    • zonen som definieras av klockrestriktionen där begränsningarna på klockorna för tas bort,
  • för varje plats övergångar och , de två följande zonerna är disjunkta:
    • zonen som definieras av klockrestriktionen där begränsningarna på klockorna för tas bort,
    • zonen som definieras av klockrestriktionen där begränsningarna på klockorna för tas bort,

Förenklad signalautomat

Beroende på författarna kan den exakta definitionen av signalautomater vara något annorlunda. Två sådana definitioner ges nu.

Halvöppna intervaller

För att förenkla definitionen av en körning kräver vissa författare att varje intervall i en körning är högerstängd och vänsteröppen. Detta begränsar automater att endast acceptera signaler vars underliggande partition uppfyller samma egenskap. Det säkerställer dock att vid varje tillfälle , för som representerar någon av funktionerna , eller infört ovan.

Tvådelad signalautomat

En tvådelad signalautomat är en signalautomat där körningen växlar mellan öppna intervall och singulära intervall (dvs intervall som är singletons). Det säkerställer att grafen som ligger bakom automaten är en tvådelad graf , och således att uppsättningen platser kan delas upp i , uppsättningen öppna platser och enstaka platser. Eftersom det första intervallet innehåller 0, kan det inte vara en öppen plats, det följer att . För att säkerställa att varje singular plats verkligen är singular, för varje plats , måste det finnas en klocka som återställs när och så att klockrestriktionen för innehåller .

Vilken signalautomat som helst kan omvandlas till en likvärdig tvådelad signalautomat. Det räcker att ersätta varje plats med ett par platser och introducera en ny klocka , så att för varje , .

I närheten visas en tvådelad automat som motsvarar signalautomaten från exempeldelen. Rektangeltillstånd representerar singulära platser.

En tvådelad signalautomat som säkerställer att A håller diskret och åtminstone en gång per tidsenhet

Synkronisering av automater

Begreppet produkt av ändlig automat utvidgas till signalautomat. En sådan produkt kallas dock en synkronisering av automat för att betona det faktum att tiden ska passera på liknande sätt i båda automaterna. Den största skillnaden mellan synkronisering och produkt är att när två ändliga automater läser samma ord tar de övergång samtidigt. Detta är inte fallet längre för signalautomater, eftersom de kan ta övergång vid godtycklig tid. Sålunda kan övergångsrelationen för en signalautomat tillåta att övergång tas i en eller två automater.

Låt och två signalautomater, deras synkronisering signalautomaten där innehåller följande övergångar:

  • för , och på liknande sätt för ,
  • för och .

Skillnad med tidsstyrda automater

Tidsinställda automater är en annan förlängning av finita automater, som lägger till en föreställning om tid till ord. Vi anger nu några av de viktigaste skillnaderna mellan tidsstyrda automater och signalautomater.

I tidsstyrda automater sänds bokstäver ut på övergångarna och inte på platserna. Såsom förklarats ovan när man jämför signalautomater med finita automater, sänds bokstäver vid övergångar när orden sänds ut diskret, som för ord och tidsbestämda ord medan de sänds ut på platser där bokstäver sänds ut kontinuerligt, som för signaler.

I tidsstyrda automater kontrolleras väktare endast vid övergångar. Detta förenklar definitionen av deterministisk automat, eftersom det betyder att begränsningen måste uppfyllas innan klockorna startas om.

Se även

Anteckningar

  1. ^ Brihaye, Thomas; Geeraerts, Gilles; Ho, Hsi-Ming; Monmege, Benjamin (2017). "Timed-Automata-Based Verification of MITL over Signals". 24:e internationella symposiet om temporär representation och resonemang (TIME 2017) . 90 : 7:1–7:19. doi : 10.4230/LIPIcs.TIME.2017.7 .