Timed automaton

<h2 id="example">Example</h2>
<p>Before formally defining what a timed automaton is, some examples are given.
</p><p>Consider the language 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  
 of <a href="/facts/Timed_word/HkB4W242">timed words</a> 
  
    
      
        w
      
    
    {\displaystyle w}
  
 over the unary alphabet 
  
    
      
        {
        a
        }
      
    
    {\displaystyle \{a\}}
  
 such that there is an 
  
    
      
        a
      
    
    {\displaystyle a}
  
 during the first time unit, and there is less than one time unit between two successive 
  
    
      
        a
      
    
    {\displaystyle a}
  
. A timed automaton recognizing this language, pictured nearby, uses a single <a href="/facts/Clock_(model_checking)/3q9X8trL">clock</a> 
  
    
      
        x
      
    
    {\displaystyle x}
  
, which should never be equal to one. This clock counts the time since the start of the run if no 
  
    
      
        a
      
    
    {\displaystyle a}
  
 were emitted, or from the last 
  
    
      
        a
      
    
    {\displaystyle a}
  
 emitted otherwise. This means that each time an 
  
    
      
        a
      
    
    {\displaystyle a}
  
 is emitted, this clock is reset to zero.
</p>

<p>Consider the language 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  
 of <a href="/facts/Timed_word/HkB4W242">timed words</a> 
  
    
      
        w
      
    
    {\displaystyle w}
  
 over the binary alphabet 
  
    
      
        {
        a
        ,
        b
        }
      
    
    {\displaystyle \{a,b\}}
  
 such that each 
  
    
      
        a
      
    
    {\displaystyle a}
  
 is followed by a 
  
    
      
        b
      
    
    {\displaystyle b}
  
 in the next time unit.  The timed automaton recognizing this language, pictured nearby, recalls whether or not there was an 
  
    
      
        a
      
    
    {\displaystyle a}
  
 that was not yet followed by a 
  
    
      
        b
      
    
    {\displaystyle b}
  
. If it is not the case, it accepts the run, otherwise it rejects it. Furthermore, when there is such a 
  
    
      
        a
      
    
    {\displaystyle a}
  
, it has a clock 
  
    
      
        x
      
    
    {\displaystyle x}
  
 that records the time elapsed since the first such 
  
    
      
        a
      
    
    {\displaystyle a}
  
 was emitted. In this case, a 
  
    
      
        b
      
    
    {\displaystyle b}
  
 cannot be emitted if the clock is at least equal to one, and thus the run fails.
</p>

<h2 id="formal-definition">Formal definition</h2>
<h3>Timed automaton</h3>
<p>Formally, a timed automaton is a tuple 
  
    
      
        
          
            A
          
        
        =
        ⟨
        Σ
        ,
        L
        ,
        
          L
          
            0
          
        
        ,
        C
        ,
        F
        ,
        E
        ⟩
      
    
    {\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }
  
 that consists of the following components:
</p>
<ul><li>
  
    
      
        Σ
      
    
    {\displaystyle \Sigma }
  
 is a finite set called the alphabet or actions of 
  
    
      
        
          
            A
          
        
      
    
    {\displaystyle {\mathcal {A}}}
  
.</li>
<li>
  
    
      
        L
      
    
    {\displaystyle L}
  
 is a <a href="/facts/Finite_set/za1newlP">finite set</a>. The elements of 
  
    
      
        L
      
    
    {\displaystyle L}
  
 are called the locations or states of 
  
    
      
        
          
            A
          
        
      
    
    {\displaystyle {\mathcal {A}}}
  
.</li>
<li>
  
    
      
        
          L
          
            0
          
        
        ⊆
        L
      
    
    {\displaystyle L_{0}\subseteq L}
  
  is the set of start locations.</li>
<li>
  
    
      
        C
      
    
    {\displaystyle C}
  
 is a finite set called the <i><a href="/facts/Clock_(model_checking)/3q9X8trL">clocks</a></i> of 
  
    
      
        
          
            A
          
        
      
    
    {\displaystyle {\mathcal {A}}}
  
.</li>
<li>
  
    
      
        F
        ⊆
        L
      
    
    {\displaystyle F\subseteq L}
  
 is the set of accepting locations.</li>
<li>
  
    
      
        E
        ⊆
        L
        ×
        Σ
        ×
        
          
            B
          
        
        (
        C
        )
        ×
        
          
            P
          
        
        (
        C
        )
        ×
        L
      
    
    {\displaystyle E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L}
  
 is a set of edges, called transitions of 
  
    
      
        
          
            A
          
        
      
    
    {\displaystyle {\mathcal {A}}}
  
, where
<ul><li>
  
    
      
        
          
            B
          
        
        (
        C
        )
      
    
    {\displaystyle {\mathcal {B}}(C)}
  
 is the set of <a href="/facts/Clock_(model_checking)/3q9X8trL">clock constraints</a> involving clocks from 
  
    
      
        C
      
    
    {\displaystyle C}
  
, and</li>
<li>
  
    
      
        
          
            P
          
        
        (
        C
        )
      
    
    {\displaystyle {\mathcal {P}}(C)}
  
 is the <a href="/facts/Powerset/61VHAgXq">powerset</a> of 
  
    
      
        C
      
    
    {\displaystyle C}
  
.</li></ul></li></ul>
<p>An edge 
  
    
      
        (
        ℓ
        ,
        σ
        ,
        g
        ,
        r
        ,
        
          ℓ
          ′
        
        )
      
    
    {\displaystyle (\ell ,\sigma ,g,r,\ell ')}
  
 from 
  
    
      
        E
      
    
    {\displaystyle E}
  
 is a transition from locations 
  
    
      
        ℓ
      
    
    {\displaystyle \ell }
  
 to 
  
    
      
        
          ℓ
          ′
        
      
    
    {\displaystyle \ell '}
  
 with action 
  
    
      
        σ
      
    
    {\displaystyle \sigma }
  
, guard 
  
    
      
        g
      
    
    {\displaystyle g}
  
 and clock resets 
  
    
      
        r
      
    
    {\displaystyle r}
  
.
</p>
<h3>Extended state</h3>
<p>A pair with a location 
  
    
      
        ℓ
      
    
    {\displaystyle \ell }
  
 and a <a href="/facts/Clock_(model_checking)/3q9X8trL">clock valuation</a> 
  
    
      
        ν
      
    
    {\displaystyle \nu }
  
 is called either an <i>extended state</i> or a <i>state</i>.
</p><p>Note that the word state is thus ambiguous, since, depending on the author, it may mean either a pair or an element of 
  
    
      
        L
      
    
    {\displaystyle L}
  
.  For the sake of the clarity, this article will use the term location for element of 
  
    
      
        L
      
    
    {\displaystyle L}
  
 and the term extended location for pairs.
</p><p>Here lies one of the biggest difference between timed automata and <a href="/facts/Finite_automata/GMusWd0a">finite automata</a>. In a finite automaton, at some point of the execution, the state is entirely described by the number of letter read and by a finite number of possible values, which are actually called "states". That means that, given a state and a suffix of the word to read, the remaining of the run is totally determined. Thus, the word "finite" in the name "finite automata". However, as it is explained in the section "run" below, clocks are used to determine which transitions can be taken. So, in order to know the state of the automaton, it must both be known the location and the clock valuation.
</p>
<h3>Run</h3>
<p>Given a <a href="/facts/Timed_word/HkB4W242">timed word</a> 
  
    
      
        w
        =
        (
        
          σ
          
            1
          
        
        ,
        
          t
          
            1
          
        
        )
        ,
        (
        
          σ
          
            2
          
        
        ,
        
          t
          
            2
          
        
        )
        ,
        …
        ,
      
    
    {\displaystyle w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,}
  
 with 
  
    
      
        
          σ
          
            i
          
        
        ∈
        Σ
      
    
    {\displaystyle \sigma _{i}\in \Sigma }
  
, 
  
    
      
        (
        
          t
          
            i
          
        
        
          )
          
            i
          
        
      
    
    {\displaystyle (t_{i})_{i}}
  
 an increasing sequence of non-negative number, and a timed automaton 
  
    
      
        
          
            A
          
        
      
    
    {\displaystyle {\mathcal {A}}}
  
 as above, a <i>run</i> is a sequence of the form 
  
    
      
        (
        
          ℓ
          
            0
          
        
        ,
        
          ν
          
            0
          
        
        )
        
          
            →
            
              
                
                  t
                  
                    1
                  
                
              
            
            
              
                σ
                
                  1
                
              
            
          
        
        (
        
          ℓ
          
            1
          
        
        ,
        
          ν
          
            1
          
        
        )
        …
      
    
    {\displaystyle (\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }
  
 satisfying the following constraint:
</p>
<ul><li>(initialization) 
  
    
      
        
          ℓ
          
            0
          
        
        ∈
        
          L
          
            0
          
        
      
    
    {\displaystyle \ell _{0}\in L_{0}}
  
</li>
<li>(consecution), for all 
  
    
      
        i
        ≥
        1
      
    
    {\displaystyle i\geq 1}
  
, there exists an edge in 
  
    
      
        E
      
    
    {\displaystyle E}
  
 of the form 
  
    
      
        ⟨
        
          ℓ
          
            i
            −
            1
          
        
        ,
        
          σ
          
            i
          
        
        ,
        
          g
          
            i
          
        
        ,
        
          r
          
            i
          
        
        ,
        
          ℓ
          
            i
          
        
        ⟩
      
    
    {\displaystyle \langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle }
  
 such that:
<ul><li>we assume that 
  
    
      
        
          t
          
            i
          
        
        −
        
          t
          
            i
            −
            1
          
        
      
    
    {\displaystyle t_{i}-t_{i-1}}
  
 time units passed, and at this time, the guard is satisfied. I.e. 
  
    
      
        
          ν
          
            i
            −
            1
          
        
        +
        
          t
          
            i
          
        
        −
        
          t
          
            i
            −
            1
          
        
      
    
    {\displaystyle \nu _{i-1}+t_{i}-t_{i-1}}
  
 satisfies 
  
    
      
        
          g
          
            i
          
        
      
    
    {\displaystyle g_{i}}
  
,</li>
<li>the new clock valuation 
  
    
      
        
          ν
          
            i
          
        
      
    
    {\displaystyle \nu _{i}}
  
 corresponds to 
  
    
      
        
          ν
          
            i
            −
            1
          
        
      
    
    {\displaystyle \nu _{i-1}}
  
, in which 
  
    
      
        
          t
          
            i
          
        
        −
        
          t
          
            i
            −
            1
          
        
      
    
    {\displaystyle t_{i}-t_{i-1}}
  
 time units passed and in which the clocks of 
  
    
      
        
          r
          
            i
          
        
      
    
    {\displaystyle r_{i}}
  
 where reset. Formally, 
  
    
      
        
          ν
          
            i
          
        
        =
        (
        
          ν
          
            i
            −
            1
          
        
        +
        
          t
          
            i
          
        
        −
        
          t
          
            i
            −
            1
          
        
        )
        [
        
          r
          
            i
          
        
        →
        0
        ]
      
    
    {\displaystyle \nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]}
  
.</li></ul></li></ul>
<p>The notion of accepting run is defined as in <a href="/facts/Finite_automata/GMusWd0a">finite automata</a> for finite words and as in <a href="/facts/B%25C3%25BCchi_automata/5qKx0f5Q">Büchi automata</a> for infinite words. That is, if 
  
    
      
        w
      
    
    {\displaystyle w}
  
 is finite of length 
  
    
      
        n
      
    
    {\displaystyle n}
  
, then the run is accepting if 
  
    
      
        
          ℓ
          
            n
          
        
        ∈
        F
      
    
    {\displaystyle \ell _{n}\in F}
  
. If the word is infinite, then the run is accepting if and only if there exists an infinite number of position 
  
    
      
        i
      
    
    {\displaystyle i}
  
 such that 
  
    
      
        
          ℓ
          
            i
          
        
        ∈
        F
      
    
    {\displaystyle \ell _{i}\in F}
  
.
</p>
<h3>Deterministic timed automaton</h3>
<p>As in the case of finite and Büchi automaton, a timed automaton may be deterministic or non-deterministic. Intuitively, being deterministic has the same meaning in each of those case. It means that the set of start locations is a singleton, and that, given a state 
  
    
      
        s
      
    
    {\displaystyle s}
  
, and a letter 
  
    
      
        a
      
    
    {\displaystyle a}
  
, there is only one possible state which can be reached from 
  
    
      
        s
      
    
    {\displaystyle s}
  
 by reading 
  
    
      
        a
      
    
    {\displaystyle a}
  
. However, in the case of timed automaton the formal definition is slightly more complex. Formally, a timed automaton is deterministic if:
</p>
<ul><li>
  
    
      
        
          L
          
            0
          
        
      
    
    {\displaystyle L_{0}}
  
 is a singleton</li>
<li>for each pair of transitions 
  
    
      
        (
        ℓ
        ,
        σ
        ,
        g
        ,
        r
        ,
        
          ℓ
          ′
        
        )
      
    
    {\displaystyle (\ell ,\sigma ,g,r,\ell ')}
  
 and 
  
    
      
        (
        ℓ
        ,
        σ
        ,
        
          g
          ′
        
        ,
        
          r
          ′
        
        ,
        
          ℓ
          ″
        
        )
      
    
    {\displaystyle (\ell ,\sigma ,g',r',\ell '')}
  
, the set of clocks valuations satisfying 
  
    
      
        g
      
    
    {\displaystyle g}
  
 is disjoint from the set of clocks valuations satisfying 
  
    
      
        
          g
          ′
        
      
    
    {\displaystyle g'}
  
.</li></ul>
<h2 id="closure-property">Closure property</h2>
<p>The class of languages recognized by non-deterministic timed automata is:
</p>
<ul><li>closed under union, indeed, the disjoint union of two timed automata recognize the union of the language recognized by those automata.</li>
<li>closed under intersection.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a></li>
<li>not closed under complement.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a></li></ul>
<h2 id="problems-and-their-complexity">Problems and their complexity</h2>
<p>The <a href="/facts/Computational_complexity/Qenh22Ja">computational complexity</a> of some problems related to timed automata are now given.
</p><p>The emptiness problem for timed automata can be solved by constructing a <a href="/facts/Region_(model_checking)/F11tNw8G">region automaton</a> and checking whether it accepts the empty language. This problem is <a href="/facts/PSPACE-complete/gkV3vHfX">PSPACE-complete</a>.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a>: 207 
</p><p>The universality problem of non-deterministic timed automaton is undecidable, and more precisely <a href="/facts/Coanalytic_set/5XkDAeQk">Π11</a>. However, when the automaton contains a single clock, the property is decidable; however, it is not <a href="/facts/Primitive_recursive/4z97gRnl">primitive recursive</a>.<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> This problem consists of deciding whether every word is accepted by a timed automaton.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Alternating_timed_automaton/AawQkf0B">Alternating timed automaton</a>: an extension of timed automaton with universal transitions.</li></ul>
<h2 id="notes">Notes</h2>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Ingólfsdóttir, Anna; Srba, Jiri; Larsen, Kim Guldstrand; Aceto, Luca, eds. (2007), "Timed automata", Reactive Systems: Modelling, Specification and Verification, Cambridge: Cambridge University Press, pp. 175–192, ISBN 978-0-521-87546-2, retrieved 2025-05-10 <a href="978-0-521-87546-2" target="_blank">978-0-521-87546-2</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Rajeev Alur, David L. Dill. 1994 A Theory of Timed Automata. In Theoretical Computer Science, vol. 126, 183–235, pp. 194–1955 <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.1093" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.1093</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Modern Applications Of Automata, page 118 <a href="https://books.google.com/books?id=a-TFCgAAQBAJ&dq=timed+automaton+closure+intersection&pg=PA117" target="_blank">https://books.google.com/books?id=a-TFCgAAQBAJ&dq=timed+automaton+closure+intersection&pg=PA117</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>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. S2CID 12319. <a href="/wiki/ACM_Transactions_on_Computational_Logic" target="_blank">/wiki/ACM_Transactions_on_Computational_Logic</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
<li id="fn:5"><p>Rajeev Alur, David L. Dill. 1994 A Theory of Timed Automata. In Theoretical Computer Science, vol. 126, 183–235, pp. 194–1955 <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.1093" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.1093</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li>
<li id="fn:6"><p>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. S2CID 12319. <a href="/wiki/ACM_Transactions_on_Computational_Logic" target="_blank">/wiki/ACM_Transactions_on_Computational_Logic</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li>
</ol>

Timed automaton open-in-new

Timed automaton