Signal automaton explained

In automata theory, a field of computer science, a signal automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a signal automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton. Further, clocks can be reset. [1]

Example

Before formally defining what a signal automaton is, an example will be given. Let one consider the language

lL

of signals, over a binary alphabet

\{A,B\}

, which contains signals

\gamma

such that:

A

appears in singular intervals. That is, the set of times

\{t\mid\gamma(t)=A\}

is discrete, and

A

appears at least once during each interval of length one.This language can be accepted by the automaton pictured nearby.As for finite automaton, incoming arrows represents initial locations and double circle represents accepting locations. However, contrary to finite automata, letters occurs in locations and not in transition. This is because letters are emitted continuously and transitions are taken discretely. The symbol

x

represents a clock. This clock allow to measure the time since the last time where

A

was emitted. Thus

x=0

ensures that

A

is emitted discretely. And

1>x

ensures that no more than a unit of time can pass without

A

occurring.

Formal definition

Signal automaton

Formally, a signal automaton is a tuple

lA=\langle\Sigma,L,L0,C,F,\alpha,\beta,E\rangle

that consists of the following components:

\Sigma

is a finite set called the alphabet or actions of

lA

.

L

is a finite set. The elements of

L

are called the locations or states of

lA

.

C

is a finite set called the clocks of

lA

.

L0\subseteqL

is the set of start locations.

F\subseteqL

is the set of accepting locations.

\alpha:L\to\Sigma

which associates a letter to each location.

\beta:L\tolB(C)

which associate a clock constraints to each location, and

E\subseteqL x lP(C) x L

is a set of edges, called transitions of

lA

, where

lP(C)

is the powerset of

C

.

An edge

(\ell,r,\ell')

from

E

is a transition from locations

\ell

to

\ell'

which reset the clocks of

r

.

Extended state

A pair with a location

\ell

and a clock valuation

\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

L

. For the sake of the clarity, this article will use the term location for element of

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.

Run

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

\xrightarrow[\nu0]{C}(\ell0,I0)\xrightarrow[\nu1]{r1}(\ell1,I1)...

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

(\sigmai)

,

(\nui)

,

(\elli)

are now introduced. Let

i\ge0

integral and

t\inIi

, then

\sigma't

be equal to

\sigmai

,

\nu't

be

\nui+t-\lceilIi\rceil

with

\lceilIi\rceil

being the lower bound of the interval

Ii

,

\ell't=\elli

.

The constraints satisfied by run are, for each

i\ge0

integral and

t\ge0

real:

\ell0\inL0

,

(\elli,ri,\elli+1)\inE

,

\nui+1=(\nui+\midIi\mid)[ri0]

,

\nu't\models\beta(\ell't)

.

The signal defined by this run is the function

\sigma'

defined above. It is said that the run defined above is a run for the signal

\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

w

is finite of length

n

, then the run is accepting if

\elln\inF

. If the word is infinite, then the run is accepting if and only if there exists an infinite number of position

i

such that

\elli\inF

.

Accepted signals and language

A signal

\gamma

is said to be accepted by a signal automaton

lA

if there exists a run of

lA

on

\gamma

accepting it. The set of signals accepted by

lA

is called the language accepted by

lA

and is denoted by

l{S(A)}

.

Deterministic signal automaton

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

s

, and a letter

a

, there is only one possible extended state which can be reached from

s

by reading

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:

L0

is a singleton

\ell\inL

, for each transition

(\ell,r,\ell')\inE

, the two following zones are disjoint:

\beta(\ell)

,

\beta(\ell')

where the constraints on clocks of

r

are removed,

(\ell,r',\ell')\inE

and

(\ell,r'',\ell'')\inE

, the two following zones are disjoint:

\beta(\ell')

where the constraints on clocks of

r'

are removed,

\beta(\ell'')

where the constraints on clocks of

r''

are removed,

Simplified signal automata

Depending on the authors, the exact definition of signal automata may be slightly different. Two such definitions are now given.

Half-open intervals

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

t\ge0

,
\lim
t\leftarrowx+

f(x)=f(t)

for

f

representing any of the function

\sigma'

,

\nu'

or

\ell'

introduced above.

Bipartite signal automaton

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

\{Lo,Ls\}

, 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

L0\subseteqLs

. In order to ensure that each singular location is indeed singular, for each location

\ell

, there must be a clock

x\ell

which is reset when entering

\ell

and such that the clock constraint of

\ell

contains

x=0

.

Any signal automaton can be transformed into an equivalent bipartite signal automaton. It suffices to replace each location

\ell

by a pair of locations

(\ello,\ells)

and introduce a new clock

x

, such that for each

\ell

,
x
\ells

=x

.

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

Synchronization of automata

The notion of product of finite automaton is extended to signal automaton. However, such a product is called a synchronization of automaton to emphasize the fact that the time should pass similarly in both automata considered. The main difference between synchronization and product is that, when two finite automata read the same word, they take transition simultaneously. This is not the case anymore for signal automata, since they can take transition at arbitrary time. Thus, the transition relation of a signal automaton may allow transition to be taken in one or two automata.

Let

lA1=\langle\Sigma,L1,L

1,F
0,C

1,\alpha1,\beta1,E1\rangle

and

lA2=\langle\Sigma,L2,L

2,F
0,C

2,\alpha2,\beta2,E2\rangle

two signal automata, their synchronization is the signal automaton

lA1 ⊗ lA2=\langle\Sigma,\{(\ell1,\ell2)\inL1 ⊗ L2\mid\alpha1(\ell1)=\alpha2(\ell2)\},L

1
0 ⊗
1\cup
L
0,C

C2,F1 ⊗ F2,(\ell1,\ell2)\mapsto\alpha1(\ell1),(\ell1,\ell2)\mapsto\beta1(\ell1)\land\beta2(\ell2),E\rangle

, where

E

contains the following transitions:

((\ell1,\ell2),r1,(\ell\prime1,\ell2)

for

(\ell1,r,\ell\prime1)\inE1

, and similarly for

E2

,

((\ell1,\ell2),r1\cupr2,(\ell\prime1,\ell\prime2)

for

(\ell1,r,\ell\prime1)\inE1

and

(\ell2,r,\ell\prime2)\inE2

.

Difference with timed automata

Timed automata is another extension of finite automata, which adds a notion of time to words. We now state some of the main differences between timed automata and signal automata.

In timed automata, letters are emitted on the transitions and not in the locations. As explained above when comparing signal automata to finite automata, letters are emitted on transitions when the words are emitted discretely, as for words and timed-words while they are emitted on locations when letters are emitted continuously, as for signals.

In timed automata, guards are only checked on transitions. This simplifies the definition of deterministic automaton, since it means that the constraint must be satisfied before the clocks are restarted.

See also

Notes

  1. Brihaye . Thomas . Geeraerts . Gilles. Ho. Hsi-Ming. Monmege. Benjamin . Timed-Automata-Based Verification of MITL over Signals . 24th International Symposium on Temporal Representation and Reasoning (TIME 2017) . 2017. 90 . 7:1–7:19. 10.4230/LIPIcs.TIME.2017.7. free .