Combining structural and symbolic methods for the verification of concurrent systems

Combining structural and symb olic metho ds for the verication of concurrent systems Jordi Cortadella  Department of Software Universitat Politecnica de Catalunya Barcelona, Spain Abstract The contributions during the last few years on the structural theory of Petri nets can now be applied to formal verication. The structural theory provides methods to nd ecient encoding schemes for symbolic representations of the reachable markings. It also provides approximations of the state space that al low to al leviate many bottlenecks in the calculation of the reachability set by breadth or depth rst search algorithms. The paper reviews some of the results on the structural theory and explains how they can be incorporated inamodel-checking verication framework for concurrent systems. 1 Intro duction Formal verication of concurrent systems suers from the state explosion problem. The number of states of a system can grow exponentially in the numb er of subsystems. One ma jor challenge in the ongoing researchon ver- ication is to signicantly increase the size of the systems that can be veried. The progress achieved by symb olic mo del-checking techniques have approached the verication domain to practical-sized systems. However, there are still serious limitations of time and memory for many cases. We discuss here several techniques for the ver- ication of systems mo deled with Petri nets [16]. For many years, Petri nets have b een the target of many researchers and dierent theoretical results have emerged. These results can now b e used to alleviate some of the verication bottlenecks. We consider the verication of concurrent systems using temp oral logics such as linear temp oral logic (LTL), computation tree logic (CTL) or  -calculus [1]. Typically, temp oral logic formulae can describ e state and path prop erties. An example of state property  This work has b een funded by CICYT TIC 95-0419 is \at most one writer has access to the database" . This is a prop erty that can b e checked lo cally for each state of the system. On the other hand, the property \every request wil l be eventual ly acknow ledged" is a path prop erty that must be checked for all p ossible sequences of events of the system. Verifying a prop erty often requires the exploration of the state space. To reduce the complexityofsuch exploration, approaches going to opposite directions can b e devised, namely,  by reducing the state space while preserving the prop erties that must be veried or  by enlarging the state space, making verication conservative (no false p ositives) but reducing the symb olic representation of the state space. The main contribution of this work is to showhow structural and symb olic techniques can be combined in the same verication framework. The techniques we will discuss can b e classied according to their eect on the calculation and representation of the state space:  State reduction and abstraction techniques.  Symb olic representation of the state space.  Approximations of the state space. We assume the reader to be familiar with Petri nets and symb olic mo del checking techniques. We refer the reader to [12,11] for a basic background on these topics. 2 State reduction and abstraction techniques Partial-order reduction techniques have b een prop osed to reduce the state space generated by concurrent systems [18, 15]. Intuitively, the main observation of these methods relies on the fact that concurrent i1 i1 i1 v vi2 i2 State space i1 i2 vStructural reduction i1 v;i2 Partial-order reduction i1 i1 v v i2 State space i1 v;i2 v;i2 i1 Figure 1: State reduction and abstraction techniques events are modeled by a set of sequences executing all p ossible interleavings. When the execution order is irrelevant for the prop erties that must b e veried, it is enough to cho ose one of them to preserve the b ehavioral skeleton of the system without losing accuracy in the verication task. An example is illustrated in Figure 1. Assume that i 1 and i 2 denote invisible events from the p oint of view of the prop erties that must b e veried. Clearly, the transitions lab eled with i 1 and i 2 are indep endent since they do not share any input/output place. Under such conditions, i 1 and i 2 will o ccur concurrently when enabled and any of the sequences i 1 ; i 2 or i 2 ; i 1 could b e produced. Partial-order reduction techniques would cho ose only one of them, thus resulting in a reduction of the state space. In practice, this technique can be applied by reducing the set of enabled events explored at each state when building the reachability set of the system with breadth or depth rst search algorithms [15]. When the formalism to mo del the system is a Petri net, reduction rules to transform the net into a simpler one that preserves the relevant prop erties can be applied [12, 17]. The example of Figure 1 illustrates one of such rules. Transitions labeled with v and i 2 represent a sequence of these twoevents. A reduction ruled called \fusion of series transitions" can b e applied and obtain a new transition that abstracts the b ehavior of b oth events into a single event lab eled v ; i 2 . Suchtype of rules can b e used to automatically remove invisible actions (e.g. i 2 could b e removed from the label v ; i 2 ) or to derive a symb olic representation of the state space in a hierarchical manner [14]. 3 Symb olic representation of the state space Ordered binary decision diagrams (OBDDs) [2] have emerged as an ecient form to represent b oolean functions and have provided a crucial toolb ox for ver- ication systems based on symb olic mo del checking techniques [11]. Petri nets present a structure appropriate for b oolean enco ding. If we consider a safe Petri net 1 , the state of each place can be enco ded by one b o olean variable. Thus, the reachability set of the Petri net can be represented by a b oolean characteristic function and manipulated by b o olean op erations [14]. Figure 2 depicts a safe Petri net. Its reachability set is represented by the state graph at the left of the gure (8 states). Each state is lab eled with the indices of the marked places. The set of reachable markings can b e characterized by the b o olean function 2 S = ( s 1  s 4 )( s 2  s 3 )( s 5  s 8 )( s 6  s 7 ) (( s 1  s 2 ) , ( s 5  s 6 )) (1) that can b e eciently represented by an OBDD. Traversal algorithms for building the reachability set of the Petri net from its initial marking can be eciently implemented by using b oolean op erations [4,3]. In particular, if m 0 is the initial marking of a net N , the reachability set S can b e obtained by computing the least x p oint of the following recurrence: S 0 = f m 0 g S i +1 = S i [ Image ( N; S i )(2) where Image is a function that returns the states reachable from S i in one step. In the example, Image ( N; f [1256] g )= f [3456] ; [1278] g . The eciency of OBDD-based metho ds manipulating sets of markings has b een shown by dierent authors. As an example, [14] shows how a Petri net mo deling the dining philosophers paradigm can represent the reachability set for 28 philosophers (4 : 8  10 18 markings) with an OBDD of about 10 3 no des. 4 Approximations of the state space The exact exploration of the state space can b e a tedious task, even for symb olic representations of such space. It is well known that, although the nal symb olic representation of the state space can be small, traversal algorithms, such as the one dened by the 1 the metho d can b e easily extended to k -b ounded Petri nets [14]. 2  and , denote XOR and XNOR op erations resp ectively. [1256] [3456] [1278] [3478] [1357] [2457] [1368] [2468] t1 t1 t4 t4 t3 t2 t5 t2 t5 t3 [1257] [3457] [1268] [3468] [1356] [2456] [1378] [2478] t1 t1 t5 t5 t3 t2 t4 t2 t4 t3 t1 t2 t3 t4 t5 s1 s3 s2 s4 s5 s7 s6 s8 Figure 2: Safe Petri net and its reachability set (example from [5]). recurrence (2), often suer from the size of the representation of S i at intermediate steps of the exploration. This phenomenon may cause the exploration to b ecome impractical. Here we review some methods from the structural theory of Petri nets that can alleviate most of these problems. In particular, they can help to nd  an ecient enco ding of the state space  conservative approximations of the state space without executing search algorithms  successive renements of the state space approximation 4.1 Ecient enco ding Assume that it is possible to identify a set of safe places P 0 = f p 1 ;:::;p n g that are not pairwise concurrent, i.e. no pair of places can be marked simultaneously. Thus, at most one token will mark the places in P 0 at any reachable marking of the net. Therefore, the places in P 0 can only b e in n + 1 dierent states. In the case that some place is always marked, only n states are p ossible. Under this constraint, the state of the places in P 0 can b e encoded with d log 2 ( n +1) e (or d log 2 n e if always marked) b o olean variables [13]. Identifying places that are not concurrent can be conservatively performed by computing the structural t1 t2 t3 p1 p3 2 2 2 p2 p4 2010 3002 2104 0120 1112 0214 1206 0308 t1 t1 t1 t2 t2 t2 t2 t3 t3 t3 t2 t3 Figure 3: Potentially reachable markings (example from [12]). concurrency relation [9] that gives necessary conditions for two places not to be concurrent. A complementary way is the calculation of state machines initially marked with one token. State machines corresp ond to place invariants that can be obtained by using algebraic methods [7, 12]. Let us illustrate this feature with the example of Figure 2. There are four place invariants that dene state machines of the net. They corresp ond to the sets of places f s 1 ;s 4 g , f s 2 ;s 3 g , f s 5 ;s 8 g and f s 6 ;s 7 g . In all cases, there is always one place in the set that is marked in the state space. This prop erty can be structurally deduced from the fact that they dene state machines of the net. Thus, the state of each set of places can be enco ded with one b o olean variable. Let us call these variables x 1 ;:::;x 4 resp ectively, i.e. x 1 ) s 1 s 4 , x 1 ) s 1 s 4 , x 2 ) s 2 s 3 , and so on. The set of reachable states can now be characterized by the b o olean equation S = ( x 1  x 2 ) , ( x 3  x 4 ) (3) whichismuch simpler than (1). 4.2 Conservative approximations The structural theory of Petri nets provides ecient mechanisms to derive the so-called potential ly reachable state space , that corresp onds to the set of markings that full the state equation of the Petri net [12]. The state equation gives a sup erset of the state space since any reachable marking fulls the state equation, but not vice versa. Figure 3 depicts a Petri net and its p otentially reachable state space. The states are labeled with four digits that corresp ond to the token countof p 1 :::p 4 resp ectively (the initial marking is 2010). We can ob- serve than one of the markings fulling the state equation, 0308, is not reachable from the initial marking. Using a sup erset of the state space results in some limitations of the predicates that can be veried. Thus, prop erties that hold for al l states in a set ( universal quantiers ) also hold for any subset of states. However properties than hold when there exists some state with a sp ecic characteristic in a set ( existential quantiers ) only hold for sup ersets. Therefore, the p otentially reachable state space provides a conservative metho d to verify properties without existential quantiers. On the other hand, subsets of the reachable state space can b e useful for conservativeverication of prop erties with existential quantiers. 4.3 Renements of the state space approximation We discuss here two approaches to derive successive renements of the state space. Backward state elimination The p otentially reachable state space also provides a starting point to calculate the exact state space using backward state elimination. If we call ^ S 0 the p otentially reachable state space of a net and S the reachable state space, the following recurrence gives successive subsets S  ^ S i +1  ^ S i  ^ S 0 : ^ S i +1 = Image ( N; ^ S i ) [f m 0 g (4) At each step of the recurrence, all those states that are not reachable from anyof the states of ^ S i are eliminated in ^ S i +1 , except the state corresp onding to the initial marking m 0 . In the example of Figure 3, S can be obtained from ^ S 0 by applying the previous recurrence only once, thus eliminating the state 0308 from the reachable set. Unfortunately, a x point does not always guarantee the exact state space. This is illustrated by the example of Figure 2. The shadowed states full the state equation and, therefore, b elong to ^ S 0 . However the backward state elimination cannot remove any state since all states are reachable from some state of the set. In the worst case, still any ^ S i gives an initial set of unreachable states. This knowledge can b e crucial to make the state exploration much more ecientby taking the unreachable states as \don't cares" of the b oolean functions used to represent the transition relation and the reachability set of the net [3]. Mo dulo-invariants Desel et al. [5]intro duced mo dulo-invariants as a generalization of the concept of place-invariants. The interesting property of mo dulo-invariants is that a basis can be calculated in p olynomial time from the incidence matrix of the net by obtaining its Smith Normal Form [8]. Besides providing the conventional place invariants that can b e used to enco de the token countof the places, as explained in section 4.1, they also provide extra information to prune the potentially reachable state space. Let us take again the example of Figure 2. A basis of the place-invariants of the net is the following (all of them corresp onding to state machines): s 1 + s 4 =1 s 2 + s 3 =1 s 5 + s 8 =1 s 6 + s 7 =1 Interestingly, these invariants can b e used to obtain a superset of the state space. By using the enco ding prop osed in section 4.1 with four b o olean variables ( x 1 :::x 4 ) the characteristic function ^ S 0 =1 would be obtained. Note that this is the characteristic function of the 16 states depicted in Figure 2. Even though the state space is larger, the characteristic function is simpler than (3). Mo dulo-invariants provide a new invariant I = s 1 + s 2 + s 5 + s 6  0 (mo d 2) indicating that the token count of the places in the invariant must remain 0 mo dulo 2. As an example, the marking [1357] fulls the invariant since I =2  0 (mo d 2) whereas [1257] do es not since I =3 6 0 (mo d 2) Invariant I removes all shadowed states of Figure 2 from the reachability set. The characteristic function of the markings fulling the modulo-invariant corresp onds to the b o olean equation (3). In general, mo dulo-invariants provide more stringent conditions for reachability than the state equation. In our example, they are able to obtain the exact state space. 5 Putting everything together The metho ds describ ed in the previous section can b e combined in the same verication framework. This illustrated in Figure 4. Petri net of the state space approximation Conservative BDD-encoding of places moduloinvariants Reduced Petri net Structural analysis (place bounds and invariants) Reduction rules (abstraction) State space refinement (backward or forward traversal) verification ? Successful enough resources (CPU, memory) ? Answer: YES NO Answer: Answer: KNOW DON’T state space ? Exact Verification YES YES YES NO NO NO Figure 4: Putting everything together Reduction rules can b e applied at the earliest steps of the verication to simplify the structure of the Petri net. Structural methods based on the state equation and place invariants can b e used to derive an ecient enco ding of the markings. Next, the characteristic function of the p otentially reachable state space can b e derived from the mo dulo-invariants of the net. Finally a cyclic verication pro cess starts. This pro cess completes when some of the following conditions holds:  The veried prop erty conservatively holds for an approximate state space.  The exact state space has b een reached. Then the result of the verication (either positive or negative) is also exact.  The veried prop erty do es not hold in an approximate state space and there are no more resources (time and/or memory) to obtain a further renement of the state space. The answer to the veri- cation pro cess is \don't know" and the designer must conservatively assume that is negative. The successive renements can b e obtained by applying one or several steps of the backward state elimination strategy (4). In case a x p oint is reached, a forward traversal from m 0 must be p erformed using the information ab out unreachable states as \don't care" conditions for the manipulation of b oolean characteristic functions. 6 Conclusions The results on the structural theory of Petri nets make this formalism attractive for the sp ecication and verication of concurrent systems. A Petri netbased verication framework can also be applied to other event-based mo dels, such as pro cess algebras, from whichPetri nets can b e derived, e.g. by syntaxdirected translation techniques. This pap er has presented a strategy to integrate structural and symbolic metho ds in the same mo delchecking verication framework, thus taking advantage of the ecient algorithms devised at each domain. Recent researchby Esparza and Melzer [6] has prop osed to perform conservative verication with the information provided by transition-invariants. The utilization of constraint programming [10] to derive \realizable" transition-invariants results in an ecient strategy to ght against the state explosion problem. The integration of constraint programming in mo del checking techniques seems to deserve further investigation. Acknowledgments I wish to thank Michael Kishinevsky, Luciano Lavagno and Enric Pastor for numerous discussions on the topics presented in this pap er. References [1] A. Arnold. Finite transition systems: semantics of communicating systems . Prentice Hall, 1994. [2] R. Bryant. Symb olic bo olean manipulation with ordered binary-decision diagrams. ACM Computing Surveys , 24(3):293{318, Septemb er 1992. [3] G. Cabodi and P. Camurati. Symb olic FSM traversals based on the transition relation. IEEE Trans. on Computer-Aided Design , 16(5):448{ 457, May 1997. [4] O. Coudert, C. Berthet, and J. C. Madre. Veri- cation of sequential machines using b oolean functional vectors. In L. Claesen, editor, Proc. IFIP Int. Workshop on Applied Formal Methods for Correct VLSI Design , pages 111{128, Leuven, Belgium, Novemb er 1989. [5] J. Desel, K.-P. Neuendorf, and M.-D. Radola. Proving nonreachability by mo dulo-invariants. Theoretical Computer Science , 153:49{64, 1996. [6] J. Esparza and S. Melzer. Mo del checking LTL using constraint programming. In 18th International Conference on Application and Theory of Petri Nets , pages 1{20, June 1997. [7] M. Hack. Analysis of production schemata by Petri nets . PhD thesis, MIT, 1972. [8] R. Kannan and A. Bachem. Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput. , 8(4):499{577, Novemb er 1979. [9] A. Kovalyov and J. Esparza. A p olynomial algorithm to compute the concurrency relation of free-choice signal transition graphs. In Proc. of the International Workshop on Discrete Event Systems (WODES) , pages 1{6, August 1996. [10] K. McAlo on and C. Tretko. Optimization and Computational Logic . John Wiley & Sons, 1996. [11] K.L. McMillan. Symbolic Model Checking . Kluwer, 1993. [12] T. Murata. Petri Nets: Prop erties, analysis and applications. Proceedings of the IEEE , 77(4):541{ 580, April 1989. [13] E. Pastor and J. Cortadella. Ecient enco ding schemes for symb olic analysis of Petri nets. In Proc. of the Conference on Design, Automation and Test in Europe(DATE) , March 1998. [14] E. Pastor, O. Roig, J. Cortadella, and R. Badia. Petri net analysis using b o olean manipulation. In 15th International Conference on Application and Theory of Petri Nets , pages 416{435, June 1994. [15] D. Peled. Combining partial order reductions with on-the-y mo del-checking. Formal Methods in System Design , 8:39{64, 1996. [16] C. A. Petri. Kommunikation mit Automaten . PhD thesis, Bonn, Institut fur Instrumentelle Mathematik, 1962. (technical rep ort Schriften des I IM Nr. 3). [17] M. Silva. Las Redes de Petri: en la Automatica y la Informatica . AC, 1985. (in Spanish). [18] A. Valmari. Stubb orn sets for reduced state space generation. In 10th International Conference on Application and Theory of Petri Nets , pages 1{22, June 1989.