Signal automaton

Formally, a signal automaton is a tuple ${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,\alpha ,\beta ,E\rangle }$ that consists of the following components:

• ${\displaystyle \Sigma }$ is a finite set called the alphabet or actions of ${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle L}$ is a finite set. The elements of ${\displaystyle L}$ are called the locations or states of ${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle C}$ is a finite set called the clocks of ${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle L_{0}\subseteq L}$ is the set of start locations.
• ${\displaystyle F\subseteq L}$ is the set of accepting locations.
• ${\displaystyle \alpha :L\to \Sigma }$ which associates a letter to each location.
• ${\displaystyle \beta :L\to {\mathcal {B}}(C)}$ which associate a clock constraints to each location, and
• ${\displaystyle E\subseteq L\times {\mathcal {P}}(C)\times L}$ is a set of edges, called transitions of ${\displaystyle {\mathcal {A}}}$, where
  • ${\displaystyle {\mathcal {P}}(C)}$ is the powerset of ${\displaystyle C}$.

An edge ${\displaystyle (\ell ,r,\ell ')}$ from ${\displaystyle E}$ is a transition from locations ${\displaystyle \ell }$ to ${\displaystyle \ell '}$ which reset the clocks of ${\displaystyle r}$.

A pair with a location ${\displaystyle \ell }$ and a clock valuation ${\displaystyle \nu }$ is called either an extended state or a state.

Note that the word state is thus ambiguous, since, depending on the author, it may means either a pair or an element of ${\displaystyle L}$. For the sake of the clarity, this article will use the term location for element of ${\displaystyle L}$ and the term extended location for pairs.

Here lies one of the biggest difference between signal-automata and finite automata. 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, in order to resume clocks are used to determine which transitions can be taken. Thus, in order to know the state of the automaton, you must both now in which location you are, and the clock valuation.

As for finite automata, a run is essentially a sequence of locations, such that there exists a transition between two locations. However, two differences must be emphasized. The letter is not determined by the transition but by the locations; this is due to the fact that the letters are emitted continuously while transitions are taken discretely. Some time elapses while in a location; the clock constraints labelling a location or its successor may constraint the time spent in a single location.

A run is a sequence of the form ${\displaystyle {\xrightarrow[{\nu _{0}}]{C}}(\ell _{0},I_{0}){\xrightarrow[{\nu _{1}}]{r_{1}}}(\ell _{1},I_{1})\dots }$ satisfying some constraints. Before stating those constraints, some notations are introduced. The sequences are discrete but represents continuous events. A continuous version of the sequences ${\displaystyle (\sigma _{i})}$, ${\displaystyle (\nu _{i})}$, ${\displaystyle (\ell _{i})}$ are now introduced. Let ${\displaystyle i\geq 0}$ integral and ${\displaystyle t\in I_{i}}$, then

• let ${\displaystyle \sigma '_{t}}$ be equal to ${\displaystyle \sigma _{i}}$,
• let ${\displaystyle \nu '_{t}}$ be ${\displaystyle \nu _{i}+t-\lceil I_{i}\rceil }$ with ${\displaystyle \lceil I_{i}\rceil }$ being the lower bound of the interval ${\displaystyle I_{i}}$,
• let ${\displaystyle \ell '_{t}=\ell _{i}}$.

The constraints satisfied by run are, for each ${\displaystyle i\geq 0}$ integral and ${\displaystyle t\geq 0}$ real:

• ${\displaystyle \ell _{0}\in L_{0}}$,
• ${\displaystyle (\ell _{i},r_{i},\ell _{i+1})\in E}$,
• ${\displaystyle \nu _{i+1}=(\nu _{i}+\mid I_{i}\mid )[r_{i}\rightarrow 0]}$,
• ${\displaystyle \nu '_{t}\models \beta (\ell '_{t})}$.

The signal defined by this run is the function ${\displaystyle \sigma '}$ defined above. It is said that the run defined above is a run for the signal ${\displaystyle \sigma '}$.

The notion of accepting run is defined as in finite automata for finite words and as in Büchi automata for infinite words. That is, if ${\displaystyle w}$ is finite of length ${\displaystyle n}$, then the run is accepting if ${\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 ${\displaystyle i}$ such that ${\displaystyle \ell _{i}\in F}$.

A signal ${\displaystyle \gamma }$ is said to be accepted by a signal automaton ${\displaystyle {\mathcal {A}}}$ if there exists a run of ${\displaystyle {\mathcal {A}}}$ on ${\displaystyle \gamma }$ accepting it. The set of signals accepted by ${\displaystyle {\mathcal {A}}}$ is called the language accepted by ${\displaystyle {\mathcal {A}}}$ and is denoted by ${\displaystyle {\mathcal {S(A)}}}$.

As in the case of finite and Büchi automaton, a signal-automaton may be deterministic or non-deterministic. Intuitively, being deterministic as the same meaning in each of those case. It means that the set of start locations is a singleton, and that, given an extended state ${\displaystyle s}$, and a letter ${\displaystyle a}$, there is only one possible extended state which can be reached from ${\displaystyle s}$ by reading ${\displaystyle a}$. More precisely, either it is possible to stay in the location longer, or there is at most one possible successor location.

Formally, this can be defined as follows:

• ${\displaystyle L_{0}}$ is a singleton
• for each location ${\displaystyle \ell \in L}$, for each transition ${\displaystyle (\ell ,r,\ell ')\in E}$, the two following zones are disjoint:
  • the zone defined by the clock constraint ${\displaystyle \beta (\ell )}$,
  • the zone defined by the clock constraint ${\displaystyle \beta (\ell ')}$ where the constraints on clocks of ${\displaystyle r}$ are removed,
• for each location transitions ${\displaystyle (\ell ,r',\ell ')\in E}$ and ${\displaystyle (\ell ,r'',\ell '')\in E}$, the two following zones are disjoint:
  • the zone defined by the clock constraint ${\displaystyle \beta (\ell ')}$ where the constraints on clocks of ${\displaystyle r'}$ are removed,
  • the zone defined by the clock constraint ${\displaystyle \beta (\ell '')}$ where the constraints on clocks of ${\displaystyle r''}$ are removed,

In order to simplify the definition of a run, some authors requires that each interval of a run is right-closed and left-open. This restrict automata to accept only signals whose underlying partition satisfies the same property. However, it ensures that at each time ${\displaystyle t\geq 0}$, ${\displaystyle \lim _{t\leftarrow x^{+}}f(x)=f(t)}$ for ${\displaystyle f}$ representing any of the function ${\displaystyle \sigma '}$, ${\displaystyle \nu '}$ or ${\displaystyle \ell '}$ introduced above.

A bipartite signal automaton is a signal automaton in which the run alternates between open intervals and singular intervals (i.e. intervals which are singletons). It ensures that the graph underlying the automaton is a bipartite graph, and thus that the set of locations can be partitioned into ${\displaystyle \{L^{o},L^{s}\}}$, the set of open locations and of singular locations. Since the first interval contains 0, it can not be an open location, it follows that ${\displaystyle L_{0}\subseteq L^{s}}$. In order to ensure that each singular location is indeed singular, for each location ${\displaystyle \ell }$, there must be a clock ${\displaystyle x_{\ell }}$ which is reset when entering ${\displaystyle \ell }$ and such that the clock constraint of ${\displaystyle \ell }$ contains ${\displaystyle x=0}$.

Any signal automaton can be transformed into an equivalent bipartite signal automaton. It suffices to replace each location ${\displaystyle \ell }$ by a pair of locations ${\displaystyle (\ell ^{o},\ell ^{s})}$ and introduce a new clock ${\displaystyle x}$, such that for each ${\displaystyle \ell }$, ${\displaystyle x_{\ell ^{s}}=x}$.

Nearby is pictured a bipartite automaton equivalent to the signal automaton from the example section. Rectangle states represents singular locations.

A bipartite signal automaton ensuring A holds discretely and at least once by time unit