타임아웃 오토매틱

오토마타 이론에서, 타이밍 오토마톤은 유한한 집합의 실제 가치 클럭으로 확장된 유한한 오토마톤이다.타이밍 설정 자동화를 실행하는 동안 클럭 값은 모두 동일한 속도로 증가한다.자동화의 전환을 따라 시계 값을 정수와 비교할 수 있다.이러한 비교는 전환을 활성화하거나 비활성화할 수 있는 가드를 형성하며, 그렇게 함으로써 자동화의 가능한 동작을 구속한다.게다가, 시계는 재설정될 수 있다.타이밍 설정 자동타(Timed automata)는 하이브리드 자동타 타입의 하위 클래스다.

타이밍 설정 자동자는 컴퓨터 시스템(예: 실시간 시스템 또는 네트워크)의 타이밍 동작을 모델링하고 분석하는 데 사용할 수 있다.지난 20년 동안 안전성과 탄성 성질을 모두 점검하는 방법이 개발되어 집중적으로 연구되었다.

타이밍 설정 자동타에 대한 상태 도달성 문제가 디커블이 가능한 것으로 확인되었으며,^[1] 이는 하이브리드 자동타에 대한 흥미로운 하위 등급이다.스톱워치, 실시간 작업, 비용 기능, 시간 제한 게임 등 확장이 광범위하게 연구돼 왔다.모델 체커 UPAAL, Kronos 및 스케줄링 분석기 TIMES를 포함하여, 타이밍 설정 자동 및 확장을 입력 및 분석하는 다양한 도구가 있다.이러한 도구들은 점점 더 성숙해 가고 있지만, 여전히 모두 학문적인 연구 도구들이다.

예

타이밍 설정 자동화가 무엇인지 공식적으로 정의하기 전에 몇 가지 예를 제시한다.

${\mathcal {L}}$ 번째 시간 단위 동안 $a$ $a$ 이(가) 있고 $두$ 연속 a $a$ 사이에 하나의 시간 단위가 있도록 단일 문자 $\{a\}$ $\{a\}}$ 에 $w$ 대한 시간 $단위$ w{\ $displaystystyle w}$ 의 ${\mathcal L}$ L ${\displaystystystyleane}$ 언어를 고려하십시오 $a$ 이 언어를 인식하는 시간 제한 자동화는 하나의 시계 $x$ $x$ 을 사용하며, 이 값은 결코 하나와 같을 수 없다 $x$ 이 시계는 $a$ 이(가) 방출되지 않은 $a$ 경우 실행이 시작된 이후부터 또는 마지막으로 $a$ 된 $a$ {\ $displaystyle a}$ 이(가) 다른 방식으로 방출된 후부터의 시간을 카운트한다. $a$ 는 ${\displaystyle$ a $}$ 이(가) 방출될 $a$ 때마다 이 시계가 0으로 재설정됨을 의미한다.

길이 1의 각 열린 간격에서 문자가 방출되도록 언어 a*를 수락하는 시간 제한 자동.

이진 문자 $\{a,b\}$ { $\{a,b\}$ , $\{a,b\}$ ${\displaystyle$ $\{$ $a,b\}$ 을(를) 통해 $w$ 시간 지정 단어 $w$ $w$ 의 ${\mathcal L}$ ${\mathcal {L}}$ ${\$ $\{$ $a,b\}$ 을(를) 고려하여 각 ${\$ $displaystystyle a$ $}$ 이 다음 $a$ 시간 $b$ 단위에 $}$ 뒤에 오도록 하십시오 $\{a,b\}$ .이 언어를 인식하는 시간 제한 자동화는 이 $b$ 에 b ${\displaystyle$ a $}$ 뒤에 b $b$ 이 $a$ (가) 없었는지 여부를 $b$ 회상한다.그렇지 않으면 주행을 받아들이고, 그렇지 않으면 거부한다.또한 $이러한$ $a$ 이(가) 있을 때 $a$ 처음 $a$ 이(가) 방출된 $a$ 이후 경과된 시간을 기억하는 $x$ 시계 $x$ $x$ 을(를) 가진다.이 경우 시계가 적어도 1과 같으면 $b$ $b$ 을(를) 내보낼 수 없어 $b$ 실행이 실패한다.

\{a,b\}

,

\{a,b\}

\{a,b\}

\{a,b\

에 걸쳐 시간 제한 단어를 받아들이는 시간 제한 자동 분석.

b

서

\{a,b\}

a

의 각 발생은 b

b

의 발생에 의해 1회 미만으로 이어진다

a

b

형식 정의

타임아웃 오토매틱

형식적으로 타이밍 설정 자동화는 튜플 ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ = ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ , L ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ , ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ , ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ , F , ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ ${\mathcal{A}=\langle \Sigma ,L,L_{0}}C,F,E\angle }$ 이다 ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ .

$\Sigma$ $\Sigma$ 은(는) ${\mathcal {A}}$ ${\$ { $A}$ 의 알파벳 또는 동작이라고 하는 유한 집합이다 $\Sigma$ ${\mathcal {A}}$
$L$ $L$ 은 $L$ (는) 유한 집합이다. $L$ $L$ 의 요소를 ${\mathcal {A}}$ ${\$ { $A}$ 의 위치 또는 상태라고 한다 ${\mathcal {A}}$
$L_{0}\subseteq L$ $L_{0}\subseteq L$ $L_{0}\subseteq L$ $L_{0}\subseteq L$ $L_{0}\subseteq L$ 은 $L_{0}\subseteq L$ (는) 시작 위치의 집합이다.
$C$ $C$ 은 $C$ (는) ${\mathcal {A}}$ {\ $displaystyle {\mathcal {A}$ 의 클럭이라고 하는 유한 집합이다 ${\mathcal {A}}$
$F\subseteq L$ $F\subseteq L$ $F\subseteq L$ $F\subseteq L$ 은 $F\subseteq L$ (는) 승인 위치의 집합이다.
$E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L$ is a set of edges, called transitions of ${\mathcal {A}}$ , where
- ${\mathcal {B}}(C)$ ) ${\mathcal {B}(C)$ 은 ${\mathcal {B}}(C)$ $C$ 는) $C$ $C$ 의 클럭을 포함하는 클럭 제약 조건 집합이며,
- ${\mathcal {P}}(C)$ ( ${\mathcal {P}}(C)$ ) ${\mathcal {P}(C)$ 은 ${\mathcal {P}}(C)$ (는) $C$ ${\displaystyle C$ 의 파워셋이다.

An edge $(\ell ,\sigma ,g,r,\ell ')$ from $E$ is a transition from locations $\ell$ to $\ell '$ with action $\sigma$ , guard $g$ and clock resets $r$ .

확장 상태

위치 $\ell$ $\ell$ 과 $\ell$ 시계 $\nu$ { $\nu$ 을(를) 가진 쌍을 확장된 상태 또는 상태라고 한다 $\nu$ .

상태라는 단어는 저자에 따라 $L$ $L$ 의 한 쌍 또는 한 요소를 의미할 수 있으므로 매우 모호하다는 점에 유의하십시오 $L$ 명확성을 위해 본 문서는 $L$ $L$ 요소의 위치 및 $L$ 쌍의 확장 위치라는 용어를 사용할 것이다.

여기에 시간 자동자와 유한 자동자 사이의 가장 큰 차이점 중 하나가 있다.유한자동화에서, 실행의 어느 시점에서, 상태는 읽히는 문자의 수와 실제로 "상태"라고 불리는 가능한 값의 한정된 숫자에 의해 전적으로 설명된다.즉, 읽을 단어의 상태와 접미사로 볼 때, 달리기의 남은 부분이 완전히 결정된다는 것을 의미한다.따라서, "마인렛 오토마타"라는 이름의 "마인렛"이라는 단어는단, 아래의 "실행" 섹션에서 설명하듯이, 시계를 다시 시작하기 위해 어떤 전환이 가능한지 결정하는 데 사용된다.따라서 자동화의 상태를 알기 위해서는 자신이 어느 위치에 있는지, 그리고 시계 가치평가를 둘 다 알아야 한다.

달리다

Given a timed word $w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,$ with $\sigma _{i}\in \Sigma$ , $(t_{i})_{i}$ an increasing sequence of non-negative number, and a timed-automaton ${$ $\displaystyle {\mathcal {A}}}$ as above, a run is a sequence of the form $(\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots$ satisfying the following constraint:

(초기화) $\ell _{0}\in L_{0}$ $\ell _{0}\in L_{0}$ $\ell _{0}\in L_{0}$ $\ell _{0}\in L_{0}$ $\ell _{0}\in L_{0}$ ${\$
(consecution), for all $i\geq 1$ , there exists an edge in $E$ of the form $\langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle$ such that:
- $t_{i}-t_{i-1}$ $t_{i}-t_{i-1}$ - $t_{i}-t_{i-1}$ $t_{i}-t_{i-1}$ - $t_{i}-t_{i-1}$ ${\$ 시간 $t_{i}-t_{i-1}$ 단위가 경과했다고 가정하며, 이때 가드는 만족한다.즉, $\nu _{i-1}+t_{i}-t_{i-1}$ $\nu _{i-1}+t_{i}-t_{i-1}$ - 1 $\nu _{i-1}+t_{i}-t_{i-1}$ + $\nu _{i-1}+t_{i}-t_{i-1}$ $\nu _{i-1}+t_{i}-t_{i-1}$ - $\nu _{i-1}+t_{i}-t_{i-1}$ $\nu _{i-1}+t_{i}-t_{i-1}$ - $\nu _{i-1}+t_{i}-t_{i-1}$ 1 ${\$ 1}은(는) ${\$
- 새로운 시계 평가 $\nu _{i}$ i ${\$ $displaystyle$ $\nu_{i}}$ 는 $\nu _{i-1}$ $t_{i}-t_{i-1}$ - $\nu _{i-1}$ 1 ${\$ $}$ 에 $t_{i}-t_{i-1}$ 해당하며, $\nu _{i-1}$ t - $t_{i}-t_{i-1}$ - $t_{i}-t_{i-1}$ - $t_{i}-t_{i-1}$ ${\$ 시간 단위가 경과되고 ${$ 의 클럭이 재설정되는 $r_{i}$ 경우에 해당한다 $\nu _{i}$ .형식적으로 $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ i $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ = ( $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ i $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ - 1 $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ + $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ - t $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ - t - $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ i - $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ ) $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ [ $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ i $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ → 0 $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ ] ${\displaystyle \nu _{i-1}=(\nu _{i-1}+t_{i-1}-t_{i-1}[r_{i}\오른쪽 화살표$ 0 $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ .

런을 받아들이는 개념은 유한한 단어의 경우 유한한 오토마타에서, 무한단어의 경우 부치 오토마타에서와 같이 정의된다.즉, $w$ $w$ 이 $w$ $n$ 가) $길이$ n $n$ 의 유한인 경우, 실행은 $\ell _{n}\in F$ F $\ell _{n}\in F$ _ ${n}\in$ F $}$ 인 경우 $\ell _{n}\in F$ $\ell _{i}\in F$ $\ell _{i}\in F$ ${\displaystyl$ $}$ 과 같은 위치 $i$ $i$ 가 무한히 존재하는 경우에만 수락하는 것이다. $e \ell _{i}\in$ F $\ell _{i}\in F$

결정론적 시간 자동 분석

유한 및 부치 자동화의 경우와 같이, 시간 자동화는 결정론적이거나 비결정론적일 수 있다.직관적으로 결정론적이라는 것은 각각의 경우에 같은 의미를 갖는다.시작 위치 집합이 단일 톤이며, $상태$ s $s$ 및 $문자$ a $a$ 을 $a$ 를) 고려할 때 $a$ 을(를) 읽음으로써 $s$ $s$ ${\displaystystyle s}$ 에서 도달할 수 있는 상태는 단 하나라는 것을 의미한다 $a$ 그러나, 시간 자동화의 경우 형식 정의는 slightimate이다.훨씬 더 복잡한공식적으로 다음과 같은 경우 시간 자동 분석은 결정론적이다.

$L_{0}$ $L_{0}$ ${\$ 은 $L_{0}$ (는) 싱글톤이다.
for each pair of transitions $(\ell ,\sigma ,g,r,\ell ')$ and $(\ell ,\sigma ,g',r',\ell '')$ , the set of clocks valuations satisfying $g$ is disjoint from the set of clocks valuations satisfying ${\displaystyle$ $g$

폐업특성

비결정론적 시간 자동화가 인식하는 언어의 종류는 다음과 같다.

실제로, 조합에 의해 폐쇄된, 두 개의 시간 제한 오토마타의 분리 연합은 그 오토마타에 의해 인식된 언어의 결합을 인식한다.
교차로에서 ^[2]폐쇄하다
보수가 ^[3]없는

문제와 그 복잡성

시간 자동화와 관련된 몇 가지 문제의 계산 복잡성이 현재 제시되어 있다.

시간대별 자동화의 공허함 문제는 지역 자동화를 구축하고 빈 언어를 수용하는지 여부를 확인함으로써 해결할 수 있다.이 문제는 PSPACE-완전이다.^[1]^{: 207}

비결정론적 타이밍 자동화의 보편성 문제는 불분명하며, 보다 정확하게는 π이다¹
₁.그러나, 자동화가 하나의 시계를 포함할 때, 그 속성은 결정 가능하지만, 원시적인 재귀는 아니다.^[3]이 문제는 모든 단어가 시간 자동 응답에 의해 받아들여지는지를 결정하는 데 있다.

참고 항목

교대 시간 지정 자동: 범용 전환이 포함된 시간 지정 자동화의 확장.

메모들

^ ^a ^b Rajev Alur, David L. Dill. 1994 타임 오토마타 이론.이론 컴퓨터 과학에서, 제126권, 183–235권, 페이지 194–1955.
^ 오토마타의 현대적 응용 프로그램, 118페이지
^ ^a ^b Lasota, SƗawomir; Walukiewicz, Igor (2008). "Alternating Timed Automata". ACM Transactions on Computational Logic. 9 (2): 1–26. arXiv:cs/0512031. doi:10.1145/1342991.1342994.

[AlurDill-1] Rajev Alur, David L. Dill. 1994 타임 오토마타 이론.이론 컴퓨터 과학에서, 제126권, 183–235권, 페이지 194–1955.

[2] 오토마타의 현대적 응용 프로그램, 118페이지

[Alternating_timed_automata-3] Lasota, SƗawomir; Walukiewicz, Igor (2008). "Alternating Timed Automata". ACM Transactions on Computational Logic. 9 (2): 1–26. arXiv:cs/0512031. doi:10.1145/1342991.1342994.

[1]

[2]

[3]

Search

타임아웃 오토매틱

네임스페이스

더

목차

예

형식 정의

타임아웃 오토매틱

확장 상태

달리다

결정론적 시간 자동 분석

폐업특성

문제와 그 복잡성

참고 항목

메모들