Signal (modellkontroll)

Inom modellkontroll är ett underområde av datavetenskap , en signal- eller tidsbestämd tillståndssekvens en förlängning av begreppet ord, på ett formellt språk , där bokstäver kontinuerligt sänds ut. Medan ett ord traditionellt definieras som en funktion från en uppsättning icke-negativa heltal till bokstäver, är en signal en funktion från en uppsättning reella tal till bokstäver. Detta gör det möjligt att använda formalism som liknar automatteorin för att hantera kontinuerlig signal.

Exempel

Överväg en hiss. Det som formellt kallas ett brev kan i själva verket vara en information som att "någon trycker på knappen på andra våningen", eller "dörrarna är för närvarande öppna på tredje våningen". I detta fall indikerar en signal vid varje tillfälle vilket är det aktuella tillståndet för hissen och dess knappar. Signalen kan sedan analyseras med en formell metod för att kontrollera om en fastighet så att "varje gång hissen anropas kommer den på mindre än tre minuter förutsatt att ingen hållit dörren i mer än femton sekunder" håller. Ett påstående som det här uttrycks vanligtvis i metrisk temporal logik , en förlängning av linjär temporal logik som tillåter att uttrycka tidsbegränsningar.

En signal kan skickas till en modell, till exempel en signalautomat , som kommer att avgöra, med tanke på de bokstäver eller åtgärder som redan har inträffat, vad som är nästa åtgärd som ska göras. I vårt exempel, till vilken våning hissen måste gå. Sedan kan ett program testa denna signal och kontrollera den ovan nämnda egenskapen. Det vill säga, den kommer att försöka generera en signal där dörren aldrig hålls öppen i mer än femton sekunder, och där en användare måste vänta mer än tre minuter efter att ha ringt hissen.

Definition

Givet ett alfabet A är en signal $\gamma$ en sekvens $(I_{0},a_{0}),(I_ {1},a_{1}),\dots ,$ , finit eller oändlig, så att $a_{i}\in A$ , varje $I_{i} \subseteq \mathbb {R} _{+}$ är parvis disjunkta intervall, $0\in I_{0}$ , och $I_{i}\cup I_{ i+1}$ är också ett intervall. Givet $t\in I_{i}$ för vissa $i$ , representerar $\gamma (t)$$a_{i}$ .

Egenskaper

Vissa författare begränsar vilken typ av signaler de anser. Vi listar här några standardegenskaper som en signal kanske uppfyller eller inte uppfyller.

Finit variation

Intuitivt sägs en signal vara ändligt variabel, eller ha den ändliga variabilitetsegenskapen, om bokstaven ändras ett ändligt antal gånger under varje avgränsat intervall. I vårt tidigare hissexempel skulle den här egenskapen innebära att en användare bara får trycka på en knapp ett ändligt antal gånger under en begränsad tid. Och på liknande sätt, under en begränsad tid, kan hissen bara öppna och stänga sin dörr ett begränsat antal gånger.

Formellt sägs en signal ha den finita variabilitetsegenskapen, om inte sekvensen är oändlig och $\bigcup _{i}I_{i}$ är avgränsad. Intuitivt anger egenskapen finita variabilitet att det inte finns ett oändligt antal förändringar under en finit tid. Att ha egenskapen finita variabilitet liknar begreppet att vara icke-Zeno för ett tidsbestämt ord .

Begränsad variabilitet

Begreppet begränsad variabilitet är en begränsning till begreppet ändlig variabilitet. En signal har den begränsade variabilitetsegenskapen om det finns en nedre gräns mellan början av två intervall med samma bokstav.

Innan vi ger en formell definition ger vi ett exempel på signal som är ändligt variabel men inte gränslöst variabel. Ta alfabetet $A=\{a,b\}$ . Ta intervallet $\gamma$ som skickar realerna av formen $n+{\frac {c}{n}}$ med $n\in \mathbb {N }$ och $c<n$ till $a$ och varannan real till $b$ . Under varje ändligt tidsintervall ändras bokstaven ett ändligt antal gånger. Således är denna signal ändligt variabel. Avståndet mellan två på varandra följande förekomster av bokstaven $a$ är dock godtyckligt litet. Den har alltså inte egenskapen begränsad variabilitet.

Låt en sekvens $(I_{0},a_{0}),(I_{1},a_{1}),\dots$ . Om $a_{i}\neq a_{i+1}$ för varje heltal $i$ , så sägs sekvensen ha den begränsade variabilitetsegenskapen om det finns en reell $r>0$ så att för varje $i<j$ med $a_{i}=a_{j}$ så att det inte finns någon ${ \displaystyle k}$ med $i<j<k$ och $a_{i}=a_{k}$ sedan skillnaden mellan den nedre gränsen för ${\ displaystyle I_{j}}$ och av $I_{i}$ är minst $r$ . Observera att varje sekvens $\gamma$ är ekvivalent med en sekvens $\gamma '$ där två på varandra följande bokstäver är distinkta. Sekvensen $\gamma$ sägs ha egenskapen bounded variabilitet om och endast om $\gamma '$ har den bounded variabilitetsegenskapen.

En signaluppsättning sägs ha egenskapen bounded variabilitet om den ovan nämnda nedre gränsen $r$ kan väljas att vara densamma för varje signal i uppsättningen.

Vi vet ger huvudanledning att överväga signaler med gränsade variabiliteter. Antag att vi behöver skapa ett system, till exempel en signalautomat , som måste återkalla allt som inträffade under de senaste tidsenheterna. Om vi ​​vet att signalen är gränslöst variabel kan vi beräkna en övre gräns för antalet åtgärder som inträffade under en tidsenhet. Därmed kan vi skapa ett sådant system och säkerställa att det bara kräver ett ändligt minne.

Till exempel, för ett godtyckligt predikat $e$ , har signalen som anger huruvida påståendet " $p$ gäller någon gång i nästa tidsenhet" den bounded variabilitetsegenskapen. När detta påstående blir sant förblir det sant för en heltidsenhet. Således är skillnaden mellan två händelser där detta påstående blir sant större än en tidsenhet.

Tvådelad signal

En signal sägs vara tvådelad om sekvensen av intervall börjar med ett singulärt intervall – dvs ett slutet intervall vars nedre och övre gräns är lika, därav en mängd som är en singelton. Och om sekvensen växlar mellan singulära intervall och öppna intervall.

Varje signal är ekvivalent med en tvådelad signal. Ja, varje intervall som är stängt till vänster är föreningen av ett singularisintervall och ett intervall öppet till vänster, i denna ordning. Och på samma sätt för intervaller stängda till höger.

En signalautomat som läser en tvådelad signal har en speciell form. Dess uppsättning platser kan delas upp i platser för singulära intervall och platser för öppna intervall. Varje övergång går från en singulär plats till en öppen och ömsesidigt.

Se även

• Tidsbestämt ord

• Kini, Dileep Raghunath; Krishna, Shankara Narayanan; Pandya, Paritosh K. (2011). "Om konstruktion av säkerhetssignalautomater för MITL[U,S] med hjälp av tidsprojektioner". Format : 227.