The paper relates to practical aspects of insertion modeling. 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 programming' project.
Insertion modeling is the approach to modeling complex distributed systems
based on the theory of interaction of agents and environments [
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 [
Another source of ideas for insertion modeling is the search of universal
programming paradigms such as Gurevich’s ASM [
To implement the insertion model in IMS one must develop insertion machine with easily extensible input language, the rules to compute insertion functions and a program of interpretation and analyzing of insertion models. The architecture, input languages and examples of insertion machines and insertion modeling system are considered in the paper. 2
Insertion modeling system is an environment for the development of insertion
machines and performing experiments with them. The notion of insertion
machine was first introduced in [
Insertion model of a system represent this system as a composition of environment 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 environment 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
environment 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 [
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(E0) ∧ beh(u) = beh(u0) ⇒ beh(E[u]) = beh(E0[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 [
The general architecture of insertion machine is represented on the fig. 1.
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 environment, interacting with it in the real or virtual time. Analytical machines 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 exactly one alternative and perform the action specified as a prefix of this alternative. 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 behavior 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 information 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 different 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 environment 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 insertion 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.
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: <behavior>::= Delta | bot | 0 | < action > | <action> . <behavior> | <behavior> + <behavior>| <environment state>[<list of named agent behaviors separated by ,>]| <functional expression> <named agent behavior>::=<agent name>:<behavior>
Therefore, the language of behavior algebra (termination constants, prefixing and nondeterministic choice) is extended by functionals expressions and explicit 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 comments.
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 multisorted (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 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 symbols 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 insertion. 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 actions 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.
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 u →au0
u=u+ε
The function seq is a function from IMS library that defines the sequential composition of behaviors: (u; v) = X a.(u0; v) +
X (ε; v), (0; v) = 0, (Δ; v) = v, (⊥; v) = ⊥ The function unfold reduces the behavior expression to normal form P ai.ui +ε. This insertion machine generates a word cnam with nondeterministically chosen 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 cnan.
An example of sequential (not strong) insertion is shown on fig. 4.
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: synchr(x, y) =
X (a × b).(x0, y0),
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]) ) lmrg(x, y) = X a. (x0 k y) , delta(x, y) =
X ε k μ x →aa0 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 indecomposable 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 [
E →a E0, α : u →b β : u0 E[α : u] →c E0[β : u0] , P (E, a, α, b, β, c), 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 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
E →a E0, u →b β : u0
E [u] →c E0[u0] , P (E, a, c), 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 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
bioinformatics [
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,
Constraint 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 [
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 Constraint programming (were search is implicit in language itself); – 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
combinatorial 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
cooperation with the user. Many decisions can be encoded in mathematical formulae,
which appear as rules and which are handled by the internal solvers, so
(although, of course, not always) there is no need to program explicit decision
trees [
Among the applications with these characteristics, the following may be cited: planning, scheduling, resource allocation, logistics, circuit design and verification, finite state machines, financial decision making, transportation, spatial databases, etc. 5
Some example of insertion machines and restrictions for insertion function are
in [
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.
ϕ [p] −f−e−rr−y−→x ϕi [p] , constraints(ϕ) = 1 ϕ [p] −a−s−s−et−io−n−c−o−n−st−r−ai−n−t→s 0, constraints(ϕ) = 0 ϕ [p] −f−e−rr−y−→x 0, constraints(ϕi) = 0 ∨ ¬constraints(ϕ) = 1 ϕ [p] −a−s−s−et−io−n−c−o−n−st−r−ai−n−t→s ϕ [p] , ¬constraints(ϕ) = 0 Fig. 6. Relations of System’s Transitions
where ϕi is a new environment state without acception of constration equation.
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. 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, Shegoat) transport(lef t, F erryman, N il) transport(right, F erryman, W olf ) transport(lef t, F erryman, Shegoat) transport(right, F erryman, Cabbage) transport(lef t, F erryman, N il) transport(right, F erryman, Shegoat) 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
The main concepts of insertion modeling system has been considered in the present paper. The system was successfully used for the development of prototypes 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.