Davide Grossi edited untitled.tex  about 8 years ago

Commit id: a1034381621976359d97a165bdbbd699f3bcd619

deletions | additions      

       

We list some relevant known results about $\K^{\mu}$. The logic has a sound and (weakly) complete axiom system \cite{Walukiewicz_2000}. The satisfiability problem of $\K^{\mu}$ is decidable \cite{Streett_1984}. The complexity of the model-checking problem for $\K^{\mu}$ is known to be in NP $\cap$ co-NP \cite{Gr_del_1999}. However, it is known that the model-checking problem for a formula of size $m$ and alternation depth $d$ on a system of size $n$ is $O(m \cdot n^{d+1})$ \cite{Emerson_2001}, where the alternation depth of a formula of $\L^{\K^{\mu}}$ is the maximum number of $\mu/\nu$ alternations in a chain of nested fixpoints.  \subsection{On the Logic of Influence Networks} Graphs}  \paragraph{The class of Influence Graphs}  The class of (possibly infinite) influence graphs is characterized by the following properties:  \begin{align}  \lbox \phi \limp \ldia \phi & & \mbox{(seriality)} \\  \ldia \phi \limp \lbox \phi & & \mbox{(functionality)}  \end{align}  \paragraph{Expressing convergence}  \ldots  \paragraph{Validities ofthe Class of  Influence Networks} Graphs}  \ldots  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%