宇宙塑膠人早期唱片

更多請溯源。下載請移步所鏈接之捷克網站。

File List:

• Plastic People-1969-72_Muz_bez_usi-iGalerie.cz.rar (鏈)
• Plastic_People-Francovka-iGalerie.cz.rar (鏈)
• Plastic_People-1973-75_Vozralej_jak_sliva-iGalerie.cz.rar (鏈)
• Plastic_People-1975_Egon_Bondys_Happy_Hearts_Club_Banned-iGalerie.cz.rar (鏈)

Temp Post - An Integration

Consider $a$ as a constant. \begin{align*} &2 \pi \int_1^2 (2a - ax) \sqrt{1+a^2} dx \\ =&2 \pi a \sqrt{1+a^2} ( 2 \int_1^2 1 dx - \int_1^2 x dx ) \\ =&2 \pi a \sqrt{1+a^2} \big( 2 (x|_1^2) - (\frac{1}{2}x^2|_1^2) \big) \\ =&2 \pi a \sqrt{1+a^2} (2 - (\frac{1}{2} \times 4 - \frac{1}{2})) \\ =&2 \pi a \sqrt{1+a^2} (\frac{1}{2}) \\ =&\pi a \sqrt{1+a^2} \end{align*}

Labelled CNF Conversion and its Improvement

The CNF classical conversion is expensive although it preserves the equivalence. However, CNF labelled conversion maintains the equi-satisfiability, i.e., if the original formula is SAT, then so is the converted version.

The idea is to label a part of formula as a new variable and convert only the labelled ones, which we can derive it now.

$$ \phi \leftrightarrow \phi [(p \wedge q) | B] \wedge CNF_{label} (B \leftrightarrow (p \wedge q))$$

where

\begin{align*} &CNF_{label} (B \leftrightarrow (p \wedge q)) \\ =& (\neg B \vee (p \wedge q)) \wedge (\neg (p \wedge q) \vee B) \\ =& (\neg B \vee p) \wedge (\neg B \vee q) \wedge (B \vee \neg p \vee \neg q)) \end{align*}

The same applies for disjunction, implication and double implication.

Improved version

By utilizing the results we had in last post (polarity), we can simplify the $CNF_{label}$ procedure. For instance, if $p \wedge q$ occurs positively, we only proceed with $CNF_{label} (B \rightarrow (p \wedge q))$, on negative occurrence, we instead use $CNF_{label} ((p \wedge q) \rightarrow B)$

An example

Convert the following using improved $CNF_{label}$. Credit: R. Sebastiani.

$$(A_1 \wedge A_2) \vee (A_3 \wedge \neg A_4) \vee (\neg A_1 \wedge \neg A_3) \vee (A_2 \wedge \neg A_4)$$

We start considering the whole formula as a sole variable $B$. And the rest conjunctions are $B_1$,$B_2$, $\cdots$, i.e.

$$\overbrace{\underbrace{(A_1 \wedge A_2)}_{B_1} \vee \underbrace{(A_3 \wedge \neg A_4)}_{B_2} \vee \underbrace{(\neg A_1 \wedge \neg A_3)}_{B_3} \vee \underbrace{(A_2 \wedge \neg A_4)}_{B_4}}^{B}$$

Finally, $B_i$s all occur positively, then we only use one-side implication. i.e.

\begin{align*} &B \wedge (B \rightarrow (B_1 \vee B_2 \vee B_3 \vee B_4)) \\ & \wedge (B_1 \rightarrow (A_1 \wedge A_2)) \\ & \wedge \cdots \end{align*}

Polarity in Propositional Logic

The polarity of a Boolean variable in a formula is recursively defined,

• $p$ occurs positively in $p$ itself.
• If $p$ occurs positively in $\phi$, then $\neg p$ occurs negatively in $\phi$, vice versa.
• If $p \wedge q$ or $p \vee q$ occur positively in $\phi$, then $p$ and $q$ occurs positively in $\phi$, and negatively for the negative occurrence.
• If $p \rightarrow q$ occurs positively in $\phi$, then $p$ negatively, $q$ positively. (i.e. $\neg p \vee q $)
• If $p \leftrightarrow q$ occurs in $\phi$, then $p$ and $q$ occur both negatively and positively in $\phi$.

Example:

$$B_1 \vee B_2 \vee B_3 \vee B_4$$

$B_1 \vee ( \cdots)$ occurs positively in itself. $B_1$ occurs positively since the former disjunction occurs positively. The same for all the other variables.

Clarke-Emerson Theorem

The theorem gives CTL formula an iterative interpretation of their denotational semantics. \begin{align*} [\mathbf{EG} \phi] &= \nu z. ([\phi] \cap [\mathbf{EX} z]) \\ [\mathbf{E}(\phi \mathbf{U} \psi)] &= \mu z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}z])) \\ [\mathbf{EF} \phi] &= \mu z. ([\phi] \cup [\mathbf{EX} z] \end{align*}

Appendix

• $[\mathbf{EX} \phi]$ is the existential pre-image of $[\phi]$.
• $\nu z. F z$ calculates the greatest fixed point.
• $\mu z. F z$ calculates the least fixed point.
• $\mathbf{EF} \phi = \mathbf{E}(\top \mathbf{U} \phi)$

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,