Pattern Formulas

Pattern Formulas
Next: Bibliography Up: Input Formulas Previous: Counter 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 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}$

Kristin Yvonne Rozier 2007-05-10