From Interfaces to property Sets

To install a model of the observable behavior one has to start with the assumptions about the intended interface of the involved agents as well as about the necessary actions to be done to realize a certain task. The idea of a formal description of the behavior is an example of the general case that some measuring agents which are looking to the real world and are transforming certain perceivable properties of the real world into a data language $L_{PROP}$ representing those observed properties. As it can be seen in figure 2.4 can the measuring agent either be a human person who is looking to the world and who writes his subjective observations down with some data description language $L_{PROP}$ . In another case researchers have agreed to use an objective measuring method which is independent from a human person and which is certified to delivere repeatedly the same data if the object is the same.

**Figure 2.4:** From Reality to Data descriptions with Properety Sets
$\includegraphics[width=3.5in]{from_interface_to_properties_3.5in.eps}$

There is no agreement with regard to a genera data language. In the realm of model checking there are different examples of data languages which are used to describe properties which will be summarized here as follows:

$\displaystyle Names$	$\displaystyle \subseteq$	$\displaystyle UPPER \times LOWER^{*}$	(2.1)
$\displaystyle Names$	$\displaystyle \subseteq$	$\displaystyle L_{PROP}$	(2.2)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f = f') \in L_{PROP}$	(2.3)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \neq f') \in L_{PROP}$	(2.4)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f < f') \in L_{PROP}$	(2.5)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f > f') \in L_{PROP}$	(2.6)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \leq f') \in L_{PROP}$	(2.7)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \geq f') \in L_{PROP}$	(2.8)

The expressions of $L_{PROP}$ as such have no meaning. Only the user of these expressions is responsible to attach some meaning to these expressions. Thus the expression Size is a name property, $\neg$ Size would be a negated name property,

coud be interpreted as a relation between the name property 'Size' and the name value '4', saying that 'Size' is 'larger than' '4'.

Finite subsets of properties can be used as a kind of property states (P-states) like e.g. {

If one describes the different configurations of an interface as a collection of P-states which change during time triggered by certain events then one can decribe the behavior of an interface with the aid of a directed graph whose vertices are P-states and whose edges are those transitions between property sets which can be observed -or should be observable- in a certain interface. Therefore one could write:

$\displaystyle INTERFACE(x)$	$\displaystyle iff$	$\displaystyle \langle V, E, Act, P-states\rangle$	(2.9)
$\displaystyle Act$	$\displaystyle \subseteq$	$\displaystyle \Sigma^{*}$	(2.10)
$\displaystyle P-states$	$\displaystyle \subseteq$	$\displaystyle 2^{L_{PROP}}$	(2.11)
$\displaystyle V$	$\displaystyle \subseteq$	$\displaystyle P-states$	(2.12)
$\displaystyle E$	$\displaystyle \subseteq$	$\displaystyle V \times Act \times V$	(2.13)

With these assumptions one can translate different kinds of interfaces and their dynamics into sets of properties (P-states) embedded into a network of transitions (cf. 2.5).