\documentclass[11pt,oneside]{fithesis} \emergencystretch 8pt \usepackage[plainpages=false, pdfpagelabels]{hyperref} \usepackage{array} \usepackage{amsmath, amssymb} \usepackage{amsthm} \usepackage{graphicx} \usepackage{algorithm} \usepackage{xtab} \usepackage{subfig} \usepackage{algorithmic} \usepackage{hyperref} \thesislang{en} \thesistitle{Parallel verification of LTL(F,G) properties} \thesissubtitle{Master's Thesis} \thesisstudent{Jitka Kudrn\'{a}\v{c}ov\'{a}} \thesiswoman{true} \thesisfaculty{fi} \thesisyear{spring 2008} \thesisadvisor{RNDr. Jan Strej\v{c}ek, Ph. D.} \begin{document} \FrontMatter \ThesisTitlePage \begin{ThesisDeclaration} \DeclarationText \AdvisorName \end{ThesisDeclaration} \begin{ThesisAbstract} Computational complexity of model checking is the reason, why researchers are trying to find ways how to lower the amount of memory and time needed for the model checking procedure. When considering specification formulae for model checking only from the fragment LTL($\mathsf{F,G}$), there is a way how to translate the specification formula into a finite disjunction of formulae in special form called $\alpha$-formulae. Then, instead of verifying the original formula, we verify every formula in the disjunction. The implementation of this translation of formulae from the fragment LTL($\mathsf{F,G}$) into the finite disjunction of $\alpha$-formulae (see \cite{tech-rep}) is the main objective of this thesis. Since every $\alpha$-formula can be easily translated into a B\"uchi automaton and there is a strong probability that this automaton will be significantly smaller than the automaton obtained by traditional translation of LTL formulae into B\"uchi automata, the translation of $\alpha$-formula into a B\"uchi automaton will be implemented as well. Afterwards, model checking of $\alpha$-formulae will be evaluated within the DiVinE environment. \end{ThesisAbstract} \begin{ThesisKeyWords} Linear temporal logic, model checking, $\alpha$-formulae. \end{ThesisKeyWords} \begin{ThesisThanks} Here I would like to thank my family and Shkodran for their support while I was working on this thesis. I would also like to thank my advisor for his supervision. \end{ThesisThanks} \MainMatter \tableofcontents \chapter{Introduction} Disastrous events caused by errors in software that have occured in the past few years, like the crash of Ariane 5, have drawn the attention to the validation of the critical software systems, e.g. of the air traffic control system or medical systems, to name a few. The two methods for debugging a system that are still in use, namely simulation and testing, have shown up to be improper because they cannot, in principle, test all the possible inputs and all the possible behaviors of the software, they test only some of them. The other method, theorem proving, is, contrary to the first two, very expensive and time-consuming and requires the full-time attention of an expert, mathematician or logician. This method can, however, really prove the model of the system to be error-free. Verification enjoys some important advantages -- it can search through all the behaviors of the system and therefore can reveal errors which testing or simulation would not detect, and if an error is found, the trace which led to the erroneous state of the program is produced. This counterexample is particularly useful for finding the bug in the system and for removing this unwanted behavior. Specification of the properties which are supposed to verify is often given in some temporal logic. In this thesis we deal only with LTL, linear temporal logic, namely its fragment LTL($\mathsf{F,G}$), which is fragment of LTL with the temporal operators $\mathsf{F, G}$ only. However, verification, namely model checking, suffers from the \textit{state space explosion problem} -- the number of all the possible states of the system is too high and therefore it is sometimes infeasible to verify properties of a system on a single machine or the verification takes a very long time. There are many ways to reduce this problem, one of them is the possibility of distribution the computation task among more computers and computing this task in parallel. This solution uses DiVinE (\cite{ANNA}), distributed verification environment, developed by the Parallel and distributed systems laboratory (ParaDiSe) at Masaryk University, Brno. %We used DiVinE for our computations for the purpose of this thesis. \section{Work objectives} %We hoped that translation of the specification formula into the finite disjuction of formulae in a special form will help us to reduce the amount of memory needed for verification -- every formula of the disjunction could be verified independently. The main purpose of this thesis is to implement an algorithm for translation the specification formula into a finite disjunction of formulae in a special form called $\alpha$-formulae. We hope that verification of every part of this disjunction can save us time and/or memory compared to the verification of the original formula. Also, the fact, that the original formula is equivalent to the finite disjunction of $\alpha$-formulae, gives us the possibility of parallel computation -- every part in the disjunction, every $\alpha$-formulae, can be verified independently of the other parts of the disjunction. It will be also presented and implemented the translation of conjunction of $\alpha$-formulae into the equivalent finite disjunction of $\alpha$-formulae. Every $\alpha$-formula can be easily translated into a B\"{u}chi automaton, this algorithm for converting the $\alpha$-formulae into a B\"{u}chi automaton will also be implemented, since we hope that, compared to the translation of LTL formula into B\"uchi automata presented in \cite{fast-ltl} and implemented in DiVinE, we would be able to use less memory to store the automaton. All the above mentioned implementations will then be tested on models found in \cite{BEEM} within DiVinE. The amount of time and memory needed for verification the $\alpha$-formulae will then be compared with the amount of memory and time needed for verification of the original formula within DiVinE. The thesis is organized as follows. The second chapter recalls some basic terms and definitions. In chapter three we define $\alpha$-formulae. We also present the way how to translate the conjunction of $\alpha$-formulae into the equivalent disjunction of $\alpha$-formulae. The next chapter deals with the translation of formulae from the fragment LTL($\mathsf{\mathsf{F_s}, \mathsf{G_s}}$) into the disjunction of finitely many $\alpha$-formulae. In the following chapter is presented an algorithm for translating the $\alpha$-formulae into a B\"{u}chi automaton. Technical details on implementation itself can be found in Chapter 6. The last chapter presentes and evaluates the experimental results. \chapter{Preliminaries} In this section we present the way how a system is formalized and we also present the model checking problem for LTL logic. %\section{Model Checking} The process of model checking has the following three parts: \begin{itemize} \item \textbf{Modelling} First, we must transform the input system into the mathematical formalism which is accepted by the model checking tool. The modelling often requires some level of abstraction because the systems we model are often infinite or the state space (the space of all possible states of the system) is simply too large to be stored in a computer memory. \item \textbf{Specification} Now we must specify the properties -- invariants for example. This is usually given as formula of temporal logic for example linear temporal logic (LTL). \item \textbf{Verification} It is a fully automatic part. The model checker now goes through the whole state space of the system. At the end of this procedure, the output of the model checker is either \textit{yes} or \textit{no}. In the first case, we now know that the model of the system has the property specified in the specification formula. In case of the latter, the counterexample is produced as well. This counterexample can help the designers of the verified system to clear out the unwanted behavior. However, this error trace is sometimes not present in the original system, because it is the model that is erroneous, not the system itself. This is often called the \textit{false negative} and it can help the modellers to improve the specification formula or a model of the input system. \end{itemize} Now we present the formalism for modelling the systems, namely the Kripke structures \cite{model}. \\ \textbf{Definition.} Let \textit{AP} be a set of atomic propositions. A \textit{Kripke structure M} over \textit{AP} is a four tuple $M = (S, S_0, R, L)$ where \begin{itemize} \item $S$ is a finite set of states \item $S_0 \subseteq S$ is a set of initial states \item $R \subseteq S \times S$ is a transition relation that must be total (that is, for every state $s \in S$ there is a state $s' \in S$ such that $R(s,s')$) \item $L : S \rightarrow 2^{AP}$ is a function that labels each state with the set of atomic propositions true in that state. \end{itemize} A \textit{path} in Kripke structure is a sequence of states $q_{0},q_{1},q_{2}... $ such that for every $i \geq 0$ it holds $(q_i, q_{i+1}) \in R$ (often written as $q_i \rightarrow q_{i+1}$); the path can be finite or infinite. A \textit{run} of a Kripke structure is an infinite path which begins in one of the initial states. \section{Linear Time Logic} While Kripke structures are suitable for modelling systems, temporal logics are very suitable for specifying the system properties. In temporal logics, one of the most popular logics is the linear temporal logic, LTL \cite{Pnueli77}. Let $AP = \lbrace a,b, \ldots \rbrace$ be a countably infinite set of atomic actions. LTL syntax is defined as \begin{center} $\varphi ::= tt\; |\; a\; |\; \neg \varphi \;|\; \varphi \wedge \varphi \;|\; \mathsf{X} \, \varphi\; |\; \varphi \, \mathsf{U}\, \varphi, \;$ \end{center} where $a$ ranges over $AP$. $\mathsf{X}$ is called \textit{next}, $\mathsf{U}$ is called \textit{until}. Other boolean connectives ($\vee, \Rightarrow, \Leftrightarrow$) are defined in a standard way. The logic is interpreted over words. Given a word $u$, for all $0 \leq i < |u|$, $u(i)$ denotes the $(i+1)^{th}$ letter of $u$ ($|u|$ denotes the length of the word), $u = u(0)u(1)u(2)...$. Moreover, for all $0 \leq i < |u|$, $u(i)$, let us denote $u_i$ as the $i^{th}$ suffix of $u$, $u_i = u(i)u(i+1)u(i+2)...$. A \textit{pointed word} is a pair $(u,i)$ of $u \neq \varepsilon$ and a \textit{position} $0 \leq i < |u|$ in this word. \textbf{Definition.} Let $\varphi$ be an LTL formula and $(u,i)$ be a pointed word. We define that a formula $\varphi$ is \textit{valid} for the position $i$ in the word $u$, written $(u,i) \models \varphi$, by induction on the structure of $u$. \begin{center} \begin{minipage}{250pt} {\baselineskip=20pt \begin{tabbing} \hspace{80pt}\=\hspace{20pt}\=\kill $(u,i) \models tt$ \> \> $ \mathsf{always}$ \\ $(u,i) \models a$ \> $\Leftrightarrow$ \> $a \in u(i)$ \\ $(u,i) \models \neg \varphi $ \> $\Leftrightarrow$ \> $(u,i) \nvDash \varphi$\\ $(u,i) \models \varphi_{1} \wedge \varphi_{2} $ \> $\Leftrightarrow$ \> $ (u,i) \models \varphi_{1}\; \wedge\; (u,i) \models \varphi_{2}$\\ $(u,i) \models \mathsf{X}\varphi $ \> $\Leftrightarrow$ \> $(u,i+1) \models \varphi $ \\ $(u,i) \models \varphi_{1} \mathsf{U} \varphi_{2} $ \> $\Leftrightarrow \exists k \geq i.\, (u,k) \models \varphi_2 \;\wedge$ \\ \> \> $ \wedge \;\forall j.(i \leq j 0,$ \item $\theta_i \in LTL() $ for each $i \leq n + 1,$ \item $O_i$ is either $`\mathsf{U}`$ or $`\mathsf{U}_+`$ or $`\wedge \mathsf{X}`$ for each $i < n$, \item $O_n$ is $`\wedge \mathsf{G_s}`.$ \end{itemize} Let $\mathcal{B} \subseteq LTL()$ be a finite set. An $\alpha$-formula is defined as \begin{center} $\alpha(\delta, \mathcal{B}) = (\theta_1 O_1(\theta_2 O_2 ... (\theta_n O_n \theta_{n+1})...)) \; \wedge \; \bigwedge_{\psi \in \mathcal{B}} \mathsf{G_s} \mathsf{F_s} \psi$ \end{center} The fragment $\mathcal{A}$ consists of finite disjunction of $\alpha$-formulae. \vspace{\baselineskip} An infinite word $u$ satisfies $\alpha(\delta, \mathcal{B})$, iff $u$ can be rewritten as \begin{center} $u_1 \cdot u_2 \cdot \ldots \cdot u_{n+1}$, \end{center} where \begin{itemize} \item for each $u_i$, $1 \leq i \leq n, u_i$ is a finite sequence of sets of atomic propositions such that $u_i \models \mathsf{G} \theta_i$ and \begin{itemize} \item $|u_i| \geq 0$ if $O_i = \mathsf{U}$ \item $|u_i| > 0$ if $O_i$ is $\mathsf{U}_+$ \item $|u_i| = 1$ if $O_i = \wedge \mathsf{X}$ or $O_i = \wedge \mathsf{G_s}$ \end{itemize} \item $u_{n+1}$ is and infinite word satisfying $\mathsf{G_s} \theta_{n+1} \wedge \bigwedge_{\psi \in \mathcal{B}} \mathsf{G_s} \mathsf{F_s} \psi$. \end{itemize} \textbf{Theorem 4.1.} A conjunction of two $\alpha$-formulae can be converted into an equivalent disjunction of $\alpha$-formulae. \vspace{\baselineskip} \begin{proof} % Let $\alpha(\delta_1, \mathcal{B}_1)$ and $\alpha(\delta_2, \mathcal{B}_2)$ be the two formulae in the conjunction.Let us $n,m$ denote the number of operators in each $\delta$-part of the formulae, respectively. % % The set $\mathcal{B}$ of every $\alpha$-formula in the disjunction will be $\mathcal{B}_1 \cup \mathcal{B}_2$. We show how to construct the $\delta$ part. %$\phi_1 \theta_1 O_1 \theta_2 \dots \wedge \mathsf{G_s} \theta_{n+1}$ %$\phi_2 = \theta_1' O_1' \theta_2' \dots \wedge \mathsf{G_s} \theta_{m+1}'$ Let $\alpha_1 = \alpha(\delta_1, \mathcal{B}_1)$ and $\alpha_2 = \alpha(\delta_2, \mathcal{B}_2)$. Let $\delta_1 = \theta_1 O_1 \theta_2 O_2 \cdots \theta_n O_n \theta_{n+1}$, $\delta_2 = \theta_1' O_1' \theta_2' O_2' \cdots \theta_m' O_m' \theta_{m+1}'$. By $\gamma_1 \vee \gamma_2 \vee \cdots \vee \gamma_k$ we denote the result of the conjunction $\alpha_1 \wedge \alpha_2$, $\gamma_i = \alpha(\delta_{\gamma_i}, \mathcal{B})$ for all $1 \leq i \leq k$. Clearly, the set $\mathcal{B}$ in each of the $\gamma_i$, $1 \leq i \leq k$, formulae will be $\mathcal{B}_1 \cup \mathcal{B}_2$. We will now present how to create the $\delta$-parts of the $\gamma_i$ formulae. The proof is done by induction on $n + m$. Without loss of generality, let us suppose $n \leq m$. \begin{itemize} \item Case $n=m=1$: In this case, the $\delta$-parts are \\ $\delta_1 = \theta_1 \wedge \mathsf{G_s} \theta_2$ \\ $\delta_2 = \theta_1' \wedge \mathsf{G_s} \theta_2'$. Clearly, $\alpha_1 \wedge \alpha_2 = \gamma_1 = \alpha(\delta_{\gamma_1}, \mathcal{B})$, where $\delta_{\gamma_1} = (\theta_1 \wedge \theta_1') \wedge \mathsf{G_s}(\theta_2 \wedge \theta_2')$. \item Case $n=1, m>1$: The $\delta$ parts of $\alpha_1, \alpha_2$ now are: \\ $\delta_1 = \theta_1 \wedge \mathsf{G_s} \theta_2$ \\ $\delta_2 = \theta_1' O_1' \theta_2' \dots \wedge \mathsf{G_s} \theta_{m+1}'$ This case is divided into subcases according to the $O_1'$. \begin{itemize} \item $O_1' = \wedge \mathsf{X}$ : Let $u_1, u_1' \in 2^{{AP}^*}$ be the words satisfying $\theta_1, \theta_1'$ ($u_1 \models \mathsf{G} \theta_1, u_1' \models \mathsf{G} \theta_1'$). As $O_1 = \wedge \mathsf{\mathsf{G_s}}$ and $O_1' = \wedge \mathsf{\mathsf{X}}$, the lengths of $u_1, u_1'$ are both equal to one. Hence, $\alpha_1 \wedge \alpha_2 = \gamma_1 = \alpha(\delta_{\gamma_1}, \mathcal{B})$, where $\delta_{\gamma_1} = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} (\theta_2 \wedge \theta_2') \dots \wedge \mathsf{G_s}(\theta_2 \wedge \theta_{m+1}')$ % constructed as $\delta = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} (\theta_2 % \wedge \theta_2') \dots \wedge \mathsf{G_s}(\theta_2 \wedge \theta_{m+1}')$ \item $O_1' = \mathsf{U}_+$ : Again, let $u_1, u_1' \in 2^{{AP}^*}, u_1 \models \mathsf{G} \theta_1, u_1' \models \mathsf{G} \theta_1'$. Since $O_1 = \wedge \mathsf{\mathsf{G_s}}$, $|u| = 1$. $O_1' = \mathsf{\mathsf{U}_+}$, hence $|u_1'| > 0$ In now can be easily seen, that $\alpha_1 \wedge \alpha_2 = \gamma_1 = \alpha(\delta_{\gamma_1}, \mathcal{B})$, where $\delta_{\gamma_1} = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} (\theta_2 \wedge \theta_1') \mathsf{U} (\theta_2 \wedge \theta_2') \dots \wedge \mathsf{G_s}(\theta_2 \wedge \theta_{m+1}')$. % Let $u_1$, $u_1'$ be the words satisfying $\theta_1$ and $\theta_1'$, respectively, and $|u_1| \leq |u_1'|$. It can be easily seen that $\delta = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} (\theta_2 \wedge \theta_1') \mathsf{U} (\theta_2 \wedge \theta_2') \dots \wedge \mathsf{G_s}(\theta_2 \wedge \theta_{m+1}')$ \item $O_1' = \mathsf{U}$ : % We can transform the $\delta_2$ part into two different ones, using only operator $\mathsf{U}_+$ as follows: We will transform the formula $\alpha_2$ into an equivalent disjunction of two $\alpha$-formulae, $\alpha_2' = \alpha(\delta_2', \mathcal{B})$ and $\alpha_2'' = \alpha(\delta_2'', \mathcal{B})$. We will then compute $(\alpha_1 \wedge \alpha_2') \vee (\alpha_1 \wedge \alpha_2'')$ instead of $\alpha_1 \wedge \alpha_2$. $ \delta_2' = \theta_1' \mathsf{U}_+ \theta_2' \dots \wedge \mathsf{G_s} \theta_{m+1}'$ $\delta_2'' = \theta_2' O_2' \theta_3' \dots \wedge \mathsf{G_s} \theta_{m+1}'$ \end{itemize} \textbf{Induction hypothesis}: we can now assume, that the conjunction can be constructed for the formulae with $\delta$-parts of lengths $n-1, m$ or $n, m-1$ or $n-1, m-1$. \item $n>1, m>1$ To simplify, let us denote: $\delta_1 = \theta_1 O_1 \delta_1'$ \\ $\delta_2 = \theta_1' O_1' \delta_2'$ This case is divided into the following subcases according to the corresponding operators. We assume that there is no $\mathsf{U}$ operator in $\delta_1, \delta_2$ because $\alpha$-formula with operator $\mathsf{U}$ in its $\delta$-part can be transformed into a disjunction of two other $\alpha$-formulae without operator $\mathsf{U}$ in its $\delta$-parts as was follows: Let $\alpha_3 = \alpha( \delta_3, \mathcal{B}_3)$ is a $\alpha$-formula and $\delta_3 = \theta_1 O_1 \theta_2 O_2 \cdots \theta_k \mathsf{U} \theta_{k+1} \cdots \theta_o O_o \theta_{o+1}$, $1 \leq k \leq o-1 $ Then $\alpha_3$ is equivalent to the disjunction $\alpha_4 \vee \alpha_5 = \alpha(\delta_4, \mathcal{B}_3) \vee \alpha(\delta_5, \mathcal{B}_3)$, where $\delta_4 = \theta_1 O_1 \theta_2 O_2 \cdots \theta_k \mathsf{U}_+ \theta_{k+1} \cdots \theta_o O_o \theta_{o+1}$ and $\delta_5 = \theta_1 O_1 \theta_2 O_2 \cdots \theta_{k-1} O_{k-1} \theta_{k+1} \cdots \theta_o O_o \theta_{o+1}$. \begin{itemize} \item $O_1 = \wedge \mathsf{X}, O_1' = \wedge \mathsf{X}$ The $\delta$-parts now are: $\delta_1 = \theta_1 \wedge \mathsf{X} \delta_1'$, $\delta_2 = \theta_1' \wedge \mathsf{X} \delta_2'$. As $O_1 = O_1' = \wedge \mathsf{X}$, the lengths of words $u_1, u_1'\in 2^{{AP}^*}$ satisfying $\theta_1,$ $\theta_1'$ ($u_1 \models \mathsf{G} \theta_1, u_1' \models \mathsf{G} \theta_1'$) are equal to one. Let us also note that because $\delta_1'$ and $\delta_2'$ are strictly shorter than $\delta_1$ and $\delta_2$, one can compute the conjuction $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\delta_2', \mathcal{B}) = \gamma_1' \vee \gamma_2' \vee \cdots \vee \gamma_l' = \alpha(\delta_{\gamma_1'}, \mathcal{B}) \vee \alpha(\delta_{\gamma_2'}, \mathcal{B}) \vee \cdots \vee \alpha(\delta_{\gamma_l'}, \mathcal{B})$. The $\delta$-parts of the resulting formulae $\gamma_1 \vee \gamma_2 \vee \cdots \vee \gamma_l$ will be constructed as follows: $\gamma_i = \alpha(\delta_{\gamma_i}, \mathcal{B})$ for $1 \leq i \leq l$, where $\delta_{\gamma_i} = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} \delta_{\gamma_i'}$. \item $O_1 = \wedge \mathsf{X}, O_1' = \mathsf{U}_+$ % $\delta_1 = \theta_1 \wedge \mathsf{X} \theta$, $\delta_2 = \theta_1' \mathsf{U}_+ \theta'$. Let $u_1$ and $u_1'$ be the words satisfying $\theta_1$, $\theta_1'$; $|u_1| = |u_1'| = 1$. Therefore the word satisfying the conjunction of the two formulae must begin with $\theta_1 \wedge \theta_1'$ and, in case $\theta_1'$ is longer than one, continue with the conjunction of $\theta$ and $\theta_1' \mathsf{U}_+ \theta'$. % Again, due to the induction hypothesis, $\theta \wedge (\theta_1' \mathsf{U} \theta'))$ can be constructed, hence % $\delta = (\theta_1 \wedge \theta_1') \wedge \mathsf{X}(\theta \wedge % (\theta_1' \mathsf{U} \theta'))$ $\delta_1 = \theta_1 \wedge \mathsf{X} \delta_1'$ $\delta_2 = \theta_1' \mathsf{U}_+ \delta_2'$ $u_1, u_1' \in 2^{{AP}^*}$, $u_1 \models \mathsf{G} \theta_1, u_1' \models \mathsf{G} \theta_1'$ $O_1 = \wedge \mathsf{X} \Longrightarrow |u_1| = 1, O_1' = \mathsf{U}_+ \Longrightarrow |u_1'| > 0$ The word satisfying the conjunction of the $\alpha$-formulae must begin with the word satifying $\theta_1 \wedge \theta_1'$, and, if $|u_1'| > 1$, continue with the word satisfying the conjunction of $\alpha(\delta_1', \mathcal{B})$ and $\alpha(\theta_1' \mathsf{U} \delta_2', \mathcal{B})$. Due to the induction hypothesis, this conjunction can be constructed. Let $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\theta_1' \mathsf{U} \delta_2', \mathcal{B}) = \gamma_1' \vee \gamma_2'\vee \cdots \vee \gamma_k' = \alpha(\delta_{\gamma_1'}, \mathcal{B}) \vee \alpha(\delta_{\gamma_2'}, \mathcal{B}) \vee \cdots \vee \alpha(\delta_{\gamma_k'}, \mathcal{B})$. Therefore, the $\delta$-parts of the resulting formulae $\gamma_1, \gamma_2, \cdots, \gamma_k$ will be $\delta_{\gamma_i} = (\theta_1 \wedge \theta_1') \wedge \mathsf{X} \delta_{\gamma_i'}$ for $1 \leq i \leq k$. \vspace{\baselineskip} \item $ O_1 = \mathsf{U}_+, O_1' = \mathsf{U}_+$ $\delta_1 = \theta_1 \mathsf{U}_+ \delta_1'$ $\delta_2 = \theta_1' \mathsf{U}_+ \delta_2'$ $u_1, u_1' \in LTL()$, $u_1 \models \mathsf{G} \theta_1, u_1' \models \mathsf{G} \theta_1'$ $O_1 = O_1' = \mathsf{U}_+ \Longrightarrow |u_1| > 0, |u_1'| > 0 $ In general, we do not know anything about the lengths of words $u_1, u_1'$, therefore every possibility must be considered. Due to the induction hypothesis, the conjunctions $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\delta_2',\mathcal{B})$, $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\theta_1' \mathsf{U}_+\delta_2',\mathcal{B})$, $\alpha(\delta_2', \mathcal{B}) \wedge \alpha(\theta_1 \mathsf{U}_+\delta_1',\mathcal{B})$ can be constructed. Let $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\delta_2',\mathcal{B}) = \gamma_1' \vee \gamma_2' \vee \cdots \vee \gamma_k'$ $\alpha(\delta_1', \mathcal{B}) \wedge \alpha(\theta_1' \mathsf{U}_+\delta_2',\mathcal{B}) = \gamma_1'' \vee \gamma_2'' \vee \cdots \vee \gamma_l''$ $\alpha(\delta_2', \mathcal{B}) \wedge \alpha(\theta_1 \mathsf{U}_+\delta_1',\mathcal{B}) = \gamma_1''' \vee \gamma_2''' \vee \cdots \vee \gamma_o'''$ The $\delta$-parts of the resulting formulae will be: $\delta_{\gamma_i} = (\theta_1 \wedge \theta_1') \mathsf{U}_+ \delta_{\gamma_i'}$ for $1 \leq i \leq k$ $\delta_{\gamma_{i+k}} = (\theta_1 \wedge \theta_1') \mathsf{U}_+ \delta_{\gamma_i''}$ for $1 \leq i \leq l$ $\delta_{\gamma_{i+k+l}} = (\theta_1 \wedge \theta_1') \mathsf{U}_+ \delta_{\gamma_i'''}$ for $1 \leq i \leq o$ \end{itemize} \end{itemize} \end{proof} \chapter{Translation of LTL$(\mathsf{F_s}, \mathsf{\mathsf{G_s}})$ into $\mathcal{A}$} In this chapter we present an algorithm introduced in \cite{tech-rep} for translating any formula from the fragment LTL$(\mathsf{F_s}, \mathsf{\mathsf{G_s}})$ into the equivalent disjunction of $\alpha$-formulae. Because $\mathsf{F_s}$ and $\mathsf{\mathsf{G_s}}$ are dual modalities, in the following we assume that negations are only in front of atomic propositions. All the specification formulae we wish to translate into to the finite disjuntion of $\alpha$-formulae are from the fragment LTL($\mathsf{F},\mathsf{G}$). The following equivalences shows that this is no restriction. $\mathsf{F} \varphi_1 \equiv \varphi_1 \wedge \mathsf{F}_s \varphi_1$ $\mathsf{G} \varphi_1 \equiv \varphi_1 \wedge \mathsf{G}_s \varphi_1$ \vspace{\baselineskip} \textbf{Theorem 5.1.} Every LTL$(\mathsf{F_s}, \mathsf{\mathsf{G_s}})$ formula can be translated into an equivalent disjunction of $\alpha$-formulae. \vspace{\baselineskip} \textbf{Proof.} From the given formula $\varphi$, we construct a finite set $A_\varphi$ of $\alpha$-formulae, such that $\varphi$ is equivalent to a disjunction of formulae in $A_\varphi$. The proof is done by induction on the length of $\varphi$. Therefore, if $\varphi \notin LTL()$ we assume that for every formula $\varphi'$ from $LTL(\mathsf{F_s}, \mathsf{G_s})$ shorter that $\varphi$, we can construct the set $A_{\varphi'}$. In the following, $p$ denotes a formula of $LTL()$, i.e. boolean combination of actions. \begin{itemize} \item[$\bullet p$] Case $p$: $p$ is equivalent to $p \wedge \mathsf{G_s} tt$. Therefore $A_\varphi = \lbrace \alpha(p \wedge \mathsf{G_s} tt, \emptyset)\rbrace$. \item[$\bullet \vee$] Case $\varphi_1 \vee \varphi_2$: According to the induction hypothesis, we can assume we have already constructed the sets $A_{\varphi_1}$ and $A_{\varphi_2}$. Hence, the corresponding set is $A_\varphi = A_{\varphi_1} \cup A_{\varphi_2}$. \item[$\bullet \wedge$] Case $\varphi_1 \wedge \varphi_2$: Due to theorem 4.1, the set $A_\varphi$ can be constructed from the sets $A_{\varphi_1}$ and $A_{\varphi_2}$. \item[$\bullet \mathsf{F_s}$] Case $\mathsf{F_s} \varphi_1$: Because $\mathsf{F_s}(\alpha_1 \vee \alpha_2) \equiv (\mathsf{F_s} \alpha_1) \vee (\mathsf{F_s} \alpha_2)$ and $\mathsf{F_s}(\alpha \wedge \mathsf{G_s} \mathsf{F_s} \phi) \equiv (\mathsf{F_s} \alpha) \wedge (\mathsf{G_s} \mathsf{F_s} \phi)$, we have $A_\varphi = \lbrace \alpha(tt \,\mathsf{U}_+ \delta, \mathcal{B})\; |\; \alpha(\delta, \mathcal{B}) \in A_{\varphi_1} \rbrace$. \item[$\bullet \mathsf{G_s}$] Case $\mathsf{G_s} \varphi_1$: This case is divided into the following subcases according to the structure of $\varphi_1$: \begin{itemize} \item[$\circ p$] Case $\mathsf{G_s} p$: Because $\mathsf{G_s} p$ is equivalent to $tt \wedge \mathsf{G_s} p$, we have $A_\varphi = \lbrace \alpha(tt \wedge \mathsf{G_s} p, \emptyset)\rbrace$. \item[$\circ \wedge$] Case $\mathsf{G_s}(\varphi_2 \wedge \varphi_3)$: Because $\mathsf{G_s}(\varphi_2 \wedge \varphi_3) \equiv (\mathsf{G_s} \varphi_2) \wedge (\mathsf{G_s} \varphi_3)$, the set $A_\varphi$ can be constructed from sets $A_{\mathsf{G_s} \varphi_2}$ and $A_{\mathsf{G_s} \varphi_3}$ using theorem 4.1. \item[$\circ \mathsf{F_s}$] Case $\mathsf{G_s} \mathsf{F_s} \varphi_2$: This case is divided into the following subcases according to the structure of $\varphi_2$: \begin{itemize} \item[$\star p$] Case $\mathsf{G_s} \mathsf{F_s} p$: As $p \in LTL()$, we set $A_\varphi = \lbrace \alpha(tt \wedge \mathsf{G_s} tt, \lbrace p \rbrace) \rbrace$. \item[$\star \vee$] Case $G_S \mathsf{F_s}(\varphi_3 \vee \varphi_4)$: Because $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \vee \varphi_4) \equiv (\mathsf{G_s} \mathsf{F_s} \varphi_3) \vee (\mathsf{G_s} \mathsf{F_s} \varphi_4)$, we have $A_\varphi = A_{\mathsf{G_s} \mathsf{F_s} \varphi_3} \cup A_{\mathsf{G_s} \mathsf{F_s} \varphi_4}$. \item[$\star \wedge$] Case $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \varphi_4)$: This case is divided into the following subcases: \begin{itemize} \item[$\diamond p$] Case $\mathsf{G_s} \mathsf{F_s}(p_3 \wedge p_4)$: As $p_3 \wedge p_4 \in LTL()$, this case has been covered by case $\mathsf{G_s} \mathsf{F_s} p$. \item[$\diamond \vee$] Case $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge (\varphi_5 \vee \varphi_6))$: Because $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge (\varphi_5 \vee \varphi_6)) \equiv \mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \varphi_5) \vee \mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \varphi_6)$, we have $A_\varphi = A_{\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \varphi_5)} \cup A_{\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \varphi_6)}$. \item[$\diamond \mathsf{F_s}$] Case $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \mathsf{F_s} \varphi_5)$: Because $\mathsf{G_s} \mathsf{F_s} (\varphi_3 \wedge \mathsf{F_s} \varphi_5) \equiv (\mathsf{G_s} \mathsf{F_s} \varphi_3) \wedge (\mathsf{G_s} \mathsf{F_s} \varphi_5)$, the set $A_\varphi$ can be constructed from $A_{\mathsf{G_s} \mathsf{F_s} \varphi_3}$ and $A_{\mathsf{G_s} \mathsf{F_s} \varphi_5}$ using theorem 4.1. \item[$\diamond \mathsf{G_s}$] Case $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \mathsf{G_s} \varphi_5)$: Because $\mathsf{G_s} \mathsf{F_s}(\varphi_3 \wedge \mathsf{G_s} \varphi_5) \equiv (\mathsf{G_s} \mathsf{F_s} \varphi_3) \wedge (\mathsf{G_s} \mathsf{F_s} \mathsf{G_s} \varphi_5)$, the set $A_\varphi$ can be constructed from the sets $A_{\mathsf{G_s} \mathsf{F_s} \varphi_3}$ and $A_{\mathsf{G_s} \mathsf{F_s} \mathsf{G_s} \varphi_5}$ using theorem 4.1. \end{itemize} \item[$\star \mathsf{F_s}$] Case $\mathsf{G_s} \mathsf{F_s} \mathsf{F_s} \varphi_3$: As $\mathsf{G_s} \mathsf{F_s} \mathsf{F_s} \varphi_3 \equiv \mathsf{G_s} \mathsf{F_s} \varphi_3$, we have $A_\varphi = A_{\mathsf{G_s} \mathsf{F_s} \varphi_3}$. \item[$\star \mathsf{G_s}$] Case $\mathsf{G_s} \mathsf{F_s} \mathsf{G_s} \varphi_3$: A word $u$ satisfies $\mathsf{G_s} \mathsf{F_s} \mathsf{G_s} \varphi_3$ if and only if $|u| = 1$ or it is an infinite word satisfying $\mathsf{F_s} \mathsf{G_s} \varphi_3$ ($\mathsf{G_s} \neg tt$ is satisfied only by words of length one). Word $u$ satisfies $(\mathsf{F_s} tt) \wedge (\mathsf{G_s} \mathsf{F_s} tt)$ if and only if $u$ is infinite. Therefore, $\mathsf{G_s} \mathsf{F_s} \mathsf{G_s} \varphi_3 \equiv (\mathsf{G_s} \neg tt) \vee \varphi'$, where $\varphi' = (\mathsf{F_s} tt) \wedge (\mathsf{G_s} \mathsf{F_s} tt) \wedge (\mathsf{F_s} \mathsf{G_s} \varphi_3)$. Therefore $A_\varphi = A_{\mathsf{G_s} \neg tt} \vee A_{\varphi'}$, where $A_{\varphi'}$ is constructed from the sets $A_{\mathsf{F_s} tt}$, $A_{\mathsf{G_s} \mathsf{F_s} tt}$, and $A_{\mathsf{F_s} \mathsf{G_s} \varphi_3}$ using theorem 4.1. \end{itemize} \item[$\circ \vee$] Case $\mathsf{G_s}(\varphi_2 \vee \varphi_3)$: This case is divided into to the following subcases according to the structure of $\varphi_2$ and $\varphi_3$: \begin{itemize} \item[$\ast p$] Case $\mathsf{G_s}(p_2 \vee p_3)$: Because $p_2 \vee p_3 \in LTL()$, this case has been already covered by the case $\mathsf{G_s} p$. \item[$\ast \wedge$] Case $\mathsf{G_s}(\varphi_2 \vee (\varphi_4 \wedge \varphi_5))$: As $\mathsf{G_s}(\varphi_2 \vee (\varphi_4 \wedge \varphi_5)) \equiv \mathsf{G_s}(\varphi_2 \vee \varphi_4) \wedge \mathsf{G_s}(\varphi_2 \vee \varphi_5)$, the set $A_\varphi$ can be constructed from the sets $A_{\mathsf{G_s}(\varphi_2 \vee \varphi_4)}$ and $A_{\mathsf{G_s}(\varphi_2 \vee \varphi_5)}$ using theorem 4.1. \item[$\ast \mathsf{F_s}$] Case $\mathsf{G_s}(\varphi_2 \vee \mathsf{F_s} \varphi_4)$: As $\mathsf{G_s}(\varphi_2 \vee \mathsf{F_s} \varphi_4) \equiv (\mathsf{G_s} \varphi_2) \vee \mathsf{F_s}(\mathsf{F_s} \varphi_4 \wedge \mathsf{G_s} \varphi_2) \vee \mathsf{G_s} \mathsf{F_s} \varphi_4$, the set $A_\varphi$ can be constructed as $A_{\mathsf{G_s} \varphi_2} \; \cup \; \lbrace \alpha(tt\, \mathsf{U}_+ \delta, \mathcal{B}) \; | \; \alpha(\delta, \mathcal{B}) \in A_{\mathsf{F_s} \varphi_4 \wedge \mathsf{G_s} \varphi_2} \rbrace \; \cup \; A_{\mathsf{G_s} \mathsf{F_s} \varphi_4}$, where $A_{\mathsf{F_s} \varphi_4 \wedge \mathsf{G_s} \varphi_2}$ is created from the sets $A_{\mathsf{F_s} \varphi_4}$ and $A_{\mathsf{G_s} \varphi_2}$ using theorem 4.1. \item[$\ast \mathsf{G_s}$] Case $\mathsf{G_s}( \varphi_2 \vee \mathsf{G_s} \varphi_4)$: There are the following two subcases: \begin{itemize} \item[$(i)$] Case $\mathsf{G_s}(\bigvee_{\varphi' \in G} \mathsf{G_s} \varphi')$: It holds, that $\mathsf{G_s}(\bigvee_{\varphi' \in G} \mathsf{G_s} \varphi') \equiv (\mathsf{G_s} \neg tt \vee \bigvee_{\varphi' \in G}(\mathsf{X} \mathsf{G_s} \varphi'))$, therefore the set $A_\varphi$ can be constructed as $A_{\mathsf{G_s} \neg tt} \cup \bigcup_{\varphi' \in G} \lbrace \alpha(tt\,\wedge \mathsf{X} \delta, \mathcal{B}) \; | \; \alpha(\delta, \mathcal{B}) \in A_{\mathsf{G_s} \varphi'}\rbrace$. \item[$(ii)$] Case $\mathsf{G_s}( p_2 \vee \bigvee_{\varphi' \in G} \mathsf{G_s} \varphi')$: Since $\mathsf{G_s}(p_2 \vee \bigvee_{\varphi' \in G} \mathsf{G_s} \varphi') \equiv (\mathsf{G_s} p_2) \vee \bigvee_{\varphi' \in G}(\mathsf{X}(p_2 \mathsf{U} \mathsf{G_s} \varphi'))$, the set $A_\varphi$ can be constructed as $A_{\mathsf{G_s} p_2} \cup \bigcup_{\varphi' \in G} \lbrace \alpha(tt \wedge \mathsf{X} p_2 \mathsf{U} \delta, \mathcal{B} \; | \; \alpha(\delta, \mathcal{B}) \in A_{\mathsf{G_s} \varphi'})\rbrace$. \end{itemize} \end{itemize} \item[$\circ \mathsf{G_s}$] Case $\mathsf{G_s} \mathsf{G_s} \varphi_2$: Because $\mathsf{G_s}(\mathsf{G_s} \varphi_2) \equiv (\mathsf{G_s} \neg tt) \vee (\mathsf{X} \mathsf{G_s} \varphi_2)$, the set $A_\varphi$ can be constructed as $A_{\mathsf{G_s} \neg tt} \cup \lbrace \alpha(tt \wedge \mathsf{X} \delta, \mathcal{B}) \; | \; \alpha(\delta, \mathcal{B}) \in A_{\mathsf{G_s} \varphi_2}\rbrace$. \end{itemize} \end{itemize} %\end{itemize} \chapter{Translation of $\alpha$-formulae into B\"{u}chi automata} As said before, each $\alpha$-formula can be easily converted into an B\"{u}chi automaton. In this chapter we present two different algorithms, each with its respective advantages. These algorithms differ only in the way how to translate the part of the $\alpha$-formula corresponding to the set $\mathcal{B}$ into an B\"{u}chi automaton, there are no differences in the translation of the $\delta$ parts. Now, let us present an algorithm for converting the $\alpha$-formula into a B\"{u}chi automaton. Let $\alpha(\delta, \mathcal{B})$, where $\delta = \theta_1 O_1 \theta_2 O_2 \cdots \theta_n O_n \theta_{n+1}$, be the input formula. Every node of the B\"{u}chi automaton is represented as natural number. The algorithm works as follows. First, the set $\mathcal{B}$ is processed (it will be described later). Let $i$ denotes the last node added to the part of the B\"{u}chi automaton which represents the set $\mathcal{B}$. This node is set as accepting and it is the only accepting node. From the node 0, the first added node, we begin constructing the part of the automaton corresponding to the $\delta$-part. This part is constructed from the end of the $\delta$-part, from the operator $O_n$ down to operator $O_1$. The last node, the one added after operator $O_1$ is processed, is set as initial. Let $A$ denotes the B\"{u}chi automaton created by this algorithm. Then $A = (Q, \Sigma, \delta, q_o, \{q_f\})$ where $Q$ is a set of states (natural numbers) and $\Sigma = 2^{{AP}^*}$. The pseudocode of this algorithm is given in Algorithm 1. In the algorithm, $\beta, \gamma \in 2^{AP^{*}}$. \begin{algorithm} \caption{Translation of $\alpha$-formulae into a B\"{u}chi automaton} \textbf{Input:} $\alpha(\delta, \mathcal{B})$, where $\delta = \theta_1 O_1 \theta_2 \cdots \theta_n O_n \theta_{n+1}$ \\ \textbf{Output:} $A = (Q, \Sigma, \Delta, q_o, \{q_f\})$ \begin{algorithmic}[1] \baselineskip=12pt{ \STATE translate the set $\mathcal{B}$ \STATE $j=0$ \FOR{ $ k = n, k \geq 1, k-- $} \IF{$O_k = \wedge \mathsf{X}$} \STATE{$A.add\_node(j+1)$} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} j)$} \COMMENT{for all $\beta$ satisfying $\theta_k$} \STATE $j++$ \ENDIF \IF{$O_k = \mathsf{U}_+$} %\STATE{$\mathbf{expand\_\mathsf{U}}$} \STATE{$A.add\_node(j+1)$} \FORALL{$l$ such that $j \stackrel{\beta}{\longrightarrow} l \in \Delta$} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} l)$} \ENDFOR \IF{$j\stackrel{\gamma}{\longrightarrow} j \notin \Delta$} \STATE{$A.remove\_node(j)$} \ENDIF \COMMENT{node is removed with all its transitions} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} j)$} \COMMENT{for all $\beta$ satisfying $\theta_k$} \STATE $j++$ \STATE{$A.add\_node(j+1)$} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} j+1)$} \COMMENT{for all $\beta$ satisfying $\theta_k$} \STATE$j++$ \ENDIF \IF{$O_k = \mathsf{U}$} \STATE{$A.add\_node(j+1)$} \FORALL{$l$ such that $j \stackrel{\beta}{\longrightarrow} l \in \Delta$} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} l)$} \ENDFOR \IF{$j\stackrel{\gamma}{\longrightarrow} j \notin \Delta$} \STATE{$A.remove\_node(j)$} \ENDIF \COMMENT{node is removed with all its transitions} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} j+1)$} \COMMENT{for all $\beta$ satisfying $\theta_k$} \STATE $j++$ \ENDIF \IF{$O_k = \mathsf{G_s}$} \STATE{$A.add\_node(j+1)$} \STATE{$A.add\_trans((j+1) \stackrel{\beta}{\longrightarrow} 0)$} \COMMENT{for all $\beta$ satisfying $\theta_k$} \STATE $j++$ \ENDIF \ENDFOR \STATE {$A.set\_initial(j)$} } \end{algorithmic} \end{algorithm} \section{Memory optimized translation of the set $\mathcal{B}$} In this algorithm, we try to minimize the amount of memory used to store the B\"{u}chi automaton. The state formulae of the set $\mathcal{B}$ were ordered in some way and these state formulae were expected in this order, e.g. let $\mathcal{B} = \{ a_0, a_1, \cdots a_n \}$. The pseudocode of this procedure is shown in Algorithm 2. The input formula is again $\alpha(\delta, \mathcal{B})$ where $\delta = \theta_1 O_1 \theta_2 \cdots \theta_n O_n \theta_{n+1}$. \begin{algorithm} \caption{Memory optimized translation of the $\mathcal{B}$ set} \begin{algorithmic}[1] \STATE{$A.add\_node(0)$} \FOR{$i = 0, i < |\mathcal{B}|, i++$} \STATE{$A.add\_node(i+1)$} \STATE{$A.add\_trans(i \stackrel{\beta}{\longrightarrow} (i+1))$} \COMMENT{for all $\beta$ satisfies $a_i \wedge \theta_{n+1}$} \STATE{$A.add\_trans(i \stackrel{\gamma}{\longrightarrow} i)$} \COMMENT{$\gamma$ satisfies $\neg a_i \wedge \theta_{n+1}$} \ENDFOR \STATE{$A.add\_trans(i \stackrel{\beta}{\longrightarrow} 0)$} \COMMENT{$\beta$ satisfies $\theta_{n+1}$} \STATE{set $i$ as accepting} \end{algorithmic} \end{algorithm} % Figures 6.1 and 6.2 shows how the parts with expanded $\mathsf{X}$ and $\mathsf{U}_+$ of the resulting automaton will look like. % % The following figure shows, how to deal with the operator \mathsf{X} in the $\delta$-part. % \begin{figure} % \begin{center} % \includegraphics[height=3cm]{next} % \caption[Figure 6.1]{The part of the resulting automaton with expanded $\mathsf{X}$ operator.} % \end{center} % \end{figure} % \begin{figure} % \begin{center} % \includegraphics[height=3cm]{until_plus} % \caption[Figure 6.2]{The part of the resulting automaton with expanded $\mathsf{U}_+$ operator.} % \end{center} % \end{figure} % % % % \section{Memory optimized translation} % In this algorithm, we tried to minimize the amount of memory used to store the B\"{u}chi automaton. % The atomic propositions of the set $\mathcal{B}$ were ordered in some way and these atomic propositions were expected in this order, e.g. let $\mathcal{B} = \{ a_0, a_1, \cdots a_n \}$. % The pseudocode of this procedure is shown in algorithm 5. % % % Let us now show an example of the resulting automaton. % % Let $\alpha = tt \wedge\; \mathsf{X} \;tt \;\mathsf{U}_+ \;\neg c \;\wedge \mathsf{X} \;\neg c\; \mathsf{U} \;(\neg c \wedge b) \;\wedge \mathsf{X} \;\neg c \;\mathsf{U}_+ \;(\neg c \wedge a)\; \wedge \mathsf{G_s} \;\neg c \wedge \mathsf{G_s}\mathsf{F_s} b \;\wedge \mathsf{G_s}\mathsf{F_s} a$ be the input formula. Figure 6.3. shows the resulting automaton. % % % % \begin{figure} % % \begin{center} % % \includegraphics[height = 17 cm]{ukazka-preklad1} % % \caption[Figure 6.3.]{Example of translation of $\alpha$-formula using algorithm 5.} % % \end{center} % % \end{figure} % \section{Alternative translation of the set $\mathcal{B}$} In this section we present alternative translation of the part of the $\alpha$-formula corresponding to the set $\mathcal{B}$. The previous algorithm suffers a drawback -- the state formulae in the accepting cycle have to occur in the given order. This algorithm enables more than one atomic proposition to be satisfied in one transition. Pseudocode is given in the Algorithm 3. % % \begin{algorithm} \caption{Alternative translation of the set $\mathcal{B}$} \begin{algorithmic}[1] \STATE{$A.add\_node(0)$} \FOR{$i = 0, i < |\mathcal{B}|, i++$} \STATE{$A.add\_node(i+1)$} \STATE{$A.add\_trans(i \stackrel{\beta}{\longrightarrow} (i+1))$} \COMMENT{$\beta$ satisfies $a_i \wedge \theta_{n+1}$} \STATE{$A.add\_trans(i \stackrel{\gamma}{\longrightarrow} i)$} \COMMENT{$\gamma$ satisfies $\neg a_i \wedge \theta_{n+1}$} \ENDFOR \STATE{set $i$ as accepting} \FORALL{$j<|\mathcal{B}|, j < k \leq |\mathcal{B}|$} \STATE{$A.add\_trans(j \stackrel{\beta}{\longrightarrow} k)$} \COMMENT{$\beta$ satisfies $a_{j+1} \wedge a_{j+2} \cdots \wedge a_{k} \wedge \theta_{n+1}$} \ENDFOR \STATE{$A.add\_trans(n \stackrel{\gamma}{\longrightarrow} 0)$} \COMMENT{$\gamma$ satisfies $\neg a_1 \wedge \theta_{n+1}$} \FORALL{$1 \leq j \leq n$} \STATE{$A.add\_trans(n \stackrel{\delta}{\longrightarrow} j)$} \COMMENT{$\delta$ satisfies $a_1 \wedge a_2 \cdots \wedge a_j \wedge \theta_{n+1}$} \ENDFOR \end{algorithmic} \end{algorithm} Let us now present the B\"{u}chi automaton for the input formula $((a) \wedge \mathsf{X} ((\neg c) \wedge \mathsf{X} ((\neg c) \mathsf{U} (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s F_s} a \wedge \mathsf{G_s F_s} b$. Picture 5.1 shows the B\"uchi automata obtained using our translations, picture 5.2 show B\"uchi automaton for the same formula using the translation from \cite{fast-ltl} implemented by Milan Jaro\v{s}, which is included in DiVinE, \cite{ANNA}. As can be clearly seen from the pictures, our translations results in automaton with less states and less transitions than the translation using within DiVinE. \begin{figure}[h] \centering \subfloat[Algorithm 2]{\label{fig:preklad1}\includegraphics[height=11cm]{ukazka-preklad1} } \subfloat[Algorithm 3]{\label{fig:preklad2}\includegraphics[height=11cm]{ukazka-preklad2} } \caption{Translation of $((a) \wedge \mathsf{X} ((!c) \wedge \mathsf{X} ((!c) \mathsf{U} (((!c \wedge b)) \wedge \mathsf{G_s} (!c))))) \wedge \mathsf{G_s F_s} a \wedge \mathsf{G_s F_s} b$ into B\"{u}chi automaton. In the picture, $\&\&$ stands for $\wedge$, $!$ stands for $\neg$. (a) has the set $\mathcal{B}$ translated with Algorithm 2, (b) with Algorithm 3.} \label{flow_vectors} \end{figure} \begin{figure} \begin{center} \includegraphics[height=12cm]{ukazka-preklad-mj} \end{center} \caption[Figure 6.2.]{The B\"uchi automaton for the formula $((a) \wedge \mathsf{X} ((!c) \wedge \mathsf{X} ((!c) \mathsf{U} (((!c \wedge b)) \wedge \mathsf{G_s} (!c))))) \wedge \mathsf{G_s F_s} a \wedge \mathsf{G_s F_s} b$ using translation implemented in DiVinE.} \end{figure} \chapter{Implementation} In this chapter we describe the way how the $\alpha$-formulae are represented in the memory and briefly describe some methods used for the translation of formulae from the fragment LTL($\mathsf{F,G}$) into the disjunction of $\alpha$-formulae. All here mentioned methods were implemented in C++ using compiler g++ version 4.2.3 (from debian package). In this implementation we use the structures and classes implemented by Milan Jaro\v{s}, namely the classes \texttt{LTL\_formul\_t} and \texttt{BA\_graph\_t} and its subclasses. For building this all programs, one has to link the source codes to the files, in which the above mentioned classes, \texttt{LTL\_formul\_t} and \texttt{BA\_graph\_t}, are implemented. These source codes are part of DiVinE, \cite{ANNA}. \section{Data representation} $\alpha$-formulae are stored in the structure \texttt{alpha\_formul\_t}. This structure consists of vector of \texttt{alpha\_fragment\_t} called \texttt{fragments} (will be explained later), of \texttt{PROP\_formul\_t} \texttt{final} which represents the $\theta_{n+1}$ and the set $\mathcal{B}$. Every $\theta_i$ is represented by \texttt{PROP\_formul\_t}, which is actually class \texttt{LTL\_formul\_t}, implemented by Milan Jaro\v{s} (see \cite{milan}). Our implementation of $\alpha$-formulae guarantees that nothing but boolean combination of atomic propositions is stored in each $\theta_i$. \texttt{fragments} is a vector (the stl library implements vector as red-black tree) of \texttt{alpha\_fragment\_t}. The structure \texttt{alpha\_fragment\_t} consists of pairs of $\theta_i$ and the corresponding operator $O_i$. Stored in a special enumeration data type, operator can take on values from the following set $\{ \mathsf{U}, \mathsf{U}_+, \wedge \mathsf{X}, \wedge \mathsf{G_s} \}$ only. The set $\mathcal{B}$ is stored as a vector (for easy access) of \texttt{PROP\_formul\_t}. \section{Methods} There are several methods in the source file \texttt{alpha.cc}, the most important method in the whole program is \texttt{decompose\_alpha}. It takes as a parameter the input LTL formula in the \texttt{LTL\_formul\_t} structure. Because of verification, the input formula is negated before the actual translation since we want every $\alpha$-formula in the disjunction to be verified independently. Output is the list of \texttt{alpha\_formul\_t}, the disjunction of these formulae is then equivalent to the negation of the input formula. The method \texttt{conjunction} computes the conjunction of the $\alpha$-formulae. It takes as an input parameters two lists of $\alpha$-formulae and as a result it returns a list of $\alpha$-formulae. The method \texttt{conjunction} works as follows: let $\alpha_1, \alpha_2, \cdots \alpha_i, \beta_1, \beta_2,\cdots \beta_j$ are $\alpha$-formulae. We want to compute $(\alpha_1 \vee \alpha_2 \vee \cdots \vee \alpha_i) \wedge (\beta_1 \vee \beta_2 \vee \cdots \vee \beta_j)$. Function \texttt{conjunction} converts this conjunction into $(\alpha_1 \wedge \beta_1) \vee (\alpha_1 \wedge \beta_2) \cdots \vee (\alpha_1 \wedge \beta_j) \vee (\alpha_2 \wedge \beta_1) \vee \cdots \vee (\alpha_i \wedge \beta_j)$ and for every part of this disjunction it calls function \texttt{conjunction\_1}, which actually computes the conjunction of two given $\alpha$-formulae. The results of the callings of the function \texttt{conjunction\_1} are then gathered by function \texttt{conjunction} and are returned. The disjunction of these formulae in the output list is equivalent to the conjunction of the two input lists of $\alpha$-formulae. The translation of an $\alpha$-formula into a B\"uchi automaton is implemented in the source file \texttt{alpha\_to\_ba.cc}. Function \texttt{alpha\_to\_ba\_1} implements the Algorithms 1 and 2 (Chapter 5), function \texttt{alpha\_to\_ba\_2} implements Algorithms 1 and 3. \chapter{Experimental Results} In this chapter we present experimental data obtained from experiments ran on ParaDiSe laboratory cluster. All experiments were ran on cluster consisting of \textit{psyche} machines, their hardware characteristic is presented in the table 7.1. \begin{table} \begin{center} % use packages: array \begin{tabular}{|lr|} \hline number of CPUs & 1 \\ CPU name & Intel(R) Pentium(R) 4 CPU 2.60GHz (HyperThreading) \\ total memory & 4 GB \\ \hline \end{tabular} \caption[Table 7.1]{Hardware characterictic of cluster node} \end{center} \end{table} \section{Researched formulae} Here we list the examined formulae. There were three main sources of the formulae: \cite{BEEM} and \cite{pat-clanek}, \cite{PAT-S}. For the first one, we had the models associated with the formulae, therefore we were able to run verification of these formulae with their respective models. For the latter two, we had no models, hence we present here only the list of $\alpha$-formulae which disjunction is equivalent to the negation of the given formula. Now, let us present these formulae. In the following, the first one is the original formula, the numbered formulae associated with this formula are the $\alpha$-formulae which disjunction is equivalent to the negation of the first formula. After keyword "beem" is the number of formulae found in \cite{BEEM}, after keyword "patterns" is the number of formulae according to \cite{pat-clanek}. For the formula $\mathsf{G} a$ and $\mathsf{G} \neg a$ we wrote there is no these formulae in BEEM, however this is not particulary true. These formulae are listed in BEEM under the term "reachability", so literally there are no formulae $\mathsf{G} a$, $\mathsf{G} \neg a$ in BEEM. \begin{itemize} \item $\mathsf{G}(a\; \rightarrow \;\mathsf{F}\; b) $ \\ beem: 14\\ patterns: 241 \begin{enumerate} \item $true\; \mathsf{U} \; ((a \wedge \neg b) \wedge\; \mathsf{G_s}\; \neg b)$ \end{enumerate} \item $\mathsf{G} \; a$\\ beem: 0\\ patterns: 110 \begin{enumerate} \item $true\; \mathsf{U} (\neg a \;\wedge \;\mathsf{G_s} \;true)$ \end{enumerate} \item $\mathsf{G} \neg a$\\ beem: 0\\ patterns: 41 \begin{enumerate} \item $true \;\mathsf{U}(a \;\wedge \;\mathsf{G_s} \;true)$ \end{enumerate} \item $\mathsf{G\;F}\;a$\\ beem: 13\\ patterns: 12 \begin{enumerate} \item $true \;\mathsf{U}(\neg a \;\wedge \;\mathsf{G_s} \;\neg a)$ \end{enumerate} \item $\mathsf{G} \;(a \rightarrow G \; b) $\\ beem: 0\\ patterns: 5 \begin{enumerate} \item $true\; \mathsf{U}((a \wedge \neg b) \;\wedge \;\mathsf{G_s} \;true)$ \item $true\; \mathsf{U} (a \wedge \mathsf{X} (\;true \;\mathsf{U} \;(\neg b \;\wedge\; \mathsf{G_s} \;true)))$ \end{enumerate} \item $(\mathsf{G}\; \neg a) \vee \mathsf{F}\;(a \wedge \mathsf{F}\; b)$\\ beem: 0\\ patterns: 4 \begin{enumerate} \item $(a \wedge \neg b) \wedge \mathsf{X} (\neg b \wedge \mathsf{G_s} \; \neg b)$ \item $(a \wedge \neg b) \wedge \mathsf{X} ((\neg a \wedge \neg b) \wedge \mathsf{X}((\neg a \wedge \neg b) \mathsf{U}\;(\neg b \wedge \mathsf{G_s} \; \neg b )))$ \end{enumerate} \item $\mathsf{G}(a \rightarrow \mathsf{G}\;(b \rightarrow \mathsf{F} \; c))$\\ beem: 0\\ patterns: 3 \begin{enumerate} \item $true \;\mathsf{U} ((a \wedge b \wedge !c) \wedge \mathsf{G_s} \neg c)$ \item $true\; \mathsf{U} (a \wedge \mathsf{X}( true\; \mathsf{U}\; ((b \wedge \neg c) \wedge \mathsf{G_s} \; \neg c)))$ \end{enumerate} \item $\mathsf{F} a$\\ beem: 3\\ patterns: 0 \begin{enumerate} \item $\neg a \wedge \mathsf{G_s} \neg a$ \end{enumerate} \item $\mathsf{G} \; \mathsf{F} \; ( a \vee b ) \wedge \mathsf{G} \; \mathsf{F} \; (c \vee b) $\\ beem: 1\\ patterns: 0 \begin{enumerate} \item $true \; \mathsf{U}\; ((\neg a \wedge \neg b) \; \wedge \mathsf{G_s} \; (\neg a \wedge \neg b))$ \item $true \; \mathsf{U}\; ((\neg c \wedge \neg b) \; \wedge \mathsf{G_s} \; (\neg c \wedge \neg b))$ \end{enumerate} \item $(\mathsf{G} \; \mathsf{F} \; a \wedge \mathsf{G} \; \mathsf{F} \; b) \rightarrow \mathsf{G} \; \mathsf{F} \; c$ \\ beem: 1\\ patterns: 0 \\ The list of the $\alpha$-formulae is too long (there are 74 formulae), therefore, the list of these formulae can be found in Appendix A. \end{itemize} \section{Experimental data} Here we present data from experiments on cluster in the ParaDiSe laboratory. As was said before, we had models to only subset of the examined formulae, only to those in \cite{BEEM}. The formulae and their respective models are given in the table 7.2. For all the following verifications, we used the OWCTY algorithm. All the data presented here are obtained from the output of this algorithm, we present here total memory and time consumption. \begin{table} \begin{center} % use packages: array \begin{tabular}{l|l} formula & model \\ \hline $\mathsf{G}(a\; \rightarrow \;\mathsf{F}\; b) $ & at \\ $\mathsf{G\;F}\;a$ & iprotocol \\ $\mathsf{G \; F} \; ( a \vee b ) \wedge \mathsf{G \; F} \; (c \vee b) $ & plc \\ $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F} \; b) \rightarrow \mathsf{G \; F }\; c$ & iprotocol\\ \end{tabular} \caption[Table 7.2]{The formulae from \cite{BEEM} and their respective models} \end{center} \end{table} The data itself are shown in the following tables 7.3. - 7.6. The complete experimental data can be found on the enclosed CD. % The number in the leftmost cell in the first row indicates the number of machines. If there were more than one, than the total memory and time consumption is given. \subsection{$\mathsf{GF} a$, $\mathsf{G} (a \rightarrow \mathsf{F} b)$} First, let us present data for the formula $\mathsf{GF} a$. The amount of memory and time are in all cases the same, because the automaton for the original formula and the automaton for the $\alpha$-formula are the same. From the same reason, the amount of consumed memory and time is the same in case of the formula $\mathsf{G} (a \rightarrow \mathsf{F} b)$. \subsection{$\mathsf{G \; F} \; ( a \vee b ) \wedge \mathsf{G \; F} \; (c \vee b) $} More interesting results come from the verification of the formula $\mathsf{G \; F} \; ( a \vee b ) \wedge \mathsf{G \; F} \; (c \vee b) $. The automaton for negation of the original formula (see figure 7.1) was bigger than automata for the $\alpha$-formula, see figures 7.2. and 7.3. Therefore we succeeded in finding the accepting cycle in less memory and less time when verifying the $\alpha$-formulae compared to the verification of the original formula (see table 7.3.), however we used two workstations to achieve this result. \begin{figure} \begin{center} \includegraphics[height=4cm]{plc-orig} \caption[Figure 7.1.]{The B\"uchi automaton for the negation of formula $\mathsf{G \; F} \; ( a \vee b ) \wedge \mathsf{G \; F} \; (c \vee b) $} \end{center} \end{figure} \begin{figure} \begin{center} \includegraphics[height=4cm]{plc-alpha1} \caption[Figure 7.2.]{The B\"uchi automaton for $\alpha_1$} \end{center} \end{figure} \begin{figure} \begin{center} \includegraphics[height=4cm]{plc-alpha2} \caption[Figure 7.3.]{The B\"uchi automaton for $\alpha_2$} \end{center} \end{figure} \begin{table} \begin{center} % use packages: array %plc \begin{tabular}{c|c|c| c} 1 & memory (MB) & time (s) & acc.cycle?\\ \hline orig. & 1138 & 639 & Y \\ $\alpha_1$ & 1023 & 463 & Y \\ $\alpha_2$ & 952 & 349 & Y \end{tabular} \caption[Table 7.3.]{$\mathsf{G \; F} \; ( a \vee b ) \wedge \mathsf{G \; F} \; (c \vee b) $ } \end{center} \end{table} \subsection{$(\mathsf{G \; F} \; a \wedge \mathsf{G \; F} \; b) \rightarrow \mathsf{G \; F }\; c$} The last formula is the most interesting one. As was written before, there are 74 formulae in the disjunction equivalent to the negation of this one, which gives us the possibility to a massive parallelism. The tables with the experimental results are too large to be presented here, hence we present here only a snippets -- only the $\alpha$-formulae from the disjunction with an accepting cycle. These $\alpha$-formulae are quite complicated, that's why their B\"{u}chi automata are much bigger than the automaton for the negation of the original formula. The much higher memory consumption can be seen in table 7.4, please note that this time the algorithm \cite{fast-ltl} for LTL to B\"uchi automata translation was used (implemented by Milan Jaro\v{s}, see \cite{milan}). Complete list of the experimental data can be found in appendix B. No verification of an $\alpha$-formula is completed within less memory or within less amount of time. \begin{table} \begin{center} \begin{tabular}{c|c|c| c} 1 & memory (MB) & time (s) & acc.cycle?\\ \hline orig. & 921 & 649 & Y \\ $\alpha_{55}$ & 978 & 677 & Y \\ $\alpha_{56}$ & 1013 & 706 & Y \\ $\alpha_{57}$ & 1443 & 970 & Y \\ $\alpha_{58}$ & 2721 & 1516 & Y \\ $\alpha_{59}$ & 1594 & 1029 & Y \\ $\alpha_{60}$ & 1254 & 838 & Y \\ $\alpha_{69}$ & 1127 & 907 & Y \\ $\alpha_{70}$ & 1109 & 915 & Y \\ $\alpha_{71}$ & 2940 & 1651 & Y \\ $\alpha_{72}$ & 3563 & 1786 & Y \\ $\alpha_{73}$ & 4187 & 2127 & Y \\ $\alpha_{74}$ & 1334 & 1067 & Y \\ \end{tabular} \caption[Table 7.4.]{Selected $\alpha$-formulae for the $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F} \; b) \rightarrow \mathsf{G \; F }\; c$ formula} \end{center} \end{table} Because of the size of B\"uchi automata for the $\alpha$-formulae, we used the Algorithms 1, 2 and 3 presented in Chapter 5 to translate the $\alpha$-formulae into B\"{u}chi automata, which significantly reduces the memory usage as shown (again -- snippets only, for complete table see Appendix B) in table 7.5, resp. table 7.6. As it can be seen in the mentioned tables, we succeeded in reducing the amount of memory needed for verification of the $\alpha$-formulae. In the best case, the original sytem used 4187 MB of memory, with our translation we used only 1560 MB ($\alpha$-formula $\alpha_{73}$). We even managed to verify some of the $\alpha$-formulae in less memory ($\alpha$-formula $\alpha_{69}$, 719 MB and $\alpha$-formula $\alpha_{70}$, 721 MB; Algorithm 2, Chapter 5) than the original formula (921 MB). As it can be also seen from the mentioned tables, the use of Algorithm 3 always yields in slightly bigger memory consumption, it is because the storing the additional transitions in the part of the automaton corresponging to the set $\mathcal{B}$ compared to the amount of memory consumed when Algorithm 2 is used. \begin{table} \begin{center} \begin{tabular}{c|c|c| c} 1 & memory (MB) & time (s) & acc.cycle?\\ \hline orig. & 921 & 649 & Y \\ $\alpha_{55}$ & 1101 & 769 & Y \\ $\alpha_{56}$ & 1060 & 798 & Y \\ $\alpha_{57}$ & 1343 & 964 & Y \\ $\alpha_{58}$ & 1897 & 1304 & Y \\ $\alpha_{59}$ & 1623 & 1124 & Y \\ $\alpha_{60}$ & 1318 & 929 & Y \\ $\alpha_{69}$ & 719 & 649 & Y \\ $\alpha_{70}$ & 721 & 657 & Y \\ $\alpha_{71}$ & 1245 & 908 & Y \\ $\alpha_{72}$ & 1828 & 1267 & Y \\ $\alpha_{73}$ & 1560 & 1069 & Y \\ $\alpha_{74}$ & 952 & 811 & Y \\ \end{tabular} \caption[Table 7.5.]{Selected $\alpha$-formulae for the $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F} \; b) \rightarrow \mathsf{G \; F }\; c$ formula translated by Algorithms 1 and 2 from Chapter 5.} \end{center} \end{table} \begin{table} \begin{center} \begin{tabular}{c|c|c| c} 1 & memory (MB) & time (s) & acc.cycle?\\ \hline orig. & 921 & 649 & Y \\ $\alpha_{55}$ & 1550 & 786 & Y \\ $\alpha_{56}$ & 1643 & 815 & Y \\ $\alpha_{57}$ & 1910 & 982 & Y \\ $\alpha_{58}$ & 2609 & 1304 & Y \\ $\alpha_{59}$ & 2382 & 1141 & Y \\ $\alpha_{60}$ & 1877 & 946 & Y \\ $\alpha_{69}$ & 796 & 676 & Y \\ $\alpha_{70}$ & 801 & 684 & Y \\ $\alpha_{71}$ & 1737 & 909 & Y \\ $\alpha_{72}$ & 2549 & 1267 & Y \\ $\alpha_{73}$ & 2152 & 1069 & Y \\ $\alpha_{74}$ & 1028 & 838 & Y \\ \end{tabular} \caption[Table 7.6.]{Selected $\alpha$-formulae for the $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F} \; b) \rightarrow \mathsf{G \; F }\; c$ formula translated by Algorithms 1 and 3 from Chapter 5.} \end{center} \end{table} \chapter{Conclusion} After describing the fragment $\mathcal{A}$ and the translation of formulae from LTL($\mathsf{F,G}$) into the finite disjunction of $\alpha$-formulae, all the objectives set for this thesis have been met. The technical information on the translation of formulae from LTL($\mathsf{F,G}$) into a finite disjunction of $\alpha$-formulae is described in Chapter 6. The translation of a conjunction of $\alpha$-formulae into the equivalent disjunction was described in Chapter 3, implementation details are again in Chapter 6. The algorithms for translation the $\alpha$-formula into a B\"uchi automaton were presented in Chapter 5. As the experimental data shows, the verification of $\alpha$-formulae can be for some $\alpha$-formulae memory more effective, than the verification of the original specification formula -- e.g. we can find one or more $\alpha$-formulae whose verification uses less amount of memory than the verification of the original formula. However, we cannot say in advance which of the part of the disjunction, which $\alpha$-formula, is the one whose verification will save us memory compared to the verification of the original formula. Therefore we have to run the verification of each of the $\alpha$-formulae from the disjunction either one after another on one machine until we find one with the accepting cycle (but this will not with high probability save us time) or we have to run the verification of the $\alpha$-formulae in parallel. But the latter possibility has high requirements available on computational power. There is also a problem, that the verification of some $\alpha$-formulae uses more memory and time than the verification of the original system. It was also a problem to find reasonable formulae from the fragment LTL($\mathsf{F,G}$) which do not have an accepting cycle in the model of the system. Therefore we were unable to evaluate the benefit of verifying $\alpha$-formulae in case there is no accepting cycle for the original formula. \bibliographystyle{plain} \bibliography{diplomka.bib} \appendix \chapter{$\alpha$-formulae for $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F }\; b) \rightarrow \mathsf{G \; F} \; c$} \begin{enumerate} \item $(a \wedge b \wedge \neg c) \; \wedge \mathsf{G_s} \; \neg c \; \wedge \mathsf{G_s} \; \;\mathsf{F_s} b \; \wedge \mathsf{G_s} \;\mathsf{F_s} a$ \item $(((a \wedge b)) \; \wedge \mathsf{X} \; ((true) \; \mathsf{U}\; ((\neg c) \wedge \; \mathsf{G_s} (\neg c))))\; \wedge \mathsf{G_s} \; \mathsf{F_s} b \; \wedge \mathsf{G_s}\; \mathsf{F_s} a$ \item $(((\neg c \wedge a)) \; \wedge \mathsf{X} \; (((\neg c \wedge b)) \; \wedge \mathsf{G_s}\; (\neg c))) \wedge \mathsf{G_s} \; \mathsf{F_s} a \wedge \mathsf{G_s} \; \mathsf{F_s} b$ \item $((a) \wedge \mathsf{X} \; (((b \wedge \neg c)) \; \wedge \mathsf{G_s} \; (\neg c))) \wedge \mathsf{G_s} \; \mathsf{F_s} a \wedge \mathsf{G_s} \; \mathsf{F_s} b$ \item $ ((a) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} a \wedge \mathsf{G_s} \; \mathsf{F_s} b$ \item $(((\neg c \wedge a)) \; \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+\; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} a \wedge \mathsf{G_s} \; \mathsf{F_s} b$ \item $((a) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} a \wedge \mathsf{G_s}\; \mathsf{F_s} b$ \item $((a) \wedge \mathsf{X} \; ((true)\; \; \mathsf{U}_+ \; (((b \wedge \neg c)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s} a \wedge \mathsf{G_s}\; \mathsf{F_s} b$ \item $((a) \wedge \mathsf{X}\; ((true)\; \; \mathsf{U}_+\; ((b) \wedge \mathsf{X} \; ((true)\; \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} \; (\neg c)))))) \wedge \mathsf{G_s}\; \mathsf{F_s} a \wedge \mathsf{G_s}\; \mathsf{F_s} b$ \item $((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s}\; (\neg c)))))) \wedge \mathsf{G_s}\; \mathsf{F_s} a \wedge \mathsf{G_s}\; \mathsf{F_s} b$ \item $(((\neg c \wedge b)) \wedge \mathsf{X}\; (((\neg c \wedge a)) \wedge \mathsf{G_s}\; (\neg c))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((b) \wedge \mathsf{X} \; (((a \wedge \neg c)) \wedge \mathsf{G_s}\; (\neg c))) \wedge \mathsf{G_s}\; \mathsf{F_s} b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((b) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; (((\neg c \wedge (a \wedge b))) \; \wedge \mathsf{G_s} \; (\neg c))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((((a \wedge b) \wedge \neg c)) \wedge \mathsf{G_s} \; (\neg c))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s}\; a$ \item $((true) \wedge \mathsf{X} \; (((a \wedge b)) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s}\; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X}\; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s}\; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; (((b \wedge \neg c)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s}\; b \wedge \mathsf{G_s}\; \mathsf{F_s}\; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} \; (\neg c)))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+\; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s}\; a$ \item $((true) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} \; (\neg c)))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((b \wedge \neg c)) \wedge \mathsf{G_s}\; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s}\; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+\; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s}\; (\neg c))))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s}\; (\neg c))))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $(((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s}\; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s}\; b \wedge \mathsf{G_s}\; \mathsf{F_s}\; a$ \item $((b) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} \; (\neg c))))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((a \wedge \neg c)) \wedge \mathsf{G_s} \; (\neg c)))) \wedge \mathsf{G_s}\; \mathsf{F_s} \; b \wedge \mathsf{G_s}\; \mathsf{F_s} \; a$ \item $((b) \wedge \mathsf{X} ((true) \; \mathsf{U}_+ ((a) \wedge \mathsf{X} ((true) \; \mathsf{U} ((\neg c) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s}\mathsf{F_s} b \wedge \mathsf{G_s}\mathsf{F_s} a$ \item $((b) \wedge \mathsf{X} ((true) \; \mathsf{U}_+ ((\neg c) \wedge \mathsf{X} ((\neg c) \; \mathsf{U} (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; (((a \wedge \neg c)) \wedge \mathsf{G_s} (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((\neg c) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((a \wedge \neg c)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((true) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; a \wedge \mathsf{G_s} \; \mathsf{F_s} \; b$ \item $((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge (a \wedge b))) \wedge \mathsf{G_s} (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge (a \wedge b))) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((((a \wedge b) \wedge \neg c)) \wedge \mathsf{G_s} (\neg c)))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((a \wedge b)) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge (a \wedge b))) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; (((b \wedge \neg c)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((b \wedge \neg c)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; (((a \wedge \neg c)) \wedge \mathsf{G_s} (\neg c))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; (((a \wedge \neg c)) \wedge \mathsf{G_s} (\neg c)))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((a) \wedge \mathsf{X} \; ((true) \; \mathsf{U} \; ((\neg c) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((b) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \item $((true) \wedge \mathsf{X} \; ((true) \; \mathsf{U}_+ \; ((\neg c) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U} \; (((\neg c \wedge b)) \wedge \mathsf{X} \; ((\neg c) \; \mathsf{U}_+ \; (((\neg c \wedge a)) \wedge \mathsf{G_s} (\neg c)))))))) \wedge \mathsf{G_s} \; \mathsf{F_s} \; b \wedge \mathsf{G_s} \; \mathsf{F_s} \; a$ \end{enumerate} \chapter{Complete experimental data for $(\mathsf{G \; F} \; a \wedge \mathsf{G \; F }\; b) \rightarrow \mathsf{G \; F} \; c$} \begin{center} LTL to B\"uchi automata translation from \cite{fast-ltl} \\ \begin{xtabular}{c|c|c|c} & time & mem & acc. cycle? \\ \hline orig. & 921 & 649 & Y \\ $\alpha_{1}$ & 0 & 39 & N \\ $\alpha_{10}$ & 0 & 39 & N \\ $\alpha_{11}$ & 0 & 39 & N \\ $\alpha_{12}$ & 0 & 39 & N \\ $\alpha_{13}$ & 0 & 39 & N \\ $\alpha_{14}$ & 0 & 39 & N \\ $\alpha_{15}$ & 0 & 39 & N \\ $\alpha_{16}$ & 0 & 39 & N \\ $\alpha_{17}$ & 0 & 39 & N \\ $\alpha_{18}$ & 0 & 39 & N \\ $\alpha_{19}$ & 0 & 39 & N \\ $\alpha_{2}$ & 0 & 39 & N \\ $\alpha_{20}$ & 0 & 39 & N \\ $\alpha_{21}$ & 0 & 39 & N \\ $\alpha_{22}$ & 0 & 39 & N \\ $\alpha_{23}$ & 0 & 39 & N \\ $\alpha_{24}$ & 0 & 39 & N \\ $\alpha_{25}$ & 0 & 39 & N \\ $\alpha_{26}$ & 0 & 39 & N \\ $\alpha_{27}$ & 0 & 39 & N \\ $\alpha_{28}$ & 0 & 39 & N \\ $\alpha_{29}$ & 0 & 39 & N \\ $\alpha_{3}$ & 0 & 39 & N \\ $\alpha_{30}$ & 0 & 39 & N \\ $\alpha_{31}$ & 0 & 39 & N \\ $\alpha_{32}$ & 0 & 39 & N \\ $\alpha_{33}$ & 0 & 39 & N \\ $\alpha_{34}$ & 0 & 39 & N \\ $\alpha_{35}$ & 0 & 39 & N \\ $\alpha_{36}$ & 0 & 39 & N \\ $\alpha_{37}$ & 0 & 39 & N \\ $\alpha_{38}$ & 0 & 39 & N \\ $\alpha_{39}$ & 0 & 39 & N \\ $\alpha_{4}$ & 0 & 39 & N \\ $\alpha_{40}$ & 0 & 39 & N \\ $\alpha_{41}$ & 0 & 39 & N \\ $\alpha_{42}$ & 0 & 41 & N \\ $\alpha_{43}$ & 0 & 41 & N \\ $\alpha_{44}$ & 66 & 360 & N \\ $\alpha_{45}$ & 68 & 360 & N \\ $\alpha_{46}$ & 113 & 523 & N \\ $\alpha_{47}$ & 0 & 41 & N \\ $\alpha_{48}$ & 0 & 41 & N \\ $\alpha_{49}$ & 71 & 389 & N \\ $\alpha_{5}$ & 0 & 39 & N \\ $\alpha_{50}$ & 75 & 418 & N \\ $\alpha_{51}$ & 76 & 418 & N \\ $\alpha_{52}$ & 116 & 550 & N \\ $\alpha_{53}$ & 4 & 44 & N \\ $\alpha_{54}$ & 4 & 44 & N \\ $\alpha_{55}$ & 978 & 677 & Y \\ $\alpha_{56}$ & 1013 & 706 & Y \\ $\alpha_{57}$ & 1443 & 970 & Y \\ $\alpha_{58}$ & 2721 & 1516 & Y \\ $\alpha_{59}$ & 1594 & 1029 & Y \\ $\alpha_{6}$ & 0 & 39 & N \\ $\alpha_{60}$ & 1254 & 838 & Y \\ $\alpha_{61}$ & 0 & 41 & N \\ $\alpha_{62}$ & 0 & 41 & N \\ $\alpha_{63}$ & 68 & 368 & N \\ $\alpha_{64}$ & 70 & 377 & N \\ $\alpha_{65}$ & 70 & 377 & N \\ $\alpha_{66}$ & 112 & 530 & N \\ $\alpha_{67}$ & 8 & 49 & N \\ $\alpha_{68}$ & 8 & 49 & N \\ $\alpha_{69}$ & 1127 & 907 & Y \\ $\alpha_{7}$ & 0 & 39 & N \\ $\alpha_{70}$ & 1109 & 915 & Y \\ $\alpha_{71}$ & 2940 & 1651 & Y \\ $\alpha_{72}$ & 3563 & 1786 & Y \\ $\alpha_{73}$ & 4187 & 2127 & Y \\ $\alpha_{74}$ & 1334 & 1067 & Y \\ $\alpha_{8}$ & 0 & 39 & N \\ $\alpha_{9}$ & 0 & 39 & N \\ \end{xtabular} \end{center} \begin{center} $\alpha$-formula to B\"uchi automaton translation, Algorithm 2, Chapter 5\\ \begin{xtabular}{c|c|c|c} & time & mem & acc. cycle? \\ \hline orig. & 921 & 649 & Y \\ $\alpha_{1}$ & 0 & 39 & N \\ $\alpha_{10}$ & 0 & 39 & N \\ $\alpha_{11}$ & 0 & 39 & N \\ $\alpha_{12}$ & 0 & 39 & N \\ $\alpha_{13}$ & 0 & 39 & N \\ $\alpha_{14}$ & 0 & 39 & N \\ $\alpha_{15}$ & 0 & 39 & N \\ $\alpha_{16}$ & 0 & 39 & N \\ $\alpha_{17}$ & 0 & 39 & N \\ $\alpha_{18}$ & 0 & 39 & N \\ $\alpha_{19}$ & 0 & 39 & N \\ $\alpha_{2}$ & 0 & 39 & N \\ $\alpha_{20}$ & 0 & 39 & N \\ $\alpha_{21}$ & 0 & 39 & N \\ $\alpha_{22}$ & 0 & 39 & N \\ $\alpha_{23}$ & 0 & 39 & N \\ $\alpha_{24}$ & 0 & 39 & N \\ $\alpha_{25}$ & 0 & 39 & N \\ $\alpha_{26}$ & 0 & 39 & N \\ $\alpha_{27}$ & 0 & 39 & N \\ $\alpha_{28}$ & 0 & 39 & N \\ $\alpha_{29}$ & 0 & 39 & N \\ $\alpha_{3}$ & 0 & 39 & N \\ $\alpha_{30}$ & 0 & 39 & N \\ $\alpha_{31}$ & 0 & 39 & N \\ $\alpha_{32}$ & 0 & 39 & N \\ $\alpha_{33}$ & 0 & 39 & N \\ $\alpha_{34}$ & 0 & 39 & N \\ $\alpha_{35}$ & 0 & 39 & N \\ $\alpha_{36}$ & 0 & 39 & N \\ $\alpha_{37}$ & 0 & 39 & N \\ $\alpha_{38}$ & 0 & 39 & N \\ $\alpha_{39}$ & 0 & 39 & N \\ $\alpha_{4}$ & 0 & 39 & N \\ $\alpha_{40}$ & 0 & 39 & N \\ $\alpha_{41}$ & 0 & 39 & N \\ $\alpha_{42}$ & 0 & 41 & N \\ $\alpha_{43}$ & 0 & 41 & N \\ $\alpha_{44}$ & 127 & 361 & N \\ $\alpha_{45}$ & 145 & 361 & N \\ $\alpha_{46}$ & 349 & 523 & N \\ $\alpha_{47}$ & 0 & 41 & N \\ $\alpha_{48}$ & 0 & 41 & N \\ $\alpha_{49}$ & 126 & 389 & N \\ $\alpha_{5}$ & 0 & 39 & N \\ $\alpha_{50}$ & 136 & 418 & N \\ $\alpha_{51}$ & 136 & 418 & N \\ $\alpha_{52}$ & 206 & 552 & N \\ $\alpha_{53}$ & 8 & 45 & N \\ $\alpha_{54}$ & 8 & 45 & N \\ $\alpha_{55}$ & 1101 & 769 & Y \\ $\alpha_{56}$ & 1060 & 798 & Y \\ $\alpha_{57}$ & 1343 & 964 & Y \\ $\alpha_{58}$ & 1897 & 1304 & Y \\ $\alpha_{59}$ & 1623 & 1124 & Y \\ $\alpha_{6}$ & 0 & 39 & N \\ $\alpha_{60}$ & 1318 & 929 & Y \\ $\alpha_{61}$ & 0 & 41 & N \\ $\alpha_{62}$ & 0 & 41 & N \\ $\alpha_{63}$ & 69 & 369 & N \\ $\alpha_{64}$ & 70 & 377 & N \\ $\alpha_{65}$ & 71 & 377 & N \\ $\alpha_{66}$ & 116 & 531 & N \\ $\alpha_{67}$ & 5 & 46 & N \\ $\alpha_{68}$ & 5 & 46 & N \\ $\alpha_{69}$ & 719 & 649 & Y \\ $\alpha_{7}$ & 0 & 39 & N \\ $\alpha_{70}$ & 721 & 657 & Y \\ $\alpha_{71}$ & 1245 & 908 & Y \\ $\alpha_{72}$ & 1828 & 1267 & Y \\ $\alpha_{73}$ & 1560 & 1069 & Y \\ $\alpha_{74}$ & 952 & 811 & Y \\ $\alpha_{8}$ & 0 & 39 & N \\ $\alpha_{9}$ & 0 & 39 & N \\ \end{xtabular} \end{center} \begin{center} $\alpha$-formula to B\"uchi automaton translation, Algorithm 3, Chapter 5 \\ \begin{xtabular}{c|c|c|c} & time & mem & acc. cycle? \\ \hline orig. & 921 & 649 & Y \\ $\alpha_{1}$ & 0 & 39 & N \\ $\alpha_{10}$ & 0 & 39 & N \\ $\alpha_{11}$ & 0 & 39 & N \\ $\alpha_{12}$ & 0 & 39 & N \\ $\alpha_{13}$ & 0 & 39 & N \\ $\alpha_{14}$ & 0 & 39 & N \\ $\alpha_{15}$ & 0 & 39 & N \\ $\alpha_{16}$ & 0 & 39 & N \\ $\alpha_{17}$ & 0 & 39 & N \\ $\alpha_{18}$ & 0 & 39 & N \\ $\alpha_{19}$ & 0 & 39 & N \\ $\alpha_{2}$ & 0 & 39 & N \\ $\alpha_{20}$ & 0 & 39 & N \\ $\alpha_{21}$ & 0 & 39 & N \\ $\alpha_{22}$ & 0 & 39 & N \\ $\alpha_{23}$ & 0 & 39 & N \\ $\alpha_{24}$ & 0 & 39 & N \\ $\alpha_{25}$ & 0 & 39 & N \\ $\alpha_{26}$ & 0 & 39 & N \\ $\alpha_{27}$ & 0 & 39 & N \\ $\alpha_{28}$ & 0 & 39 & N \\ $\alpha_{29}$ & 0 & 39 & N \\ $\alpha_{3}$ & 0 & 39 & N \\ $\alpha_{30}$ & 0 & 39 & N \\ $\alpha_{31}$ & 0 & 39 & N \\ $\alpha_{32}$ & 0 & 39 & N \\ $\alpha_{33}$ & 0 & 39 & N \\ $\alpha_{34}$ & 0 & 39 & N \\ $\alpha_{35}$ & 0 & 39 & N \\ $\alpha_{36}$ & 0 & 39 & N \\ $\alpha_{37}$ & 0 & 39 & N \\ $\alpha_{38}$ & 0 & 39 & N \\ $\alpha_{39}$ & 0 & 39 & N \\ $\alpha_{4}$ & 0 & 39 & N \\ $\alpha_{40}$ & 0 & 39 & N \\ $\alpha_{41}$ & 0 & 39 & N \\ $\alpha_{42}$ & 0 & 41 & N \\ $\alpha_{43}$ & 0 & 41 & N \\ $\alpha_{44}$ & 69 & 361 & N \\ $\alpha_{45}$ & 70 & 361 & N \\ $\alpha_{46}$ & 115 & 523 & N \\ $\alpha_{47}$ & 0 & 41 & N \\ $\alpha_{48}$ & 0 & 41 & N \\ $\alpha_{49}$ & 72 & 389 & N \\ $\alpha_{5}$ & 0 & 39 & N \\ $\alpha_{50}$ & 76 & 418 & N \\ $\alpha_{51}$ & 77 & 418 & N \\ $\alpha_{52}$ & 120 & 552 & N \\ $\alpha_{53}$ & 9 & 47 & N \\ $\alpha_{54}$ & 8 & 47 & N \\ $\alpha_{55}$ & 1550 & 786 & Y \\ $\alpha_{56}$ & 1643 & 815 & Y \\ $\alpha_{57}$ & 1910 & 982 & Y \\ $\alpha_{58}$ & 2609 & 1304 & Y \\ $\alpha_{59}$ & 2382 & 1141 & Y \\ $\alpha_{6}$ & 0 & 39 & N \\ $\alpha_{60}$ & 1877 & 946 & Y \\ $\alpha_{61}$ & 0 & 41 & N \\ $\alpha_{62}$ & 0 & 41 & N \\ $\alpha_{63}$ & 72 & 369 & N \\ $\alpha_{64}$ & 70 & 377 & N \\ $\alpha_{65}$ & 74 & 377 & N \\ $\alpha_{66}$ & 116 & 531 & N \\ $\alpha_{67}$ & 9 & 48 & N \\ $\alpha_{68}$ & 9 & 48 & N \\ $\alpha_{69}$ & 796 & 676 & Y \\ $\alpha_{7}$ & 0 & 39 & N \\ $\alpha_{70}$ & 801 & 684 & Y \\ $\alpha_{71}$ & 1737 & 909 & Y \\ $\alpha_{72}$ & 2549 & 1267 & Y \\ $\alpha_{73}$ & 2152 & 1069 & Y \\ $\alpha_{74}$ & 1028 & 838 & Y \\ $\alpha_{8}$ & 0 & 39 & N \\ $\alpha_{9}$ & 0 & 39 & N \\ \end{xtabular} \end{center} \chapter{Content of the enclosed CD} \begin{itemize} \item source files \texttt{alpha.cc}, \texttt{alpha\_to\_ba.cc} and header files \texttt{alpha.hh} and \texttt{alpha\_to\_ba.hh} \item experimental data results \item \LaTeX~ source file of this thesis \end{itemize} \end{document}