Expressiveness of LTL, CTL, CTL*

Consider the following examples.

• $\mathbf{GF}p = \mathbf{AGAF}p = \mathbf{AGF} p$
• The existential quantifier is not possible in LTL. E.g., $\mathbf{EF}p$
• $\mathbf{FG}p \neq \mathbf{AFAG}p$, see Fig 1.
• $\mathbf{EFG}p \neq \mathbf{FG}p \neq \mathbf{EFAG} p$
• $\phi \in$ LTL $\Rightarrow \mathbf{A} \phi \in $CTL*
• All CTL formulae are automatically CTL*.

Fig. 1 A Kripke Model $M \models \mathbf{FG}p$ but $M \not \models \mathbf{AFAG}p$

It says

• They can all express some common formulae.
• Some CTL formulae are not covered in LTL.
• Some LTL formulae can not be expressed by CTL.
• Some CTL* formulae are covered neither in CTL nor LTL.
• CTL* subsumes both CTL and LTL.

CTL Fixed-point Model Checking With Illustrations

This is a mutual-exclusion protocol for two processes. Here is the tikz model representation. Credit: R. Sebastiani from disi.unitn.it

\begin{tikzpicture}[node distance = 2.5cm]
 \tikzstyle{every state}=[fill=none]
 \node[state] (a) {N1,N2};
 \node[above of=a,yshift=-1cm] {$[C_{1} \wedge C_{2}]$};
 \node[state,xshift=-2cm] (b) [below left of=a]{T1,N2}; 
 \node[state,xshift=2cm] (c) [below right of=a]{N1,T2};
 \node[state] (d) [below left of=b]{C1,N2}; 
 \node[state] (e) [below right of=b]{T1,T2};
 \node[state] (f) [below left of=c]{T1,T2}; 
 \node[state] (g) [below right of=c]{N1,C2};
 \node[state] (h) [below right of=d]{C1,T2}; 
 \node[state] (i) [below right of=f]{T1,C2};
 \path[->] +(-1,1) edge (a);
 \path[->] (a) edge[red] (b) (a) edge (c) (b) edge[red] (d) (b) edge (e) (c) edge[red] (f) (c) edge (g) (d) edge (h) (e) edge[red] (h) (f) edge (i) (g) edge[red] (i);
 \draw[->] (i) .. controls +(180:4cm) and +(0:4cm) .. (b);
 \draw[->] (h) [red].. controls +(0:4cm) and +(180:4cm) .. (c);
 \path[->] (d) edge[red,bend left,out=60] (a);
 \path[->] (g) edge[bend right,out=-60] (a);
\end{tikzpicture}

To create a Bezier curve, we add some control points in the path, for instance:

\draw[->] (i) .. controls +(180:4cm) and +(0:4cm) .. (b);

The procedure for checking some CTL properties is illustrated in this pdf file.

• AG¬(C1 ∧ C2 )
• AG(N1 → EFT1)

Gold Price History (1849-2012)

Here is the datasheet,

PHP: Public, Protected and Private

These three keywords define the visibility of variables.

• public: visible for both inside and outside
• protected: visible only to its own methods
• private: similar to protected, intended to be accessed only by the class who defines it

An Instance

error_reporting(E_ALL);
class foo{
   public    $a=1;
   protected $b=2;
   private   $c=3;

   function stampa()
   {
      echo $this->b;
      echo $this->c;
   }
}
class bar extends foo{
   function __construct(){
      $this->b = 4;
      $this->c = 5;
   } 
}
$A = new foo;
echo $A->a;
$A->stampa();
$B = new bar;
$B->stampa();

Here is the output,

12343

Notes

• The version of tested php: 5.3.6-13
• The instance shows the re-assigning of the private member doesn't make any difference. The inheriting class can not modify private members.
• The private member is still visible (printed) to the inheriting class.

Ubuntu: LAMP Memoir

Installing

sudo apt-get install apache2
sudo apt-get install php5 libapache2-mod-php5
sudo apt-get install mysql-server
sudo apt-get install php5-mysql
sudo apt-get install libapache2-mod-auth-mysql

Restarting Service

sudo service apache2 restart
sudo service mysql restart

Interacting with MySQL

mysql -p 
mysql -p db_name < import.sql

Installing phpMyAdmin

sudo apt-get install phpmyadmin

Let Apache know about phpMyAdmin:

sudo gedit /etc/apache2/apache2.conf
Include /etc/phpmyadmin/apache.conf

Use php Mail with PEAR

If you see Failed opening required 'Mail.php', this means pear/Mail is not installed.

wget http://pear.php.net/go-pear.phar
sudo php go-pear.phar
sudo pear install Mail
sudo pear install Net_SMTP

Configure that base path be /usr/share/pear so that you don't need to change the include path. On wrong installation, uninstall it this way

sudo pear uninstall pear

Troubleshooting

After any change, restart service to see effects.

• Program halts when accessing database: the module php5-mysql may be not installed
• mysql_connect gives an empty output, this may be caused by a not guaranteed permission. Try use root or update the user with proper privilege.

Defining Macros in MathJax

In case of malfunction of other methods, one needs to include macros' configurations separately from another environment configuration. Also use "\\" instead of "\" to escape. For instance,

<script type="text/x-mathjax-config;executed=true">
MathJax.Hub.Config({
  tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}
});
MathJax.Hub.Config({
  TeX:{
      Macros: {
        p :'{\\mathcal{P}}',
        np :'{\\mathcal{NP}}'
      }
  }
});
</script>

Test

$$\p =? \np$$

Effectively Enable MathJax on Blogger

The Cause

Simply adding the javascript code in the template may not work for all bloggers, at least not for me. The reason is that Blogger filters the code one adds into the template and some of configurations are encoded in html entities, thus not functioning at all.

The Working Method

Go to the console, select layout and add a gadget "HTML/Javascript", put the following code inside.

<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js">
MathJax.Hub.Config({
extensions: ["tex2jax.js","TeX/AMSmath.js","TeX/AMSsymbols.js"],
jax: ["input/TeX", "output/HTML-CSS"],
tex2jax: {
inlineMath: [ ['$','$'], ["\\(","\\)"] ],
displayMath: [ ['$$','$$'], ["\\[","\\]"] ],
},
"HTML-CSS": { availableFonts: ["TeX"] }
});
</script>

Make sure this gadget is available globally.

Demo Test

$$\cos x = \frac{e^{ix}+e^{-ix}}{2}$$