10 S. R. Schwer / Temporal reasoning without transitive tables (Rapport interne 2004 LIPN/LCR)

$$\bigcap_{\begin{array}{c}{{1\leq i\leq k}}\\ {{1\leq j\leq s_{i}}}\end{array}}\int_{X}^{\nu_{X}}{\mathcal{L}}_{I i_{j}}\neq\emptyset$$

In order to have a look on what kind of language is computed, let us revisit the unsatisfiable closed network of [2]. There are four intervals A, B, C,

D     ✠ ❅ ❅ ❅ ❅ ❅❅❘ ❄ s, m s, m o A C B ✟✟ ✟✟✟✯❍❍ ❍❍ ❍❨ d,d ∼ d,d ∼ f, f ∼ ✲
Fig. 11. Allen's instance of an inconsistent labeling.

D. We then take the alphabet X = {a, b, c, d} and L(2, 2, 2, 2) on X**. The data are :**

 $L_1=\int_X^\nu\left\{\left\{\begin{matrix}a\\ d\end{matrix}\right\}da,d\left\{\begin{matrix}a\\ d\end{matrix}\right\}a\right\}$  $L_2=\int_X^\nu\left\{\left\{\begin{matrix}c\\ d\end{matrix}\right\}dc,d\left\{\begin{matrix}c\\ d\end{matrix}\right\}c\right\}$  $L_3=\int_X^\nu dbdb$  $L_4=\int_X^\nu\left\{ca\left\{\begin{matrix}a\\ c\end{matrix}\right\},ac\left\{\begin{matrix}a\\ c\end{matrix}\right\}\right\}$  $L_5=\int_X^\nu\left\{bccb,cbbc\right\}$  $L_6=\int_X^\nu\left\{adda,daad\right\}$  The solution is
$L=L_1\cap L_2\cap L_3\cap L_4\cap L_5\cap L_6$ . 
that we now compute.

L1 ∩ L2=

$$\int_{X}^{\nu}\left\{\left\{{\atop{c}\atop{d}}\right\}d,d\left\{{\atop{c}\atop{d}}\right\},\left\{{\atop{a}\atop{d}}\right\}\left\{{\atop{c}\atop{d}}\right\},\left\{{\atop{c}\atop{d}}\right\}\left\{{\atop{a}\atop{d}}\right\}\right\}[a||c]$$

or equivalently, due to the lack of occurrences of b, L1 ∩ L2=

$${\Bigg[}\left\{\left\{{\atop{c}\atop{d}}\right\}d,d\left\{{\atop{c}\atop{d}}\right\},\left\{{\atop{d}\atop{d}}\right\}{\Bigg\{}{\atop{c}\atop{d}}\right\},\left\{{\atop{c}\atop{d}}\right\}{\Bigg\{}{\atop{c}\atop{d}}\right\}{\Bigg\{}{\atop{d}}\right\}\}.$$
$\left[\begin{matrix}a&b\\ c&d\end{matrix}\right]$  This language contains 164 words.  $\{\left\{\begin{matrix}a\\ c\\ d\end{matrix}\right\}bd,db\left\{\begin{matrix}a\\ c\\ d\end{matrix}\right\},\left\{\begin{matrix}a\\ d\end{matrix}\right\}b\left\{\begin{matrix}c\\ d\end{matrix}\right\},\left\{\begin{matrix}c\\ d\end{matrix}\right\}b\left\{\begin{matrix}a\\ d\end{matrix}\right\}\}.$  $[a||b||c]\\$ This language contains 52 words. 
L1 ∩ L2 ∩ L3 ∩ L4=

$$\{{\left\{\begin{matrix}a\\ d\end{matrix}\right\}}\,b\,{\left\{\begin{matrix}c\\ d\end{matrix}\right\}}\,,\,{\left\{\begin{matrix}c\\ d\end{matrix}\right\}}\,b\,{\left\{\begin{matrix}a\\ d\end{matrix}\right\}}\,\therefore\,{\left[\left\{\begin{matrix}a\\ c\end{matrix}\right\}||b\right]}$$

This language contains 6 words.

L1 ∩ L2 ∩ L3 ∩ L4 ∩ L5=

$$\{\left\{\begin{matrix}a\\ d\end{matrix}\right\}b\left\{\begin{matrix}c\\ d\end{matrix}\right\}\left\{\begin{matrix}a\\ c\end{matrix}\right\}b,\left\{\begin{matrix}c\\ d\end{matrix}\right\}b\left\{\begin{matrix}a\\ d\end{matrix}\right\}b\left\{\begin{matrix}a\\ c\end{matrix}\right\}\}$$  in above, we have 2 equal. 
This language has 2 words.

L1 ∩ L2 ∩ L3 ∩ L4 ∩ L5 ∩ L6 = ∅
This language is empty: the problem is unsatisfiable.

## 6. Temporal Reasoning About Concurrent Systems

Most of the temporal properties of programs have been studied inside either the framework of temporal logics or modal logic. Temporal reasoning about concurrent systems can be partitioned in a natural way into two classes related to the modality used : necessity, symbolized by ✷ or possibility, symbolized by ✸. Translated in a temporal framework, we use the terms always and sometime**. These modalities were studied first by the**
Megarians3**, then by Aristotle and the Stoic. Despite their variant, these modalities are linked to**
the universal ∀ and particular ∃ **quantifiers.**
Manna and Pnuelli [23,24], defined three important classes of temporal properties of concurrent programs that are investigated inside the modal 3**A school founded by Euclid of Megaric, student of**
Socrates, like Plato, this school was concurrent of Aristotle's one.