Alan Mishchenko
email: alanmi@eecs.berkeley.edu

Robert Brayton
email: brayton@eecs.berkeley.edu

Roland Jiang
email: jiejiang@eecs.berkeley.edu

Tiziano Villa
email: villa@uniud.it

Nina Yevtushenko
email: ninayevtushenko@yahoo.com

Efficient Solution of Language Equations Using Partitioned Representations

A class of discrete event synthesis problems can be reduced to solving language equations F X S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs when the automata for F and S are prefix closed, and are naturally represented by multi-level networks with latches. For this special case, we present an efficient computation, using partitioned representations, of the most general prefix-closed solution of the above class of language equations. The transition and the output relations of the FSMs for F and S in their partitioned form are represented by the sets of output and next state functions of the corresponding networks. Experimentally, we show that using partitioned representations is much faster than using monolithic representations, as well as applicable to larger problem instances.

Introduction

Many important synthesis problems can be formulated in terms of solving language equations. The unknown X represents an unknown component in a known network of components, which together must satisfy a given external specification. Examples are FSM synthesis, game solving, protocol conversion, discrete control, testing, etc. The solving for X is typically very hard, involving operations that are exponential in complexity.

In many cases, hard computational problems can be reformulated using decomposition and partitioning, which lead to computational advantages. A good example is image computation [3], which is a core computation in formal verification. In its simplest form, the image of a set of states is computed using the formula: ,

Img( ) [ ( , , ) ( )],

i cs

ns T i cs ns cs

where T(i, cs, ns) is the transition relation, (cs) is the set of current states, i is the set of input variables, and cs (ns) is the set of current (next) state variables. The image, Img(ns), is the set of states reachable in one transition under all possible inputs from the current states, (cs), using the state transition structure given by T(i, cs, ns). [START_REF] Yevtushenko | Sequential synthesis by language equation solving[END_REF] When the state transition structure is given by a sequential network, the transition relation can be represented, for example, in partitioned form using a set of next state functions, {T k (i, cs)}, which update the state of each latch2 . The partition, {T k (i, cs, ns k )}, represents how the next state of each latch, ns k , depends on the values of inputs, i, and the current state, cs, of all latches:

T k (i, cs, ns k ) = [ns k T k (i, cs)]
The complete transition relations can be derived as the product of the next state functions as follows:

T(i, cs, ns) = k T k (i, cs,ns k ) = k [ ns k T k (i, cs) ]
We call T(i, cs, ns) the monolithic representation of the transition relation and contrast it with the representation in terms of the partition, {T k (i, cs, ns k )}. Many problems can be solved using a partitioned representation without ever resorting to monolithic one, which may be impossible for larger problems. For example, the image computation can be performed using the partitioned representation by scheduling those cs variables, which do not appear in some parts, to be quantified earlier [4] [5]. In practice, this approach to image computation leads to significantly smaller intermediate BDDs, and has been responsible for dramatic increases, both in efficiency and in the sizes of problems that formal verification can solve.

The contribution of this paper is in proposing a way to use the partitioned representation for solving language equations of the type F X S, for the case when the automata for F and S are prefix closed and represented by multi-level sequential networks. [START_REF] Touati | Implicit state enumeration of finite state machines using BDDs[END_REF] We show how the partitioned representation can be used to perform the basic operations of language equation solving: completing, complementing, determinizing, hiding, and computing the product of finite automata. [START_REF] Ranjan | Efficient BDD algorithms for FSM synthesis and verification[END_REF] An important aspect is that we show how most of these operations can be reformulated in terms of image computations, and hence can take advantage of the efficient developments in this area.

Section 2 gives the details of the problem statement for the specific case when the partitioned representation can be used. Section 3 outlines the computational procedures. Section 4 lists experimental results. Section 5 concludes. In the appendix, we prove that the determinization and completion operations commute, which makes the computations more efficient.

Problem Statement

Given a sequential network and its specification, it is theoretically possible to compute the Complete Sequential Flexibility (CSF) for a sub-part. The CSF represents all possible legitimate sequential FSM behaviors. They are legitimate in the sense that each can be implemented in a circuit and used to replace the selected sub-part, resulting in another network that satisfies the specification [START_REF] Chauhan | Non-linear quantification scheduling in image computation[END_REF] . The initial research on capturing the maximum set of sequential behaviors was developed in [9].

It can be shown [1] that the CSF, X, can be computed from the most general solution of the language equation, F X S, where F is the behavior of network without the selected part, X, and S is the behavior of the original network as a whole or an external specification. The CSF is the largest prefix-closed, input-progressive automaton contained in X (and thus an FSM).

The interaction of F and X within the specification S is shown in Figure 1. [START_REF]UC Berkeley[END_REF] The external input and output variables are represented by symbols i and o, respectively. The internal variables that are the inputs and outputs of X are represented by symbols u and v, respectively. Note that in Figure 1 and in the formulas below we do not distinguish between the sets of symbols used to construct the input/output languages of F, X, and S, and the sets of variables i, u, v, and o, used to encode these symbols.

The most general (the largest) solution of the language equation is the following [1]: [ ( ,,,) ( ( ,) ]

X = , , )
u v u v F i v u o S i o (1)
where symbol denotes the composition of languages (the direct product of automata), the horizontal bars denote the complementation of a language (automaton), and the symbols denote the expansion and restriction, respectively, of a language to a set of symbols. Expansion causes the insertion of the listed symbols into the language, while restriction leads to "hiding" the unlisted symbols on the inputs or arcs of the automaton.

Figure 1.

A topology showing the interaction of components F and X in the language solving problem.

We assume that the behaviors of the components F and S are represented by multi-level sequential networks, similar to the one in Figure 2. The external variables of such networks are the primary inputs (i), the primary outputs (o), and the latches having the current state (cs) and next state (ns) variables. We assume that the latch nextstate functions, {T k (i, cs)}, and the primary-output functions, {O j (i, cs)}, can be computed and stored as BDDs in terms of the primary inputs and the current state variables.

The automata for F and S are derived, from the multi-level networks representing them, simply by taking the set of inputs of these automata as the union of the sets of inputs and outputs of the corresponding network. In the sequel, we use the terms "inputs" and "outputs" meaning the inputs and outputs of the network. All reachable states of a network are the accepting states of the Example. Figure 3 shows a sequential circuit and its corresponding automaton. The circuit has input i, output o, and two latches, with current state variables cs = {cs 1 , cs 2 } and next state variables ns = {ns 1 , ns 2 }. The initial state of the latches is (00). The next state functions of the latches are T 1 (i, cs) = i & cs 2 and T 2 (i, cs) = i + cs 1 .

The two parts of the transition relation are

T 1 (i, cs, ns 1 ) = [ns 1 T 1 (i, cs)] = [ns 1 i & cs 2 ] = ns 1 & i & cs 2 + 1 ns &( i + 2 cs ) T 2 (i, cs, ns 2 ) = [ns 2 T 2 (i, cs)] = [ns 2 ( i + cs 1 )] = ns 2 & ( i + cs 1 ) + 2 ns & i & 1 cs ).
The single output relation is The states of the automaton in Figure 3 are labeled with the latch values (cs 1 ,cs 2 ). Transitions (arcs) are labeled with (i,o) values. Thus, the transition from state (00) under input 0 is to state (01). The output produced by the network in this case is 0. So the label of this transition is 00 (equal to 0/0 using conventional FSM labeling). This automaton is not complete. Thus, the transition from (00) under input (11) is not defined. The unshaded states are accepting. The additional (shaded) state (DC), added for completion, is not accepting. DC has a universal self-loop and all transitions that were originally undefined (e.g. from (00) under input (11)) are directed to DC.

Monolithic Representation of Relations. The monolithic representations of the transition and output relations of the automaton can be obtained from the next-state and output functions:

T(i, cs, ns) = k [ ns k T k (i, cs) ], O(i, cs, o) = k [ o k O k (i, cs) ].
The monolithic representation of the complete transition-output relation of the automaton is:

TO(i, o, cs, ns) = T(i, cs, ns) & O(i, cs, o).

TO specifies what the next state is for each current state and each input/output combination. A relation is not well-defined if there exists some input/output/current-state combination for which the behavior of the automaton is not specified, i.e. the automaton is incomplete.

As an example of the use of the monolithic representation TO, consider the operation of completion of an incomplete automaton. The transition-output relation of the completed automaton is '( , , , )

, TO I o cs ns TO i o cs ns A i o cs DC ns DC cs DC ns

where A(i,o,cs) = ( , , , ) ns TO i o cs ns is the sub-domain of input/output/current-state variables for which the original automaton is not defined, and DC is the code (in terms of latch variables) of the "don't-care" state added during completion. Note that we cannot use the code of an unreachable state to represent the DC because the unreachable states have next states. To encode the DC we need to add an additional state variable.

Thus the resulting relation is derived from the original one by simply directing all undefined transitions to DC and then adding a universal self-loop to DC.

Partitioned Representation of Relations. The disadvantage of monolithic representations is that they include all variables and hence their BDDs may be huge. Even if these can be computed, the operations, such as completion, product, determinization, become very inefficient if not impossible to complete. If the set of reachable states is much smaller than the set of all states, re-encoding the monolithic relations using fewer state bits may alleviate this problem. However, re-encoding can be very slow and our experience indicates that this tends to increase the BDD sizes of the relations.

In this paper, we show how partitioned representations can be used, both in making computations more efficient and in allowing larger problems to be solved. The monolithic transition and output relations are never constructed. With a partitioned representation, the functionalities of the automata are represented as sets of functions, {T k (i, cs)} and {O k (i, cs)}. All Boolean operations are performed using these functions. It will be shown that image computation plays the key role in the manipulations involving partitioned representations, and hence a decade of research resulting in techniques to speed up image computations [4] [5][8] can be used. 7

Computation Algorithms

This section describes how to perform operations on the automata, required for language equation solving, when the partitioned representations are available. First, we present the main algorithm for the computation using either monolithic or partitioned representations. Later we show that, given the partitioned representations, all the steps are essentially embedded into a modified determinization procedure, so that there is no need to compute the completion and variable hiding operations as separate steps. However, in Section 3.2 for generality we show how these operations can be performed independently of determinization. [START_REF] Somenzi | BDD package "CUDD v. 2.3.0[END_REF] Space constraints prohibit describing all these advancements; we experimented extensively with implmenting most of proposed techniques and chose the methods that we observed to be most efficient.

Main Algorithm

The main generic algorithm (shown below) first derives the most general solution from the equation X =

S F

, followed by an additional prefix-closed and progressive operation on the solution X, to make it an FSM. Later, we show how to make the computations more efficient.

Algorithm: LanguageEquationSolving Input: prefix closed S(i,o) and F(i,v,u,o) Output: most general prefix closed solution X begin 01 X:=Complete(S) 02 X:=Determinize(X) 03 X:=Complement(X) 04 X:=Support(X,(i,v,u,o)) 05 X:=Product(Complete(F),X) 06 X:=Support(X,(u,v)) 07 X:=Determinize(X) 08 X:=Complete(X) 09 X:=Complement(X) 10 X:=PrefixClose(X) 11 X:=Progressive(X,u) 12 return X end Algorithm 1: Generic Algorithm for computing the most general prefix-closed progressive solution.

Support (used for both expansion and restriction) changes its argument automaton to have the support of the given list of variables.

Complete adds one additional non-accepting state with a universal self-loop, and causes all undefined inputs to transition to it.

PrefixClose removes all non-accepting states. Progressive recursively removes those states that are not completely specified in terms of the input variables, u, of X (i.e. not input-progressive). The other operations are self-explanatory.

Elementary Operations using Partitioned Representations

In the application to the problem where the topology is as shown in Figure 1, we have partitions for F (which has both u and o as outputs):

1 1 1 { ( , , , )},{ ( , , , )},{ ( , , , )} F F j j j j j j T i v cs ns U i v cs u O i v cs o ,
and those for S:

2 2
{ ( , , )},{ ( , , )}.

S S j j j j T i cs ns O i cs o

Completion. An automaton derived from an FSM is completed by interpreting the complement of its output relation as the condition for a transition from the current state to the non-accepting DC state. The complement of the output relation, ( , , ) O i o cs , gives, for each current state, cs, all the input/output combinations, for which the automaton's behavior is not defined, since an FSM is defined for all its input combinations. When the partitioned representation is used, there is no need to construct the monolithic representation of O(i,o,cs). For any current state, given by its characteristic function (cs), its undefined input/output combinations, Q(i,o), can be found by an image computation followed by complementation:

Q(i,o) = ) ( & ) , , ( cs cs o i O cs .
This image can be efficiently computed using the partitioned representation of the output relation:

Q(i,o) = [ (, )]& ( ) cs j j o O i cs cs .
Complementation (deterministic case). In the general case of non-deterministic automata, determinization (subset construction) is required before complementation. In contrast, a deterministic automaton is easily complemented by interchanging the sets of its accepting and non-accepting states. Thus computing S , which is deterministic, is easy.

When an automaton is derived from a deterministic multi-level network, its set of accepting states is equal to the set of reachable states of the network. The DC state introduced during completion is the only non-accepting state. In this case, complementation is performed by changing the interpretation of the DC state: it becomes the only accepting state, while all other states become non-accepting.

Product computation. The product of two automata is defined when they have the same support. In the partitioned view, having the same support simply means that each function is considered as a function of the full set of variables. When the argument automata are represented in their partitioned forms,

T i v cs ns T i cs ns

, the partitioned representation of the product automaton, is simply the union of the two partitions, i.e.

1 1 1 2 2 2 ( , , , ) { ( , , , ), ( , , )} j
j k k

T i v cs ns T i v cs ns T i cs ns

.

The fact that some variables, for example, u and o, are missing, means that the relations are independent of these variables.

Hiding variables. Hiding variables i and o in the automaton

representing the product of F and S is an operation which changes the support automaton. In the monolithic form, it is performed by existentially quantifying the variables, not in the support, from the transition-output relation TO of the product automaton:

TO (v,u,cs,ns) = i,o [ TO(i,v,u,o,cs,ns) ].
This operation usually leads to a non-deterministic automaton, even if the original automaton is deterministic. Hiding variables cannot be performed on the partitioned representation because the operations of existential quantification and product do not commute. For example, it is not possible to quantify the input variables i from the transition relation by quantifying them independently from each partition:

i T(i,cs,ns) = i j [ ns j T j (i,cs)] j i [ ns j T j (i,cs) ]. Thus hiding can't be done by acting on the partitions independently. However, a key observation is that the hiding operation can be built into the next step, the determinization procedure, in such a way that there is no need to derive the monolithic transition relation and then apply hiding to it.

Determinization (Subset Construction).

Determinization is performed by enumerating explicitly the subsets of states of a nondeterministic automaton, which are reachable from the initial subset state (which contains only the initial state). The basic step is the computation of the subset of states, reachable under various assignments of (u,v) from a given subset of states, (cs). Denote by P (u,v,ns) the sets of states (the subset states) reachable from (cs) under various combinations of (u,v). Using the monolithic representation, with variable i hidden, the computation would be: ( , , ) ( , , , ) ( , , , ) ( )

cs i P u v ns U i v cs u T i v cs ns cs .
The computation of P using the partitioned form is:

, ( , , ) [ ( , , )] [ ( , , )] ( ) i cs j j j k k k P u v ns u U i v

cs ns T i v cs cs

Thus, the computation of P (u,v,ns) can be seen as the computation of the image of (cs), under the transition relation U(i,v,cs,u)T(i,v,cs) represented in its partitioned form: {U j (i,v,cs)}, {T k (i,v,cs)}, where hiding (quantification) of variables i is performed as part of the image computation.

Let C j (i,v,cs) denote the condition that is true when the j-th output of F conforms to the j-th output of S:

1 2 ( , , ) [ ( , , ) ( , )] F S j j k j k k C i v cs O i v cs O i cs ,
where cs = (cs 1 ,cs 2 ) and the iteration is over all values k of the output O j , e.g. for binary signals,

{0,1}. k Let ( , , ) ( , , ) j j
C i v cs C i v cs , which is the overall condition when all outputs of F conform to the outputs of S:

F S jk jk j k C i v cs O i v cs O i cs . 1 2 ( , , ) [ ( , , ) ( , )]
Next, we compute ( , ) Q u v , the condition when the current subset of states (cs) leads to the non-conformance of outputs of F and S:

, 1 ( , ) [ ( , , , ) ( , , ) ( )]
i cs Q u v U i v cs u C i v cs cs .
Since these combinations of (u,v) can lead to a non-conforming state, we exclude such transitions and map them all into a single nonaccpeting state DCN with a universal self loop. We remove these combinations from consideration by restricting P (u,v,ns) to those (u,v) that are not contained in ( , )

Q u v : ( , , ) ( , , )& ( , ) P u v ns P u v ns Q u v
Finally, the result is made complete by adding a state DCA (which is accepting in the final answer after complementation), with transitions from ( ) cs into it for all (u,v), which are not contained in ( , ) Q u v .

Note that ( , , )

C i v cs can be represented as the sum of output nonconformance conditions for each output. Therefore, the computation of ( , ) Q u v can be done one output at a time, without computing the monolithic relation for C(i,v,cs).

Validity of the computation. The maximum prefix-closed solution (required for an FSM implementation) is computed after determinization and completion, when the set of reachable subset states, { (cs)}, are known and, for each of these, the function ( , ) Q u v has been computed, which defines the transitions from this subset state into a newly added non-accepting state DCA.

To perform the complementation, which is the last step in computing the maximum solution, the accepting and non-accepting states are switched. To do this, we need to determine what the accepting states are after the previous steps of computation. It is helpful to follow the computation process starting from the initial automata, F and S, and consider the two types of their states: the accepting states (labeled a) and the non-accepting states.

S could be completed by adding a new state DC 1 which would be its only non-accepting state, because S is represented by the multi-level network and so is prefix closed.

In , S DC 1 would be the only accepting state. (If S is non- deterministic, {DC 1 } would be the only accepting (subset) state.)

Since F was left incomplete and is prefix closed, all states of F are accepting.

When forming the product F S , a product state is accepting only if both states are accepting. Thus, in F S , the only accepting states would be those with labels (a,DC 1 ) i.e.

accepting in F and accepting in S .

In the subset construction, a subset state is accepting if at least one product state in the subset is accepting, i.e. of type (a,DC 1 ). If such occurs, then those transitions represented by ( , ) Q v u are redirected to DCN, since in the final answer, these states are not accepting [START_REF] Wang | The compositional far side of image computation[END_REF] . The new completion state, DCA, added after the subset construction to complete it, is non-accepting for the determinized product F S , but accepting in the final answer.

Finally, in the complement of this product, which is the maximum solution, the set of accepting states are DCA plus all the subset states which are left in ( , , ) P u v cs after Q has deleted all those that lead to DCN. Thus all non-accepting subset states are mapped into DCN. As mentioned, this can be done because we will make the answer prefix- closed, a requirement for an FSM. (Thus, the X computed is the most general prefix-closed solution.) This requirement increases efficiency, because during the subset construction, as soon as a state of type (a,DC 1 ) is encountered in a subset state, , it can be replaced with DCN. This efficiently reduces the number of subset states that emanate from such S k . Further, those states that are trimmed immediately by this need not be explored for reachability from them. This leads to a substantial trimming during the subset construction. It can be traced back to the fact that S is prefix-closed, and we want X to be prefix-closed. [START_REF] Watanabe | The maximum set of permissible behaviors for FSM networks[END_REF] Similarly, the existence of the single state, DCA, stems from the fact that F is prefix-closed. This allows for deferring the completion of F until the subset construction.

Finally, to make X into a FSM automaton, it is made inputprogressive. This step is the same for both the monolithic and partitioned case and is not detailed here.

Note that in the partitioned flow, neither S nor F is made complete. In effect such completion is deferred to the all-inclusive determinization step. The validity of this is substantiated by the Appendix which proves that the determinization and completion operations commute and observes that completion also commutes with complementation and product.

Experimental results

In this section, an implementation of Algorithm 1 using the partitioned representations is compared with the implementation using the monolithic representations. In effect, the partitioned implementation performs only the determinization procedure, which subsumes all other steps, as described above. In the case of the monolithic representations, the completion of S is done first, then the intermediate product is derived, followed by hiding and determinization, performed in a traditional way.

The examples for this experiment were derived from FSM benchmarks by an operation called latch splitting. This is a syntactic transformation of a sequential circuit into two circuits, one containing a subset of the latches of the original circuit and the other containing the rest. One of these becomes the fixed component, F, in the language solving problem while the other represents a particular solution, X P , for the "unknown" component. The sequential behavior of the original circuit is used as the specification. We compute the complete sequential flexibility (CSFthe largest prefix-closed, input progressive sub-automaton of the most general solution.) Since X P , is a particular, it is contained in the CSF.

After computation of CSF, X, it was formally verified by checking (1)

P X X , and (2)
P F X S F X .

Table 1 lists the results for several examples. The columns show the example name (column "Name"), the number of inputs, outputs and latches (column "i/o/cs"), the number of latches in the fixed part and in the current implementation of the unknown (column "F cs /X cs "), the number of states in the CSF (column "States(X)"), the runtime in seconds of the partitioned algorithm (column "Part") and runtime in seconds using monolithic representations (column "Mono"), and finally the ratio of these runtimes (column "Ratio").

The algorithms were implemented in the MVSIS environment [6]. The measurements were made on a Windows XP computer with a 1.6 ghz CPU. The results show that the partitioned method is more efficient (except for very small examples) with efficiency increasing as the problem size increases. At some point, the monolithic method can not complete (CNC) when the intermediate automata become relatively large. Of course, even the partition method runs out of steam at a certain point, but note that on one example it could handle over 140,000 states in the CSF.

Conclusions

We presented a strategy for solving language equations when the fixed component and the specification are represented using multilevel deterministic sequential networks. In such cases, a partitioned representation derived from the original network can be used to perform all the operations needed to compute the maximum solution. We showed the operations required can be re-formulated in terms of image computations, which can take advantage of the advances made in the efficiency of these computations over the last decade. The proposed methods allow for faster solution of larger problem instances. We emphasize that the techniques described in this paper rely heavily on the fact that both automata, F and S, are represented initially by multi-level sequential networks and hence are prefix closed, and that the desired answer is also prefix closed.

In the Appendix, we argue that not completing F in the algorithm leads to the same answer. This has two important consequences. First, it is not necessary to form the completion conditions before computing the product or its determinization. This saves a lot of computing. Second, completion of F can lead to a non-deterministic product after hiding, while leaving F incomplete leads to a deterministic product after hiding. Thus a subset construction is avoided when F is not completed.

Finally, we note that finding the CSF is only one step in sequential synthesis. Finding an optimum sub-solution of the CSF remains the outstanding problem for future research.

Figure 2 .

 2 Figure 2. The structure of a sequential network.

Figure 3 .

 3 Figure 3. A sequential network and its automaton.

Table 1 .

 1 Comparison of partitioned and monolithic computations.

	Name i/

o/cs F cs /X cs States(X) Part,s Mono,s Ratio

	s510 19/7/6	3/3	54	0.3	0.2	0.7
	s208 10/1/8	4/4	497	0.4	0.8	2.0
	s298 3/6/14	7/7	553	0.9	2.7	3.0
	s349 9/11/15 5/10	2626	37.7	810.3	21.5
	s444 3/6/21	5/16	17730	25.9	CNC	-
	s526 3/6/21	5/16	141829	276.7	CNC	-

We do not distinguish between sets, relations, and their characteristic functions. Therefore, it is possible to think of (cs), Img(ns), and T(i, cs,ns) as completely specified Boolean functions represented using e.g. BDDs.

In this paper, we will illustrate the concepts using next state functions, but the computations also work for the case of non-deterministic relations.

We assume the reader to be somewhat familiar with the concepts related to solving language equations (e.g. see[START_REF] Yevtushenko | Sequential synthesis by language equation solving[END_REF]).

Automata are used since all operations on FSMs are done by first converting these into automata by not distinguishing between inputs and outputs -a simple syntactic change. All states of the resulting automata are accepting states. Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

However, it does not address implementations that can have combinational loops or that are not compositionally progressive[START_REF] Yevtushenko | Compositionally progressive solutions of synchronous language equations[END_REF].

The results of this paper are not limited to the particular topology of Figure1, but we confine the discussion to that of Figure1for ease of presentation.corresponding automaton, since F and S are FSMs and hence are prefix-closed. A "don't-care" (DC) state can be added to make an automaton complete. This is done by making all automaton input combinations, for which the behavior of a state is not defined, transition to DC, which becomes the only non-accepting state. Prefix-closed dictates that DC has a universal self-loop.

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)

Note that it is not necessary to compute subset states which emanate from such a state since once reached, we know that all input sequences with this prefix are not in the language of an FSM.

While this trimming can be substantial, there is no avoiding that subset construction can be exponential. However, it has been a common experience among those who have implemented subset construction, that in practice, it can be surprisingly efficient with relatively few subset states reached, sometimes leading to a reduction in the number of states.

Acknowledgements

The first three authors gratefully acknowledge the support of the National Science Foundation under contract CCR-0312676, and the California Micro program with our industrial sponsors, Intel, Fujitsu, Magma, and Synplicity. The fourth author gratefully acknowledges the support of the MADESSII Project (Italian National Research Council). The fifth author was partly supported by the Russian Ministry of High Education (Grant UR.04.01.018). We gratefully acknowledge the support of a NATO travel grant (NATO Linkage Grant No. 971217).

Appendix: Validity of Non-Completion of F

Theorem 1: To determinize an finite automaton A, the following two procedures are equivalent.

1.

Complete( Determinize( A ), non-accepting ) 2.

Determinize( Complete( A, non-accepting ) )

Proof: We show that these two procedures yield the same result by comparing subset constructions without and with pre-completion. Let DC denote the added non-accepting state. Recall that DC has a universal self-loop. It is clear that if {s 1 , …, s k } is a subset state in the automaton constructed by Procedure 1, then there must exist subset state {s 1 , …, s k } and/or {s 1 , …, s k , DC} in the automaton constructed by Procedure 2. Also, if subset state {s 1 , …, s k } or {s 1 , …, s k , DC} exists in the resultant automaton of Procedure 2, then subset state {s 1 , …, s k } must exist in the resultant automaton of Procedure Under any transition condition, the successor states of {s 1 , …, s k } are the same as those of {s 1 , …, s k , DC} except that the latter contains the DC state. Applying induction on the state space with the above two facts, it follows that subset states {s 1 , …, s k } and {s 1 , …, s k , DC} are equivalent. On the other hand, if a subset state {s 1 , …, s k } or {s 1 , …, s k , DC} can transition to the singleton subset state {DC} under some transition condition, then all of the member states s 1 , …, s k must be incomplete under this transition condition. Therefore, it is immaterial whether the completion is done before or after the determinization. QED

Other trivial propositions state that completion commutes with both the complementation and product operations. Corollary 1 follows from these observations and Theorem 1.

Corollary 1: Let X be the solution obtained by Algorithm 1 when F and S are not completed and let Y be the solution when F and S are made complete first. Then the languages of X and Y are identical.


Valentin Fougerit

Julien Lemaire

Marc-André Theoleyre

Moncef Stambouli

Fougerit Valentin

THEOLEYRE Lemaire Julien

Stambouli Moncef

Modeling the absorption of a gas mixture in a cross-flow hollow-fiber membrane module

may come

Modelling the absorption of a gas mixture in a cross-flow hollow-fiber membrane module

Introduction

Among the industrial processes involving gas-liquid exchanges, hollow-fiber membrane module (HFMM) is an efficient technology thanks to their higher specific area per volume compared to packed columns. Furthermore, it avoids operational problems such as flooding, foaming or plugging.

To help the development of HFMM at an industrial scale, models need to be developed to understand and predict mass transfers. Several studies have described the gas-liquid mass transfer occurring in a hydrophobic gas-liquid HFMM. As carbon capture is a large application of HFMM, most of them have focused on CO2 absorption as a pure gas [START_REF] Mavroudi | A study of mass transfer resistance in membrane gas-liquid contacting processes[END_REF][START_REF] Boributh | A modeling study on the effects of membrane characteristics and operating parameters on physical absorption of CO2 by hollow fiber membrane contactor[END_REF] or mixed in an inert flow [START_REF] Lu | Wetting mechanism in mass transfer process of hydrophobic membrane gas absorption[END_REF][START_REF] Al-Marzouqi | Modeling of absorption of CO2 in membrane contactors[END_REF][START_REF] Khaisri | A mathematical model for gas absorption membrane contactors that studies the effect of partially wetted membranes[END_REF][START_REF] Goyal | Mathematical modeling of CO2 separation from gaseous-mixture using a Hollow-Fiber Membrane Module: Physical mechanism and influence of partial-wetting[END_REF] under atmospheric pressure. To assess the efficiency of a biogas upgrading process, the CH4 losses due to its absorption in the solvent is a key-point. Therefore, an absorption model for a multi-components gas mixture under pressure (0-5 bar g) was developed to identify possible thermodynamic interactions or transfer limitations. The total transfer coefficient Ktot is based on the resistance-in-series model: kl, km and kg are the respective mass transfer coefficients for liquid, membrane and gas phases.

is the adimensional Henry coefficient. dfo, dfi and dln are respectively the outer, inner and logarithmic mean diameters of the hollow-fiber.

Previous models described counter-current flow modules. However, industrial HFMM may include a baffle to divert the liquid flow and increase mass transfer efficiency. Then, for this geometry, the liquid hydrodynamic in the shellside is best described by a cross-flow model.

Moreover, mass transfer in membrane contactor is limited by pore wetting. After some hours of operation, mass-transfer resistance increases [START_REF] Mavroudi | A study of mass transfer resistance in membrane gas-liquid contacting processes[END_REF]. Wetting was described by liquid condensation in the largest pores of the membrane [START_REF] Lu | Wetting mechanism in mass transfer process of hydrophobic membrane gas absorption[END_REF][START_REF] Goyal | Mathematical modeling of CO2 separation from gaseous-mixture using a Hollow-Fiber Membrane Module: Physical mechanism and influence of partial-wetting[END_REF]. As it is a limiting factor for gas absorption efficiency, the model must be validated to ensure process up-scaling.

The present work aims at developing a predictive gas-liquid mass-transfer model for a binary gas mixture which integrates the liquid flow pattern (cross-flow). This model can be extended to a multicomponents gas mixture. The second objective is to implement and experimentally validate a model for the membrane wetting phenomenon under varying working pressures. In the end, model predictions will be compared to experimental data from a biogas upgrading process.

Materials and methods

Figure 1 presents the pilot equipment used to run the experiments for optimizing model parameters and validating the membrane wetting model. The mixture of inlet gas (CO2/CH4) was adjusted (100-700 Nl/h) and the outlet gas flow was measured with mass flow controllers (Bronkhorst). Gas analysis was performed at the inlet and outlet of the membrane contactor with a micro gas chromatography (Agilent 490) with two columns. Softened water was used as the solvent. The liquid flow on the shellside (1-3.5 L/min) was regulated by a vortex flowmeter (Liqui-View) and pressure was controlled at the inlet and the outlet of the membrane contactor (3-5.5 bar g). The CO2 and CH4 absorption flowrates were calculated by mass balance. HFMM was Membrana Liqui-Cel Extra-Flow 2.5x8 equipped with X-50 fibers. Up to now, tests using CO2 as a pure gas were performed. Results in the non-wetting mode were used to optimize parameters from the Chilton-Colburn analogy to calculate liquid mass-transfer coefficient. In the dry mode, concentration profiles can be displayed for a binary gas mixture (Figure 2). Tests at different inlet compositions and operating parameters will be performed for further validation with a binary gas mixture.

Figure 1 :

 1 Figure 1: Experimental set-up

Figure 2 :

 2 Figure 2: CO2 concentration profiles in the gas and the liquid phase Inlet gas 60 % CH4 + 40 % CO2, Pgas = 5 bar g, Qgas = 500 Nl/h, Qliq = 1 L/min