Lab for Automated Reasoning and Analysis LARA

Regular Expressions and Automata with Parallel Inputs

Given an alphabet $\Sigma$, we consider a larger (but still finite) alphabet $\Sigma^n$ for some $n$. Keep in mind that $(a_1,\ldots,a_n) \in \Sigma_n$ is just one symbol; we often write it as

\begin{equation*}\left(
   \begin{array}{l}
      a_1 \\
      \ldots \\
      a_n
   \end{array}
   \right)
\end{equation*}

We can consider

  • regular expression
  • automata

on such alphabets.

Using Propositional Formulas to Denote Finite Sets of Symbols

Suppose $\Sigma = \{0,1\}$.

Let $n=3$.

$\Sigma^3 = \{ (0,0,0),(0,0,1),\ldots,(1,1,1) \}$.

Language representing that the third coordinate is the logical and of the first two is:

\begin{equation*}
  \left(
  \left(
   \begin{array}{l}
    0 \\
    0 \\
    0 \\
   \end{array}
   \right)
  +
  \left(
   \begin{array}{l}
    0 \\
    1 \\
    0 \\
   \end{array}
   \right)
  +
  \left(
   \begin{array}{l}
    1 \\
    0 \\
    0 \\
   \end{array}
   \right)
  +
  \left(
   \begin{array}{l}
    1 \\
    1 \\
    1 \\
   \end{array}
   \right)
   \right)^*
\end{equation*}

Instead of considering $\Sigma^3$, we can consider $\{x,y,z\} \to \Sigma$ where $x,y,z$ are three names of variables.

We then use propositional formulas to denote possible values of bits. For example, $[x \land y]$ denotes the regular expression

\begin{equation*}
  \left(
   \begin{array}{l}
    1 \\
    1 \\
    0 \\
   \end{array}
   \right)
  +
  \left(
   \begin{array}{l}
    1 \\
    1 \\
    1 \\
   \end{array}
   \right)
\end{equation*}

The bitwise and relation, shown above, is given by

\begin{equation*}
    [z \leftrightarrow (x \land y)]^*
\end{equation*}

In general

\begin{equation*}
  [p(v_1,\ldots,v_n)] = 
  \left(
   \begin{array}{l}
    a_{11} \\
    \ldots \\
    a_{1n} 
   \end{array}
   \right)
+ \\
\ldots \\
+ \\
  \left(
   \begin{array}{l}
    a_{k1} \\
    \ldots \\
    a_{kn} 
   \end{array}
   \right)
\end{equation*}

where $p(v_1,\ldots,v_n)$ is a propositional formula and $(a_{i1},\ldots,a_{in})$ for $1 \leq i \leq k$ are all tuples of values of propositional variables for which $p(v_1,\ldots,v_n)$ is true.

Notational advantage: even if we increase the number of components by adding new variables, the expression remains the same.

 
regular_expressions_for_automata_with_parallel_inputs.txt · Last modified: 2015/04/21 17:32 (external edit)
 
© EPFL 2018 - Legal notice