Information Technology Reference
In-Depth Information
The synthesis algorithm then combines service descriptions in terms of
these sets into the synthesis universe, that is, an abstract representation
of all possible solutions that contains all service sequences that are valid
(type-correct) executions, without taking into account any problem-specific
information. The synthesis universe is in essence an automaton that connects
states with edges according to available services. While each state represents
a subset of all types (abstract and concrete), the connecting edges perform
the transition on those types, according to input and output specifications of
services. Every path in this automaton, starting from a state that represents
the initially available data, constitutes an executable service sequence. As the
synthesis universe is usually very large, it is not explicitly generated from the
domain definition, but specified by sets of constraints that are evaluated on
the fly during the synthesis process.
Note that the synthesis method uses
taxonomies
to define semantic classi-
fications of types and services. Taxonomies are simple ontologies that relate
entities in terms of
is-a
relations and thus allow for the hierarchical struc-
turing of the involved types and services. The actually available services and
types are named
concrete
, whereas semantic classifications are named
abstract
.
The taxonomies are considered by the synthesis algorithm when constructing
the synthesis universe and when evaluating type and service constraints.
Formally, as for instance defined in [178], the synthesis universe is a triple
(
T,S
c
,Trans
), where
•
T
is a set of concrete and abstract types
•
S
c
is a set of concrete services
S
c
.
Note that the synthesis universe only contains the set of concrete services
(
S
c
), as it contains real executable paths. Abstract services (
S
a
) are solely
used as part of the specification formula (see below). The set of all services is
denoted as
S
=
S
a
∪
•
Trans
=
{
(
t, s, t
)
}
is a set of transitions where
t, t
⊆
T
and
s
∈
S
c
.Thesetsoftypes
T
c
,
T
a
and
T
are defined likewise.
With the definitions of
USE
,
GEN
,
FORBID
,and
KILL
, a service
s
S
c
can be defined as a transformation on the power set of types as
follows:
∈
s
:2
T
2
T
→
t
→
(
t
\
KILL
(
s
))
∪
GEN
(
s
)
For
s
to be admissible in a type state
t
⊆
T
, the following conditions must be
met:
USE
(
s
)
. At last, the synthesis universe
can be constructed from the service definitions as follows: for each
t
⊆
t
and
FORBID
(
s
)
∩
t
=
∅
T
,a
state in the universe is created. The transition (
t, s, t
) is added to
Trans
iff
s
is admissible in
t
and
t
=(
t
⊆
\
KILL
(
s
))
∪
GEN
(
s
).
Search WWH ::
Custom Search