=Paper=
{{Paper
|id=None
|storemode=property
|title=Insertion Modeling System and Constraint Programming
|pdfUrl=https://ceur-ws.org/Vol-716/ICTERI-2011-CEUR-WS-paper-3-p-51-64.pdf
|volume=Vol-716
|dblpUrl=https://dblp.org/rec/conf/icteri/LetichevskyPLBK11
}}
==Insertion Modeling System and Constraint Programming==
https://ceur-ws.org/Vol-716/ICTERI-2011-CEUR-WS-paper-3-p-51-64.pdf
Insertion Modeling System And Constraint
Programming
Alexander A. Letichevsky1 , Olexander A.Letychevskyi1 , Vladimir S.
Peschanenko2 , Igor O. Blynov2 , Dmitry M. Klionov
1
Glushkov Institute of Cybernetics, Academy of Sciences of
Ukraine,let@cyfra.net,lit@iss.org.ua
2
Kherson State University, vladimirius@gmail.com, anubis.igor@gmail.com,
soulslayermaster@gmail.com
Abstract. The paper relates to practical aspects of insertion model-
ing. Insertion modeling system is an environment for the development
of insertion machines, used to represent insertion models of distributed
systems. The architecture of insertion machines and insertion modeling
system IMS is presented. Insertion machine for constraint programming
is specified as an example, and as a starting point of ‘verifiable program-
ming’ project.
1 Introduction
Insertion modeling is the approach to modeling complex distributed systems
based on the theory of interaction of agents and environments [1–3]. Mathe-
matical foundation of this theory was presented in [4]. During the last decade
insertion modeling was applied to the verification of requirements for software
systems [5–9].
First time the theory of interaction of agents and environments was proposed
as an alternative to well known theories of interaction such as Milner’s CCS [10]
and pi-calculus [11], Hoare’s CSP [12], Cardelli’s mobile ambients [13] and so
on. The idea of decomposition of a system to a composition of environment
and agents inserted into this environment implicitly exists in all theories of
interaction and for some special case it appears explicitly in the model of mobile
ambients.
Another source of ideas for insertion modeling is the search of universal pro-
gramming paradigms such as Gurevich’s ASM [14], Hoare’s unified theories of
programming [15], rewriting logic of Meseguer [16]. These ideas were taken as a
basis for the system of insertion programming [17] developed as the extension
of algebraic programming system APS [18]. Now this system initiated the devel-
opment of insertion modeling system IMS which started in Glushkov Institute
of Cybernetics. The development of this system is based on the version of APS
enhanced by the former student of the author V.Peschanenko. The first version
of IMS and some simple examples of its use are available from [19].
To implement the insertion model in IMS one must develop insertion machine
with easily extensible input language, the rules to compute insertion functions
52 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
and a program of interpretation and analyzing of insertion models. The architec-
ture, input languages and examples of insertion machines and insertion modeling
system are considered in the paper.
2 The Architecture of Insertion Modeling System
Insertion modeling system is an environment for the development of insertion
machines and performing experiments with them. The notion of insertion ma-
chine was first introduced in [17] and it was used as a tool for programming
with some special class of insertion functions. Later this notion was extended
for more wide area of applications, different levels of abstraction, and multilevel
structures.
Insertion model of a system represent this system as a composition of envi-
ronment and agents inserted into it. Contrariwise the whole system as an agent
can be inserted into another environment. In this case we speak about internal
and external environment of a system. Agents inserted into the internal environ-
ment of a system themselves can be environments with respect to their internal
agents. In this case we speak about multilevel structure of agent or environment
and about high level and low level environments.
As usually, insertion function is denoted as E[u] were E is the state of envi-
ronment and u is the state of an agent (agent in a given state). E[u] is a new
environment state after insertion an agent u. So, the expression E[u[v], F [x, y, z]]
denotes the state of a two level environment with two agents inserted into it. At
the same time E is an external environment of a system F [x, y, z] and F is an
internal environment of it. All agents and environments are labeled or attributed
transition systems (labeled systems with states labeled by attribute labels [9]).
The states of transition systems are considered up to bisimilarity. This means
that we should adhere to the following restriction in the definition of states: if
E ∼B E 0 and u ∼B u0 then E[u] ∼B E 0 [u0 ].
The main invariant of bisimilarity is the behavior beh(E) of transition system
in the state E (an oriented tree with edges labeled by actions and nodes labeled
by attribute labels). Therefore the restriction above can be written as follows:
beh(E) = beh(E 0 ) ∧ beh(u) = beh(u0 ) ⇒ beh(E[u]) = beh(E 0 [u0 ])
Behaviors themselves can be considered as states of transition systems. If the
states are behaviors then the relation above is valid automatically, because in this
case beh(E) = E, beh(u) = u. Otherwise the correctness of insertion function
must be proved in addition to its definition. In any case we shall identify the
states with the corresponding behaviors independently from their representation.
To define finite behaviors we use the language of behavior algebra (a kind of
process algebra defined in [4]). This algebra has operation of prefixing, nondeter-
ministic choice, termination constants (∆, 0, ⊥) and approximation relation. For
attributed transition systems we introduce the labeling operator for behaviors.
To define infinite behaviors we use equations in behavior algebra. Usually these
equations have the form of recursive definitions ui = Fi (u), i ∈ I. Left hand sides
Insertion Modeling System And Constraint Programming 53
of these definitions can depend on parameters ui (xi ) = Fi (u, x), i ∈ I. To define
the attribute labels we use the set of attributes, symbols taking their values in
corresponding data domains. These attributes constitute a part of a state of a
system and change their values in time. All attributes are devided to external
(observable) and internal (nonobservable). By default the attribute label of a
state is the set of values of all observable attributes for this state.
The general architecture of insertion machine is represented on the fig. 1.
Fig. 1. Architecture of Insertion Machine
The main component of insertion machine is model driver, the component
which controls the machine movement along the behavior tree of a model. The
state of a model is represented as a text in the input language of insertion
machine and is considered as an algebraic expression. The input language include
the recursive definitions of agent behaviors, the notation for insertion function,
and possibly some compositions for environment states. The state of a system
must be reduced to the form E[u1 , u2 , . . . ]. This functionality is performed by
the module called agent behavior unfolder. To make the movement, the state of
environment must be reduced to the normal form
X
ai .Ei + ε
i∈I
where ai are actions, Ei are environment states, ε is a termination constant. This
functionality is performed by the module environment interactor. It computes
the insertion function calling if it is necessary the agent behavior unfolder. If
the infinite set I of indices in the normal is allowed, then the weak normal form
a.F + G is used, where G is arbitrary expression of input language.
Two kinds of insertion machines are considered: real type or interactive and
analytical insertion machines. The first ones exist in the real or virtual envi-
ronment, interacting with it in the real or virtual time. Analytical machines
54 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
intended for model analyses, investigation of its properties, solving problems
etc. The drivers for two kinds of machines correspondingly are also divided on
interactive and analytical drivers.
Interactive driver after normalizing the state of environment must select ex-
actly one alternative and perform the action specified as a prefix of this alterna-
tive. Insertion machine with interactive driver operates as an agent inserted into
external environment with insertion function defining the laws of functioning
of this environment. External environment, for example, can change a behav-
ior prefix of insertion machine according to their insertion function. Interactive
driver can be organized in a rather complex way. If it has criteria of successful
functioning in external environment intellectual driver can accumulate the in-
formation about its past, develop the models of external environment, improve
the algorithms of selecting actions to increase the level of successful functioning.
In addition it can have specialized tools for exchange the signals with external
environment (for example, perception of visual or acoustical information, space
movement etc.).
Analytical insertion machine as opposed to interactive one can consider dif-
ferent variants of making decision about performed actions, returning to choice
points (as in logic programming) and consider different paths in the behavior
tree of a model. The model of a system can include the model of external en-
vironment of this system, and the driver performance depends on the goals of
insertion machine. In the general case analytical machine solves the problems
by search of states, having the corresponding properties(goal states) or states in
which given safety properties are violated. The external environment for inser-
tion machine can be represented by a user who interacts with insertion machine,
sets problems, and controls the activity of insertion machine.
Analytical machine enriched by logic and deductive tools can be used for
symbolic modeling. The state of symbolic model is represented by means of
properties of the values of attributes rather then their concrete values.
General architecture of insertion modeling system is represented on fig. 2.
High level model driver provides the interface between the system and external
environment including the users of the system. Design tools based on algebraic
programming system APS are used for the development of insertion machines
and model drivers for different application domains and modeling technologies.
Verification tools are used for the verification of insertion machines, proving
their properties statically or dynamically. Dynamic verification uses generating
symbolic model traces by means of special kinds of analytical model drivers and
deductive components.
The repository of insertion machines collects already developed machines and
their components which can be used for the development of new machines as
their components or templates for starting. Special library of APLAN functions
supports the development and design in new projects. The C++ library for IMS
supports APLAN compilers and efficient implementation of insertion machines.
Deductive system provides the possibility of verification of insertion models.
Insertion Modeling System And Constraint Programming 55
Fig. 2. Architecture of Insertion Modeling System IMS
3 Input Languages of Insertion Machines
Input language of insertion machine is used to describe the properties of a model
and its behavior. This description consists of the following parts: environment
description, behavior description (including the behavior of environment and the
behaviors of agents), and insertion function. The behavior description has the
following very simple syntax:
::= Delta | bot | 0 | < action > | . |
+ |
[]|
::=:
Therefore, the language of behavior algebra (termination constants, prefix-
ing and nondeterministic choice) is extended by functionals expressions and ex-
plicit representation of insertion function. The syntax and semantics of actions,
environment states, and functional expressions are defined in the environment
description. We shall not consider all possibilities and details of environment
description language restricting ourselves by making only some necessary com-
ments.
First of all note, that all main components of behavior algebra language
(actions, environment states, and functional expressions) are algebraic or logic
expressions of base language (terms and formulas). This language is a multi-
sorted (multitype) first order logic language. The signature of this language is
defined in the environment description. Functional and predicate symbols can
be interpreted and uninterpreted. Interpreted symbols have fixed domains and
56 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
interpretations given by algorithms of computing values or reducing to canonical
forms. All uninterpreted symbols have types and their possible interpretations
are restricted by definite domains and ranges. Uninterpreted functional sym-
bols are called attributes. They represent the changing part of the environment.
Attributes of arity 0 are called simple attributes, others are called functional
ones. Predicates are considered as functions ranging in Boolean type {0, 1}. If
an attribute f has functional type (τ1 , τ2 , . . .) → τ then attribute expressions
f (t1 , t2 , . . .) are available for all other expressions.
3.1 Examples of Insertion Machines
The simplest insertion machines are machines for parallel and sequential inser-
tion. Insertion function is called sequential if E[u, v] = E[u; v] where ”;” means
sequential composition of behaviors. Special case of sequential insertion is a
strong sequential composition: E[u] = (E; u). This definition assumes that ac-
tions of agents and environment are the same and environment is defined by
its behaviors. The sequentiality of this composition follows from associativity of
sequential composition of behaviors.
Example of insertion machine with strong sequential insertion is represented
on fig. 3.
Model Sequential
interactor rs(P,Q,a)(
Delta[P+Q]=Delta[P]+Delta[Q],
Delta[a.P]=a.Delta[P],
Delta[P]=Delta[unfold P],
Q[P]=(Q;P)
);
unfolder rs(x,y)(
(x;y)=seq(x,y),
A=a.A+Delta,
C=c.C+Delta
);
initial(C[A]);
terminal(Delta[Delta])
)
Fig. 3. Example of Strong Sequential Insertion
The function seq is a function from IMS library that defines the sequential
composition of behaviors:
X X
(u; v) = a.(u0 ; v) + (ε; v), (0; v) = 0, (∆; v) = v, (⊥; v) = ⊥
a
u→u0 u=u+ε
P
The function unfold reduces the behavior expression to normal form ai .ui +ε.
This insertion machine generates a word cn am with nondeterministically chosen
Insertion Modeling System And Constraint Programming 57
m, n ≥ 0 and successfully terminates. We can define as the condition for the
goal state the equality m = n and the driver for this machine will terminate on
traces cn an .
An example of sequential (not strong) insertion is shown on fig. 4.
Model Imperative(
insertion rs(P,Q,H,a,x,y,u,v)(
E[P+Q]=Delta[P]+Delta[Q],
E[define env H.P]=H[P],
E[(x:=y).P]=assign proc(E,x,y,P),
E[check(u,x,y).P]=if(compute obj(E,u),E[x;P],E[y;P]),
E[a.P]=a.Delta[P],
E[P]=E[unfold P]
)where(
assign proc:=proc(E,x,y,P)(E.x−→compute obj(E,y);return E[P])
);
behaviors rs(P,Q,x,y,z,u)(
(x;y)=seq(x,y),
(u→ else Q)=check(u,P,Q),
while(u,P)=check(u,(P;while(u,P)),Delta),
for(x,y,z,P)=(x;while(y,(P;z)))
);
initial(
define env obj(i:Nil,x:10,y:Nil,fact:Nil);
y:=1;for(i:=1,i ≤ x,i:=i+1,y:=y*i);
fact:=y
);
terminal rs(E)(E[Delta]=1,E=0)
)
Fig. 4. Model of Simple Imperative Language
This example is a model of simple imperative language and can be considered
as insertion representation of its operational semantics.
Insertion function is called a parallel insertion function if E[u, v] = E[u k v].
Special case of parallel composition is a strong parallel insertion:E[u] = E k u].
As in the case of strong sequential composition this definition assumes that
actions of environment and agents are the same. Example of a model with strong
parallel insertion is presented on the fig. 5. Functions synchr, lmrg, and delta
from IMS library are used for definition of parallel composition. Their meaning
can be define by the following formulas:
X
synchr(x, y) = (a × b).(x0 , y 0 ),
a
x→x0
b
y →y 0
58 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
Model Parallel
interactor rs(P,Q,a)(
Delta[P+Q]=Delta[P]+Delta[Q],
Delta[a.P]=a.Delta[P],
Delta[P]=Delta[unfold P],
Q[P]=(Q k P )
);
unfolder rs(x,y,n)(
(x;y)=seq(x,y),
x k y = synchr(x,y)+lmrg(x,y)+lmrg(y,x)+delta(x,y),
x |ˆ 1=x,
x |ˆ 2=synchr(x,x)+lmrg(x,x)+delta(x,x),
x |ˆ n= x k (x |ˆ(n-1))),
);
initial (Delta[((a;b) k (a;b));a+b ]);
terminal (Delta[Delta])
)
Fig. 5. Example of Strong Parallel Insertion
X X
lmrg(x, y) = a. (x0 k y) , delta(x, y) = εkµ
a
x→a0 x=x+ε
y=y+µ
3.2 Restrictions on Insertion Functions
The most typical restriction is additivity. Insertion function is called additive if
E[u+v] = E[u]+E[v], (E +F )[u] = E[u]+F [u]. Another restriction, which allow
to reduce the number of considered alternatives when behaviors are analyzed is
the commutativity of insertion function: E[u, v] = E[v, u]. Especially the parallel
insertion is a commutative one. Some additional equations: 0[u] = 0, ∆[u] =
u, ⊥[u] = bot.
The state of environment is called indecomposable if from E = F [u] it follows
that E = F and u = ∆. Equality means bisimilarity. The set of all indecom-
posable states constitutes the kernel of a system. Indecomposable states (if they
exist) can be considered as states of environment without inserted agents. For
indecomposable states usually the following equations hold: E[0] = 0, E[∆] =
E, E[⊥] = ⊥.
In [3] the classification of insertion functions was presented: one-step in-
sertion, head insertion, and look-ahead insertion. Later we shall use insertion
functions with the following main rule:
a b
E → E 0 , α : u → β : u0
c , P (E, a, α, b, β, c),
E[α : u] → E 0 [β : u0 ]
where P is a continuous predicate. Continuous means that the value of this
predicate depends only on some part of behavior tree in the environment state
Insertion Modeling System And Constraint Programming 59
E, which has a finite height (prefix of the tree E of finite height). Hereby, this
rule refers to a head insertion. The rules for indecomposable environment states
and for termination constants should be added to the main rule.
The next rule
a b
E → E 0 , u → β : u0
c , P (E, a, c),
E [u] → E 0 [u0 ]
is the particular case for the head insertion rule in combination with additivity
and parallel insertion or commutativity requirements. Such rule will be named
permitted rule. It could be interpreted by as follows: agent can execute the action
a, and environment permits to execute this action. Predicate E for permitted
rule will be named permitted predicate.
4 Constraint Programming
Constraint programming is a powerful paradigm for solving combinatorial search
problems that draws on a wide range of techniques from artificial intelligence,
computer science, databases, programming languages, and operations research.
Constraint programming is currently applied with success to many domains, such
as scheduling, planning, vehicle routing, configuration, networks, and bioinfor-
matics [24].
The Constraint programming paradigm has some resemblance to traditional
Operations Research (OR) approach, in that the general path to a solution is:
1. analyzing the problem to solve, in order to understand clearly which are its
parts;
2. determining which conditions(relationships) hold among those parts: these
relationships and conditions are key to the solving, for they will be used to
model the problem;
3. stating such conditions(relationships) as equations; to achieve this step not
only the right variables and relationships must be chosen: as we will see, Con-
straint programming usually offers a series of different constraint systems,
some of which are better suited than others for a given task;
4. setting up these equations and solving them to produce a solution; this
is usually transparent to the user, because the language itself has built-in
solvers [25].
There are, however, notable differences with OR, mainly in the possibility
of selecting different domains of constraints, and in the dynamic, generation
of those constraints. This seamless combination of programming and equation
solving accounts for some of the unique components of Constraint Programming:
– the use of sound mathematical methods: well-known and proved algorithms
are provided as intrinsic, builtin components of Constraint programming
languages and tools;
– the provision of means to perform programmed search, especially in Con-
straint programming (were search is implicit in language itself);
60 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
– the possibility of developing modular, hybrid models, when necessary: many
Constraint programming systems offer different constraint systems, which
can be combined to model the various parts of the problem using the tool
more adequate for them;
– the flexibility provided by the programming language used, which allows
the programmer to create the equations to be solved dynamically, possibly
depending on the input data.
As with any other computational approach, all problems are amenable to be
tackled with Constraint programming; notwithstanding, there are some types of
problems which can be solved with comparatively little effort using Constraint
programming based tools. Those applications share some general characteristics:
– No general, efficient algorithms exist (NP-completeness): specific techniques
(heuristics) must be used. These are usually problems with a heavy com-
binatorial part, and enumerating solutions is often impractical altogether.
A fast program using usual programming paradigms is often too hard and
complicated to produce, and normally it is so tied to the particular problem
that adapting it to a related problem is not easy.
– The problem specification has a dynamic component: it should be easy to
change programs rapidly to adapt. This has points in common with the
previous item: Constraint programming tools have builtin algorithms which
have been tuned to show good behavior in a variety of scenarios, so updating
the program to new conditions amounts to changing the setting up of the
equations.
– Decision support required: either automatically in the program or in coopera-
tion with the user. Many decisions can be encoded in mathematical formulae,
which appear as rules and which are handled by the internal solvers, so (al-
though, of course, not always) there is no need to program explicit decision
trees [26].
Among the applications with these characteristics, the following may be
cited: planning, scheduling, resource allocation, logistics, circuit design and veri-
fication, finite state machines, financial decision making, transportation, spatial
databases, etc.
5 Insertion Machine for Constraint Programming
Some example of insertion machines and restrictions for insertion function are
in [3, 9, 23]. In this section we try to show how to use insertion modelling for
constraint programming [26]. The problems of constraint programming, where
a main goal is behavior of the system, is the closest to the insertion modelling.
For example, the problem of wolf-goat-cabbage [27] (A farmer wishes to transfer
(by boat) a wolf, a goat, and a cabbage from the left bank of a river to the
right bank. If left unsupervised, the wolf will eat the goat and the goat will eat
Insertion Modeling System And Constraint Programming 61
the cabbage, but nothing will happen as long as the farmer is near. Beside the
farmer there is only a place for one item in the boat).
Let’s consider a formalization of this problem in insertion modelling. Let E
be the next enviroment:
obj(
constraints : rs(x, y, z)(
obj(W olf : lef t, Goat : lef t, x, F erryman : right) = 0,
obj(W olf : right, Goat : right, x, F erryman : lef t) = 0,
obj(x, Goat : lef t, Cabbage : lef t, F erryman : right) = 0,
obj(x, Goat : right, Cabbage : right, F erryman : lef t) = 0,
obj(W olf : z, x, y, F erryman : z) = 1,
obj(x, Goat : z, y, F erryman : z) = 1,
obj(x, y, Cabbage : z, F erryman : z) = 1
);
initial : obj(
W olf : lef t,
Goat : lef t,
Cabbage : lef t,
F erryman : lef t
)
)
where initial is initial state where all creatures are in left bank of the river,
constraits are constraint equations with right part of 0 define non possible cases
(0 is the neutral element of non-deterministic choice + of insertion modeling)
and with 1 if ferryman could transport thous creatures in that case. These both
values are covered by two different states of ferry: 1 is just before ferry and 0 -
after.
The coresponded input data could be defined in the following way:
(f erry W olf k f erry Goat k f erry Cabbage).assetion constraints
So, the transition relation of the system is defined in fig. 6.
f erry x
ϕ [p] −−−−−→ ϕi [p] , constraints(ϕ) = 1
f erry x
ϕ [p] −−−−−→ 0, constraints(ϕi ) = 0 ∨ ¬constraints(ϕ) = 1
assetion constraints
ϕ [p] −−−−−−−−−−−−−−→ ϕ [p] , ¬constraints(ϕ) = 0
assetion constraints
ϕ [p] −−−−−−−−−−−−−−→ 0, constraints(ϕ) = 0
Fig. 6. Relations of System’s Transitions
where ϕi is a new environment state without acception of constration equa-
tion.
Insertion modelling system has found 1 goal trace - all creatures are in other
coast and 10 visited traces - those traces cover all possible behaviors of such
system.
62 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
Typically IMS generated trace is defined by user. It could look like sequance
of actions or environment states etc. For this example, to simplify the view of
the traces we propose to use one uninterpreted action transport:
transport(¬(c = ϕi .F erryman), F erryman, x),
where operation . returns state of the ferryman and ¬ returns other coast.
So, goal state trace has the next view:
init
transport(right, F erryman, Sheg oat)
transport(lef t, F erryman, N il)
transport(right, F erryman, W olf )
transport(lef t, F erryman, Sheg oat)
transport(right, F erryman, Cabbage)
transport(lef t, F erryman, N il)
transport(right, F erryman, Sheg oat)
Fig. 7. Example of Goal State Trace
where init is the initial state and N il means that ferryman is ferried along.
In general case, insertion machine for constraint programming should use:
1. assetion constraints agents action in agent behaviour and initial state.
2. Environment description should have non empty section constraints.
6 Conclusion
The main concepts of insertion modeling system has been considered in the
present paper. The system was successfully used for the development of proto-
types of the tools for industrial VRS (Verification of Requirement Specification)
system and research projects in Glushkov Institute of Cybernetics. Now it is used
for the development of program verification tool and ‘verifiable programming’
project, and for constraint programming. The system continues its enhancement
and new features are added while developing new projects.
The far goal in the developing of IMS consists of getting of sufficiently rich
cognitive architecture to its basis, which could be used in the artificial intelligence
research.
References
1. D.R. Gilbert, A.A. Letichevsky: A universal interpreter for nondeterministic con-
current programming languages.In M. Gabbrielli (eds.), Fifth Compulog network
area meeting on language design and semantic analysis methods (1996).
2. A. Letichevsky and D. Gilbert: A general theory of action languages.Cybernetics
and System Analyses, vol. 1, 16–36 (1998).
Insertion Modeling System And Constraint Programming 63
3. A. Letichevsky and D. Gilbert: A Model for Interaction of Agents and Environ-
ments. In D. Bert, C. Choppy, P. Moses, (eds.). Recent Trends in Algebraic Devel-
opment Techniques. LNCS, vol. 1827, pp.311–328. Springer (1999).
4. A. Letichevsky: Algebra of behavior transformations and its applications. In
V.B.Kudryavtsev and I.G.Rosenberg (eds). Structural theory of Automata, Semi-
groups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and
Chemistry, vol. 207, pp. 241–272. Springer (2005).
5. S. Baranov, C. Jervis, V. Kotlyarov, A. Letichevsky, and T. Weigert: Leveraging
UML to Deliver Correct Telecom Applications. In L. Lavagno, G. Martin, and
B.Selic, (eds.). UML for Real: Design of Embedded Real-Time Systems. Kluwer
Academic Publishers. Amsterdam (2003).
6. A. Letichevsky, J. Kapitonova, A. Letichevsky Jr., V. Volkov, S. Baranov,
V.Kotlyarov, T. Weigert: Basic Protocols, Message Sequence Charts, and the
Verification of Requirements Specifications. Computer Networks, vol. 47, 662–675
(2005).
7. J. Kapitonova, A. Letichevsky, V. Volkov, and T. Weigert: Validation of Embedded
Systems. In R. Zurawski, (eds.). The Embedded Systems Handbook, CRC Press,
Miami (2005).
8. A. Letichevsky, J. Kapitonova, V. Volkov, A. Letichevsky, jr., S. Baranov, V. Kotl-
yarov, and T. Weigert: System Specification with Basic Protocols. Cybernetics and
System Analyses, vol. 4, 479–493 (2005).
9. A. Letichevsky, J. Kapitonova, V. Kotlyarov, A. Letichevsky Jr, N. Nikitchenko, V.
Volkov, and T. Weigert: Insertion modeling in distributed system design. Problems
of Programming, vol. 4, 13–39 (2008).
10. R. Milner: Communication and Concurrency. Prentice Hall (1989).
11. R. Milner: Communicating and Mobile Systems: the Pi Calculus. Cambridge Uni-
versity Press (1999).
12. C.A.R. Hoare: Communicating Sequential Processes. Prentice Hall (1985).
13. Cardelli, L. and A.D. Gordon: Mobile Ambients. In Foundations of Software Science
and Computational Structures, Maurice Nivat (eds.), LNCS vol. 1378, pp. 140–155.
Springer (1998).
14. Y. Gurevich: Evolving Algebras 1993: Lipari Guide. In E. Borger (eds.), Specifica-
tion and Validation Methods, Oxford University Press, pp. 9–36 (1995).
15. C. A. R. Hoare and He Jifeng: Unifying Theories of Programming. Prentice Hall
International Series in Computer Science (1998).
16. J. Meseguer: Conditional rewriting logic as a unified model of concurrency. Theo-
retical Computer Science, 73–155 (1992).
17. A. Letichevsky, J. Kapitonova, V. Volkov, V.Vyshemirsky, A. Letichevsky Jr: In-
sertion programming. Cybernetics and System Analyses, vol. 1, 19–32 (2003).
18. J.V. Kapitonova, A.A. Letichevsky, and S.V. Konozenko: Computations in APS.
Theoretical Computer Science, 145–171 (1993)
19. Insertion Modeling System, http://apsystem.org.ua
20. Dexter Kozen David Harel and Jerzy Tiuryn: Dynamic Logic (2000).
21. C. A. R. Hoare: An axiomatic basis for computer programming. Communications
of the ACM, vol. 12(10), 576–580 (1969).
22. R. W. Floyd: Assigning meanings to programs. Proceedings of the American Math-
ematical Society Symposia on Applied Mathematics, vol. 19, 19–31 (1967).
23. A.A. Letichevsky, J.V. Kapitonova, V.A. Volkov, V.V. Vyshemirsky: Insertion
Modelling. Cybernetics ans System Anilises, vol. 1, 19–23 (2003).
24. F. Rossi, P. van Beek, T. Walsh: Handbook of Constraint Programming. Elsevier
Science Inc., New York, NY, USA (2006).
64 A. Letichevsky, O. Letychevskyi, V. Peschanenko, I. Blynov, D. Klionov
25. R. Bartak: Tutorial on Filtering Techniques in Planning and Scheduling. The En-
glish Lake District, Cumbria, UK (2006).
26. K. Marriott, P. Stuckey: Programming with Constraints: An Introduction. MIT
Press (1998).
27. Farmer, Wolf, Goat and Cabbage Problem, http://wiki.visual-
prolog.com/index.php?title=Farmer, Wolf, Goat and Cabbage.