This paper is devoted to the whole problem of interleaving reduction in modeling of concurrent processes. The main notions of insertional modeling were described. The verification problem in terms of insertional modeling was examined. General algorithm of interleaving reduction in terms of insertional modeling was presented. A static and incremental algorithm of reduction for reachability checking was presented. The proof of correctness of presented algorithm was introduced. The results of experiments of such algorithm application was described.
Usually the multiagent distributed systems are high level non-deterministic. The
nature of this non-determinism is symbolic nature of models and concurrency (choice
of parallel process which should operate at each time of modeling). One of the main
problem of reachability checking in verification is exponential explosion of states
number. Some of the sources of such explosion is the number of parallel processes in
model and their interleaving[
There are two different approaches for modeling: model checking and symbolic
modeling[
A state of environment in symbolic modeling presents some formula in
corresponded theory (first order logic etc) which covers some set of concrete states. A
transition is occurred with a help of predicate transformers (weakest precondition,
strongest postcondition[
This paper continues the work [
The algebra of behaviors is presented in chapter Behavior Algebras, the verification environments, corresponding insertion function, and predicate transformer are considered in chapter Verification Environments. The normal form of behavior is defined in chapter Behaviors Over Basis B. The problem of reachability of the states is described in chapter Verification. The notion of partial unfolding is examined in chapter Partial Unfolding. The optimization of partial unfolding by statically permutable operators is reviewed in chapter Static Permutability Property. The incremental algorithm for reducing of interleaving for transition systems is presented in chapter Main Interleaving Reduction Algorithm. The static algorithm of interleaving reduction is described in chapter Static Interleaving Reduction Algorithm. The statistic of applying of such algorithm to few examples is presented in chapter Examples of Application. 2
One of the main notions of insertion modeling, which is used for describing
algorithm of interleaving reduction is behavior algebra. Behavior algebra [
The algebra of sequential behaviors has operations of prefixing: <action>.<sequential behavior> and one internal operation of nondeterministic choice (()+()), which is associative, commutative, and idempotent operation with neutral element 0. We also consider the constant behavior (successful termination), which is a common element of the algebra of sequential and the algebra of parallel behaviors. The operations of action algebra will be considered later.
The algebra of parallel behaviors has the parallel composition ()||() of sequential behaviors as the main binary operation. It is associative commutative (but is not idempotent) and has the neutral element . It also has the prefixing operation and nondeterministic choice. The algebra of sequential behaviors is implicitly included to the algebra of parallel behaviors by the identity u u | | (parallel composition with one component). Unfolding of parallel composition by interleaving will be considered only after inserting of agents that are formed by parallel composition into the environment.
Verification environments of the form E E(U , P, B) are defined by the following parameters: the set of conditional expressions U, the set of operators P, and the set of basic behaviors B. The set of conditions and the set of operators are used to define actions (it is a union of these two sets). The set of basic behaviors is used to define the behaviors of agents inserted into environment in the way which will be explained later. We also suppose that some logic language (first order or temporal) called basic language is fixed to define the states of environment and checking conditions for verification. The conditional expressions also belong to this language.
The state of environment is represented as E[u] , where E is a statement of basic language and u is a parallel composition of sequential behaviors of agents inserted into environment. We suppose that operators are divided into the set of conditional and unconditional operators. Conditional operator has the form a where is a condition and a is an unconditional operator. Unconditional operator a is identified with conditional operator 1 a . The associative product ()*() and the function pt :U P U (predicate transformer) are defined by the set of actions so that the following identities are valid: pt( , a) pt( a) pt( pt( , a), b) pt( , a *b) ( a) *( b) pt( pt( , a) ,b) * Here and are conditions, a and b are unconditional operators.
Predicate transformer pt is supposed to be monotonic:
pt( , a) pt( , a)
In general case, the pt function is defined by some concrete syntax. An example of
such pair (syntax, pt) can be found in [
Example. The basic language is a first order language. Conditions are formulae over simple attributes - symbols that change their values when a system changes its state. Formally they are considered as function symbols with arity 0. Unconditional operators are assignments (parallel assignments, sequences of assignments, if-thenelse operators, loops with finite number of repetitions, etc.). As usually in this case, pt( (x), (x1 : t1(x), x2 : t2 (x),)) z( (z) (x1 t1(z) x2 t2 (z) )) Actually this is the strongest postcondition for precondition .
Example of conditional operator. Let x be an integer variable, u (x 5) (x : x 1) be an operator, x 3 is statement in basic language, u | | u is a behavior. For this case, U , P {u}, B {u (x 5) (x : x 1)} . The equation u (x 5) (x : x 1) considered here as a basic behavior and it used for definition of agent behavior u | | u . In insertion modeling environment considered as agent with insertion function. So, Insertion function is defined by the following identities and rules of operational semantics.
1. E[u, v] E[u | | v] , u,v are agents with sequential behavior (see sec. 1).
2. E[ .u v] E[v] , if (E ) 0 . these identities are obtained when v=0 or 1. 5. E[ . ] E [ ] , if (E ) 0 .
6. E[a.u v] E[v] , if pt(E, a) 0 .
7. E[a.u] a.pt(E, a)[u | | (a, E)] , if pt(E, a) 0 , (a, E) is a parallel composition of sequential behaviors (it generates some new parallel branches). If (a, E) , then u | | (a, E) u | | u and u remains unchanged.
Nondeterministic choice.
8. E[a.u a.v w] E[a.(u v) w] . The use of left distributivity means that environment considers behavior expressions up to trace equivalence. It also means that a system uses delayed (angelic) choice.
9. E[u ] E[u] E[] . The states E[0] and E[] are called terminal states of the environment. Formally, the states of the form E[0] are equivalent to 0, and states of the form E[] are equivalent to (if E[] E[] is added). But from the point of view of verification it is useful to distinguish syntactically different terminal states.
Parallel behaviors.
10. E[u] E[v] E[u | | w] E[v | | w] . Therefore all identities for conditions and operators can be applied within the parallel composition. A component a1.u1 an.un of parallel composition is called degenerated relative to the state E, if for all operators ai .pt(E, ai ) 0 and for all conditions i it is true that (E i ) 0 . Each component that is degenerated relatively to the state E is equivalent to 0 relatively to this state.
11. E[u] F[v] F[v] , if parallel composition u contains degenerated component relative to E. So all states of environment with degenerated components are equivalent to 0.
12. E[u | | v] E[u | | v] E[v] .
13. E[a1.u1 a2.u2 ] E[a1.u1 | |v] E[a2.u2 | |v] , if all actions ai are different, if ai is a condition then ui is terminal constant, and v does not contain components degenerated relatively to the state E. The state of environment E[u] is called dead lock state, if there are no transitions from this state, but u is not a successful termination. If there is at least one degenerated component in parallel composition, then the corresponding state is a dead lock state. All dead lock states are equivalent to 0, but it is useful to distinguish them as well as terminal constants. The rules (9), (12), and (13) are called unfolding of nondeterministic choice.
14. E[a1.u1 | || | an.un ] in1ai .(| | ai1.ui1 | |ui | | ai1.ui1 | |) , if all components of parallel composition are non-degenerated. This relation is called a full unfolding algorithm for a parallel composition. This is a complete unfolding and the main result of this chapter shows that it is not needed to make the complete unfolding at each step of verification. Let u a1.u1 | || | an.un ,
unfold(u,i) ai .(| | ai1.ui1 | |ui | | ai1.ui1 | |) then identity (14) can be rewritten as 14a. E[a1.u1 | || | an.un ] in1unfold(u,i) .
Environment does not distinguish trace equivalent behaviors and consequently,
bisimilar states of environment are trace equivalent[
E[u] ai E[u] , if u is a parallel composition with non-degenerated components and E[u] is defined by the identity (7). 4
The set of symbols is given for the set B of behavior basis. These symbols are called basic sequential behaviors. The expression of the algebra of sequential behaviors constructed from these symbols and termination constants is called sequential behavior over basis B. Suppose that for each symbol v B an equation of the form v Fv (v1, v2,) is given with sequential behavior over basis B as a right hand side. This equation is called the definition of a basic behavior v. The application of this definition (the substitution of the left hand side by the right hand one) is called the unfolding of this behavior. System of basic behaviors is called non-degenerated if each path in the tree representation of the expression v Fv (v1, v2,) contains at least one operator.
a1.u1 a2.u2 an.un where u1,u2 , are sequential behaviors. If ai is a condition, then ui is a termination constant, n 0 , and all actions are different (not equivalent with respect to the environment E), because of delayed (angelic) choice (see sec. 2).
Each sequential behavior u over non-degenerated basis in a state E[u] can be reduced to a normal form v equivalent to u with respect to E.
Parallel behavior over B is a parallel composition of sequential behaviors over B.
Normal form of parallel behavior is a nondeterministic sum of behaviors of the form a1.u1 a2.u2 , where u1,u2 , are sequential behaviors over B, a1, a2 , are operators or conditions such that if ai is a condition, then ui is a termination constant.
0. Each environment state with non-degenerated system of basic behaviors is a trace equivalent to some normal form. 5
A property of environment state is said to be correct if it does not distinguish equivalent states. A property of environment state is monotonic if E E (E[u]) (E[u]) .
Let S1, S2 be state of the model M . The problem of reachability checking is the answer to the question if a path exists from the state S1 to the state S2 on model M , or not. Usually models are highly non-deterministic. This non-determinism is based on interleaving of parallel processes: a | |b (a;b) (b;a) (here a,b are some processes, “ | | ” is parallel composition, “ ; ” is sequential composition and “+” is nondeterministic composition). From other side this non-determinism could produce additional paths from S1 to S2 and additional states. So, let call interleaving reduction problem an answer to the question how to reduce non-determinism of the model M to find the path from S1 to S2 as quickly as possible.
For a given set of correct and monotonic checked properties, defined on the set of environment states, the set of initial states defines which properties are reachable (not reachable) from the initial states for a finite number of steps or a number of steps bounded by some constant.
It is supposed that the set of properties to be checked contains the property of a state “to be a dead lock” and a property “to be a state of successful termination”.
The simplest verification algorithm is exhaustive unfolding of initial states up to
saturation or depletion of a given number of steps. It uses the following formula of
unfolding: in1 E[unfold(u,i)] . Such algorithm was described in [
Two operators a and a' are called permutable regarding the state of E if E[a *a] E[a*a] and dynamically permutatable regarding the state E (denoted by a Ea ) if E[a *a] E[a*a] 0 . Let E[u] E[a1.u1 | || |an.un ] is a state of the environment.
Let’s select the component nonp(E,ai ) {a j | i j (ai Ea j )} . We obtain: s ai.ui and build punfold(E,u,i) A(i) B(E,i) C(E,i) A(i) ai.(| |ai1.ui1 | |ui | |ai1.ui1 | |) B(E, i) C(E, i) i j(ai ,aj )naonjp(.E(,.s.).| | a j1.u j1 | u| j | | a j1.u j1 | |...)
ak .(...| | ak1.uk1 | | (( p; aw ); uk ) | | ak1.uk1 | |...) ki(ak ,ai )nonp(E,ai )ak Eaw
In the last formula (( p;aw );uk ) uk and p are sequences of compositions of actions (behavior). Function punfold is called partial unfolding of parallel composition. Let’s consider the following algorithm of reachability checking: we need to check the properties on a current state of the environment and each state that is reachable from this in one step. Partial unfolding is used for main function of unfolding states. This algorithm is called partial unfolding algorithm of reachability checking.
In general, the punfold uses the notion of dynamic permutability of operators, but it is not optimal, because it uses 4 times application of function predicate transformer pt for each pair of operators. Using punfold can be optimized by using the concept of static permutability of operators. Algorithm which uses punfold with some optimization is considered in section 6.3.
Theorem 1. If two operators p a, q b are permutable regarding the
states E1 , E2 , E3 then they are permutable regarding
any state [
The sufficient condition of permutability of two operators p a, q b is valid under the following conditions: 1. pt( pt( ,b), a) pt( pt( , a), b) ; 2. pt( pt( ,b), a) 0 ; 3. pt( pt( , a), b) 0 .
Example 1. Let a,b:int and 1[init.(a1.good | |b0.bad b1.good)] is initial state and behavior, where init, a1 , b0 , b1 - operators. Agent’s behavior could be represented by the following list of equations: init ((a b) 1).AndFork, AndFork a1 | | (b0 b1), a1 ((a 1) 1), b0 ((b 0) 1), b1 ((b 1) 1) .
Sufficient condition of permutability for operators a1 , b0 , b1 is performed in this case, but there can be a case in the simulation where the state of the environment includes some formula, which combines predicate memory of various parallel processes (a=b). So, one of the operator will not be applicable, ie a pair of operators will be dynamically permutable regarding this state. Thus, the notion of sufficient conditions of permutability of operators need to be strengthened.
To improve the usage of permutability for this example, we need sat(E ) 1 , otherwise operators will be dynamically permutable regarding state E. Let’s try to obtain a sufficient condition for dynamic permutability of two operators regarding some condition E.
The notion of dynamic permutability of two operators p, q regarding some state E uses a condition:
E[ p *q] E[q * p] 0
So, let E pt( pt( ,b), a) pt( pt( , a), b) 0 and try to apply backward predicate transformer to the state E. We obtain:
pt 1( pt 1(E, ,b), , a) E(q,p) , pt 1( pt(E, , a), ,b) E(p,q) .
E pt( pt( ,b), a) pt( pt( , a), b) 0 then E(q,p) E(p,q) 0 .
Proof.
Let’s assume the contrary that E(q,p) E(p,q) 0 . Since the backward predicate transformer turns back to its possible state transition set, it means that ( E(q,p) ) ( E(p,q) ) . State E(p,q) ( E(q,p) ) specifies a set of concrete states from which transitions from state with operators p and q (q and p) exist, which means that E(p,q) E(q,p) E(p,q) E(q,p) 0 . So, we got a contradiction, because if E(q,p) E(p,q) 0 then E 0 . The theorem is proved.
This condition means that if two operators were dynamically permutable regarding E then it is necessary that current state of the environment should satisfy theorem 2.
Let E be some state of environment.
Theorem 3. If two operators p a, q b satisfy the sufficient condition of permutability and E E(q,p) E(p,q) 0 then E[ p *q] E[q * p] 0 .
E[ p *q] E[( a) *( b)] pt(E , a)[ b] pt( pt(E ,b), a) pt( pt(E ( ), b), a) pt( pt(E E , a), b) pt( pt(E ), a) pt(E ), a), b) pt( pt(E ), a), b) pt( pt(E ), a), b)
Next, let’s consider in details the sufficient condition permutability of operators that satisfies the operators p, q:
E[ p *q] E[( a) *( b)] pt(E , a)[ b] pt( pt(E , a), b) pt( pt(E ( ), a), b) pt( pt( E, a) pt( E, a), b) 0
Let’s consider the E[ p *q] E[q * p] 0 .
condition of dynamic permutability regarding
E: pt( pt( E, b), a) pt( pt( E, b), a) 0 pt( pt( E, a), b) 0 pt( pt( E, a), b) 0 Equality E[ p * q] E[q * p] shall be satisfied because otherwise the operators p, q do not satisfy the sufficient condition permutability of operators (Theorem 1). Thus, we have: pt( pt(E ), a), b) pt( pt(E ), a), b) pt( pt(E , b), a) pt( pt(E , b), a) pt( pt(E ), a), b) pt( pt(E , b), a) Let’s consider opposite:
pt( pt(E ), a),b) pt( pt(E ,b), a) 0 Let’s continue to consider sufficient conditions of permutability: pt( pt( , b), a) pt( pt( , a), b) 0 pt( pt( (E E), b), a) pt( pt( (E E), a), b) 0 pt( pt( E E), b), a) pt( pt( E E), a), b) 0 pt( pt( E), b), a) pt( pt( E), b), a) pt( pt( E), a), b) pt( pt( E), a), b) 0 pt( pt( E), b), a) pt( pt( E), a), b) 0
This means that the condition E E(q, p) E(p,q) 0 should be satisfied. But we have the following condition E E (q, p) E(p,q) 0 . Thus, both conditions must be satisfied, however:
E E(q, p) E(p,q) E E(q, p) E(p,q) 0 So we got a contradiction. The theorem is proved.
If there are two operators p a, q b that satisfy the sufficient condition of permutability. Condition
E E(q, p) E(p,q) 0 is called sufficient condition of dynamic permutability of operators p, q regarding the environment E.
From a practical point of view, let’s try to identify requirements for operators with which we can determine statistically whether they satisfy the sufficient condition of dynamic permutability or not.
Let E be a state of the environment, and p - an operator. The set A(E) is called the
set of all attributes from state E and A(p) is called the set of all attributes in the
statement p[
Two operators p a, q b are called statically permutable if they satisfy the following conditions:
A( p) A(q) pt( , a) 0 pt( ,b) 0
Theorem 4. If two operators p a, q b are statically permutable then they are dynamically permutable.
Proof.
To prove the theorem we need to show that these operators satisfy necessary condition of permutability of operators in this case. Since A( p) A(q) pt( ,a) 0 pt( ,b) 0 and theorem 1 then pt( pt( , a), b) pt( pt( , a), b) 0 pt( pt( ,b), a) pt( pt( ,b)) 0 pt( pt( ,b), a) pt( pt( , a), b) pt( pt( ,b), a) pt( pt( , a), b) pt( pt( ,b), a) pt( pt( , a), b) pt( , a) pt( ,b) pt( , a) pt( ,b) The theorem is proved.
This theorem means that if a predicate that combines memory in a state of environment with different operators is absent then checking the necessary condition of dynamic permutability is not required. Since in this case a usage of one of these operators does not affect the applicability of another operator. The appearance and disappearance of such predicates can be defined statically and syntactically.
Thus, in Example 1 operators are statically permutable, but after applying init operator formula will contain predicate that combines memory of operators a1 , b0 and a1 , b1 . So, we have to use sufficient condition for dynamic permutability of pairs of operators, a1 , b0 and a1 , b1 regarding the state of the environment after application of init operator . So, E (a b) . Let’s statically compute sufficient condition of permutability of operators: (a1,bo ) : E(a1,b0 ) E
(b0 ,a1) (a 1) (b 0) (a1,b1) : E(a1,b1) E(b1,a1) (a 1) (b 1)
Next let’s try to apply sufficient condition of dynamic permutability of operators regarding the condition E for both pairs of operators: (a1,bo ) : E E(a1,b0 ) E
(b0 ,a1) (a b) (a 1) (b 0) 0 (a1,b1) : E E(a1,b1) E(b1,a1) (a b) (a 1) (b 1) 0
Thus, operators (a1,bo ) will be dynamically permutable regarding the condition E, and operators (a1, b1) will be dynamically permutable. This means that interleaving will be removed in correct way for this problem. 6.2.
The approach proposed in the previous sections can be applied to the problem of finding deadlocks in a given model, but if the user specifies a state of environment you want to check coverage, whereas previously proposed approach should be strengthened.
Example 2. Let a,b:int and 1[init.(a1 | |b1)] be initial behavior and a state of the environment, where init, a1 , b1 - operators. Agent’s behavior could be represented by the following list of equations: init ((a 0) (b 0) 1), AndFork, AndFork a1 | |b1, a1 (1 (a : 1)), b1 (1 (b : 1)) Let’s check recheability of the state F (a 0) (b 1) .
After applying the operator init obtains the state of the environment E (a 0) (b 0) . Operators a1 , b1 are statically permutable and can be applied to the state E, which means that they are dynamically permutable regarding E. So, E[a1 | |b1] E[a1.b1] , which means that the operator b1 never will be applied before the operator a1 and user defined state F will be unreachable after interleaving reduction. Let’s try to enhance sufficient condition of operators permutability regarding some state E with some conditions related to formula F. F (E[a1 *b1]) F (E[b1 *a1]) 0 for this example then we consider conditions for operators separately (not for pairs of operators).
Let p a be an operator.
Theorem 5. If pt1( pt( , a), , a) 0 then pt( , a) 0 .
Let’s consider the opposite pt 1( pt( , a), , a) 0 and pt( , a) 0 . In this case by performed substitution it can be easily obtained the following: pt 1( pt( , a), , a) 0 pt 1(0, , a) 0 0 0 So we got a contradiction. The theorem is proved.
The operator p a is called permutable regarding some user defined state F, if the following conditions are satisfied: 1) pt 1( pt( , a), , a) 0 ; 2) F pt1( pt( , a), , a) F pt( ,b) .
This permutability means that an operator does not change the state of the environment in order to reach the user defined state changed. From reachability point of view we are interested in two cases (if pt 1( pt( , a), , a) 0 ): 1) F pt1( pt( , a), , a) 0 F pt( ,b) 0 ; 2) F pt1( pt( , a), , a) 0 F pt( ,b) 0 .
In first case, the reachability of user defined state should be checked immediately before application of an operator, and in the second case - after.
If operators satisfy the sufficient condition of dynamic permutability, but at least one of them is not permutable regarding a user defined state then this operator should be applied first.
This approach can be applied to any algorithm of unfolding.
So, for checking of reachability of the user defined state F the notion of permutability regarding the user defined state could be used. You can’t consider a pair of operators if both of them do not satisfy this condition.
Coming back to example 2. Operator a1 will not be permutable regarding the user defined state F: 1 pt 1( pt(1, a : 1),1, a : 1) 1 E1 pt(1, a : 1) (a 1) E2 F E1 F E2 (a 0) (b 1) 1 (a 0) (b 1) (a 1) 0 Operator b1 is permutable regarding F: 1 pt 1 ( pt(1,b : 1),1,b : 1) 1 E1 pt(1,b : 1) (b 1) E2 F E1 F E2 (a 0) (b 1) 1 (a 0) (b 1) (b 1) 1 From other side operators a1 , b1 are statically E (a 0) (b 0) has no predicates that combine memory of these operators. permutable since
This means that in this case you should first apply an operator b1 , then you need to check reachability of F (since F E1 (a 0) (b 1) 1 0 ) before applying a1 . And after that you can try to apply a1 . So, pt((a 0) (b 0), b : 1) (a 0) (b 1) Then let’s check the reachability of user defined state: (a 0) (b 1) (a 0) (b 1) 1
So, reachability of user defined state is proved. 6.3.
Let E[u] be a model (an initial state of the environment and behavior), where u is behavior, and F is some user defined state which reachability should be checked. So, we need to check reachability of F in the model E[u] and all its deadlocks.
The main interleaving reduction algorithm for reachability checking is represented in fig. 1.
Static Analyses. In the initial behavior u we look for set Opn (set of operators of a n-th parallel process) on each parallel process. Next, for each pair of operators from different parallel processes we build a table: H : N OpN N OpN G Bool . This table by a pair (parallel process identifier and operator) returns four (number of parallel process that is not equal to the previous one, and the operator which is permutable to current one, the last two parameters are sufficient condition for permutability of operators and flag for static permutability of operators).
For each pair of operators that does not satisfy the sufficient condition of permutability of operators the table is filled: D : N OpN {N,OpN } , where {N,OpN } is a set of pairs: the number of parallel process and an operator, which does not satisfy the sufficient condition of permutability.
Each operator is constructed Flt : OpN Bool Bool Bool , which defines the triple for each operator in set: value of reachability of user defined state before and after application of an operator, the third value is 1 if all operators from other processes are statically permutable with this one, and 0 if not.
Checking Reachability. Checking reachability of user defined state F. If the filter is reachable then saving corresponded trace and stop modeling.
Choosing Component. We build normal form (section 4). From list of components we should choose one to continue working. Here we propose to select first component from the list, but in general case here some heuristics could be applied (it’s out of scope of this paper). If there is no component left then finishing.
Choosing Operator. In a chosen component we select operators in the following order. First we check the applicability of operators for which the third option from the table Fpl is 1. If there are no operators or they can’t be applied, then we choose other operators. If the flag state of the reachability of user defined state is 1 then we first try to apply such operators that are permutable regarding a user defined condition for both operators in the table Flt being 1. If the flag state of user defined state equals 0 then we choose to consider operators whose value pairs in the table Flt are (0,1). If one of such operators is applicable then after his application we need to check the reachability of user defined state. If user defined state is reachable then finishing. If no such operators left then deadlock is obtained and we get new component. Otherwise, finishing.
Cycle/Visited. Checking cycle/visited filters. If the filter is reachable then we choose a next operator to work. If no operator left then we choose other component.
Partial Unfolding. We try to build B and C if it is required, using notion of
sufficient condition of static and dynamic permutability. If the last operators satisfy
the sufficient condition of static (dynamic) permutability then B=0. Starting delayed
to build C. In general, this problem is formulated as follows. It is given: current state
of environment E, operator a one of the parallel processes u1 (other processes are
delayed to use some operators in this process, including the process by which it was
taken the operator a), and delayed parallel processes. In the set of parallel processes it
is needed to find the operator b, which does not satisfy the sufficient condition of
permutability (table D) or does not satisfy the condition of sufficient dynamic
permutability regarding the E. In order to check whether these operators are in a given
process, you generally build all states space. If these operators are not found then all
resulting state of the search should be removed from storage cycle/visited filters. This
is necessary because subtrace which leads to the required operator can modify the
current state of the environment and a sufficient condition for dynamic permutability
can not be performed, although for state E a sufficient condition for dynamic
permutability is performed. But in some cases the search for these operators do not
need to spend a dynamically performance of all subtrace. If the state of the
environment does not contain predicates that combine memory of these operators and
the set of attributes operators intersect, then we can use the concept of
specialization[
For trace equivalence each trace for deadlock should be checked additionally because of used normal form. Each cycle/visited trace should be checked for reachability of user defined state in the following way: turning back with a help of backward predicate transformer until operator doesn’t have value 1 as first and second parameters in the table Flt.
Theorem 6. punfold(E,u,i) Function which was represented in fig. 1 saves property of reachability checking.
Proof.
Let’s suppose opposite that the function punfold(E,u,i) does not save the property of reachability checking. This means that for some state of environment E such operator a exists, which is applied to the E( E a E ) and doesn’t exist as first action in components A(i), B(E,i), C(E,i) . So, the operator will be dynamically permutable regarding the environment E and all other operators resulting behavior components A(i), B(E,i), C(E,i) (according to Choosing Operator, Partial Unfolding). In addition, operator a can be applied after the application of the first operators in the resulting behavior of components A(i), B(E,i), C(E,i) .
This means that the required state of the environment is reachable, but after applying the operator a on the next step these operators are dynamically permutable regarding the environment E. From other point of view we do not take into account E . If value of pair for the operator in the table Flt is (0,1) then according to step 5 we have to take it into consideration and in this case it will be the first operator in the behavior of components A(i), B(E,i),C(E,i) . If the value of such pair is (1,1) then the state of the environment is reachable in the next step, as defined Flt. If the value is (1,0) then before application of the operator a we need to check the reachability of the environment E and definitions in Flt. If the value is (0,0) then required state is not reached in E . That means that the required state of the environment is not unreached at all states of the environment as a result of unfolding application punfold(E,u,i) . So we got contradiction. The theorem is proved.
The main problem of proposed algorithm is complicity to find component C(E,i) . One of the ways to speed up such algorithm is delayed computation. The idea of this method contains the following: 1) To collect all such special states from Partial Unfolding, where we should find component C(E,i) and finding the required states with a help of different methods: all states coverage, invariants etc. 2) To continue algorithm with built states of component C(E,i) .
Such algorithm is called incremental algorithm of reachability checking.
If operators and initial environment state of model do not contain predicates which connected to the memory of different parallel processes then general algorithm in previous section could be simplified. Such algorithm is called static interleaving reduction algorithm.
For the component C(E,i) of punfold(E,u,i) we should check reachability of application of operator which is not dynamically permutable for ai (see section 5). For elimination of such reachability checking we could build additional interleaving according to checking of reachability of corresponded operator in behavior. For example, let a | |b.c | | d and (a c) (b d) , E be some environment state. So, punfold(E,a | |b.c | |d,1) E[a.(b.c) | |d] E[b.c.(a | |d)] E[d.(a | |b.c)] Here we take into account b.c.(a | | d ) , because (a c) ; d.(a | |b.c) , because we have taken b.c.(a | | d ) and (b d ) . 6.5.
In Table 1 information about few big examples run with our static interleaving reduction algorithm are presented. All of them give out of memory error (PC with 8 Gb of RAM) if we try to obtain all states space. So, we try to run them on implementation of proposed algorithm in Insertion Modeling System.
Described algorithm of interleaving reduction was implemented in Insertional Modeling System. Its restriction for usage of static permutability condition was good account in set of big examples. In any case, the main interleaving reduction algorithm depends on reachability checking problem (component C(E,i) , section 6). Notoriously this problem is algorithmically unsolvable. It means that you could always prepare example where interleaving reduction will be impossible (for example, all operators will be non-permutable etc).