Next:
Bibliography Up: Input Formulas Previous: Counter Formulas

Pattern Formulas

These scripts generate formulas from the eight classes of scalable formulas defined by [3] to evaluate the performance of model checking algorithms on temporally-complex formulas.


Run them like this:
formula.pl [-v] n
where $n$ is the number of variables (ie the size) of the formula you desire. The flag -v is for ``verbose.''

\begin{displaymath}E(n) = \bigwedge_{i=1}^{n} \Diamond p_i \end{displaymath}

\begin{displaymath}U(n) = (\ldots (p_1  \mathcal{U}  p_2)  \mathcal{U}  \ldots)  \mathcal{U}  p_n \end{displaymath}

\begin{displaymath}R(n) = \bigwedge_{i=1}^{n} (\Box \Diamond p_i \vee \Diamond \Box p_{i+1}) \end{displaymath}

\begin{displaymath}U_2(n) = p_1  \mathcal{U}  (p_2  \mathcal{U}  (\ldots p_{n-1}  \mathcal{U}  p_n) \ldots ) \end{displaymath}

\begin{displaymath}C_1(n) = \bigvee_{i=1}^{n} \Box \Diamond p_i \end{displaymath}

\begin{displaymath}C_2(n) = \bigwedge_{i=1}^{n} \Box \Diamond p_i \end{displaymath}

\begin{displaymath}Q(n) = \bigwedge (\Diamond p_i \vee \Box p_{i+1}) \end{displaymath}

\begin{displaymath}S(n) = \bigwedge_{i=1}^{n} \Box p_i \end{displaymath}

  1. Eformula.pl
  2. Uformula.pl
  3. Rformula.pl
  4. U2formula.pl
  5. C1formula.pl
  6. C2formula.pl
  7. Qformula.pl
  8. Sformula.pl



Kristin Yvonne Rozier 2007-05-10