\newcommand{\ws}[1]{\phantom{#1}}

\newcommand{\event}{\ensuremath{F}}
\newcommand{\glob}{\ensuremath{G}}
\newcommand{\nex}{\ensuremath{X}}
\newcommand{\unt}{\ensuremath{U}}
\newcommand{\release}{\ensuremath{R}}
\newcommand{\wrelease}{\ensuremath{W}}

\newenvironment{ltltabular}[1]
  {\begin{tabular}{ |l|*{#1}{c|} } \hline}
  {\end{tabular}}

\ExplSyntaxOn
\NewDocumentCommand{\ltlrow}{m} {
   \seq_set_split:Nnn \ltl_row {|} { #1 }
   \seq_use:Nn \ltl_row { & }
   \\
   \hline
  }
\seq_new:N \ltl_row % allocate a sequence
\ExplSyntaxOff

\ExplSyntaxOn
\NewDocumentCommand{\ltlSteps}{+m +m} {
  \int_set:Nn \l_end {#1}
  \int_set:Nn \l_iter {0}
  \int_do_until:nNnn {\l_iter} = {\l_end} {
    \seq_put_right:Nx \ltl_steps { \int_use:N \l_iter}
    \int_incr:N \l_iter
  }
  \seq_put_right:Nn \ltl_steps { \multicolumn{#2}{c|}{ $\omega$ } }
  \seq_put_left:Nn \ltl_steps { Step }
  \seq_use:Nn \ltl_steps { & }
  \\
  \hline
}
\int_new:N \l_end
\int_new:N \l_iter
\seq_new:N \ltl_steps % allocate a sequence
\ExplSyntaxOff

\newcommand{\ltlTrace}[2]{
  \def\VARIABLE{#1}%
  \VARIABLE & \ltlrow{#2}
}

\newcommand{\ltlFormula}[2]{
  \def\FORMULA{#1}%
  \FORMULA & \ltlrow{#2}
}