SMT-Based Reachability Checking for Bounded Time Petri Nets

Abstract

Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present a preliminary version of the approach aimed at testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).

Introduction

The process of design and production of both systems and software – among them, the concurrent ones – involves testing whether the product conforms to its specification. This can be achieved using various kinds of formal methods. However, in order to apply any of these methods, the system to be tested needs to be modelled using an appropriate formalism. One of such formalisms, applicable to modelling systems with time dependencies, are time Petri nets by Merlin and Farber [ 1 ]. Numerous subclasses of time Petri nets have been proposed, i.e., 1-safe, bounded, unbounded, distributed nets, and many others.

For concurrent systems, the size of the state-space of the analysed system is a significant factor in the efficiency of the verification. The fact that verification methods need to explore the reachable state-space can lead to the state-space explosion problem. This follows from the fact that the size of the model grows exponentially with the number of the components of the system. Therefore, the development of methods that alleviate this problem is considered an important research subject.

There exist many papers dealing with model checking time Petri nets [ 2– 11 ]. Most of them describe techniques based on explicitly-represented abstractions of the state spaces. The developed fully symbolic methods include decision diagrams-based ones: reachability verification for Integer Timed Petri Nets [ 10 ] as well as LTL and ECTL verification for (1-safe) Distributed Time Petri Nets [ 6 ], and SAT-based methods for the distributed nets [ 6, 8 ].

This paper presents our first attempt to apply a satisfiability modulo theory (SMT) to verification of (bounded) time Petri nets, i.e., reachability testing for the nets restricted to disallow multiple enabledness of transitions. We use a bounded model checking technique (BMC), i.e., consider models truncated up to a specific depth, and transform the reachability problem into a test of satisfiability of a set of (integer) inequalities. Although the current version of the method was implemented, and we provide some preliminary experimental results, we consider our work to be in progress, and we plan on improving the efficiency of our implementation, as well as to extend it in a way allowing to test more involved reachability-related properties and to handle bounded nets with multiple enabledness of transitions [ 12 ].

The rest of the paper is organised as follows: in Sec. 2 we introduce bounded time Petri nets, their concrete state spaces and concrete models. The next Sec. 3 discusses reachability verification using SMT. In Sec. 4 and Sec. 5 we provide some preliminary experimental results and concluding remarks. 2

Time Petri Nets

Let IN (IN+) denote the set of (nonnegative) integers, and IR (IR+) - the set of (nonnegative) reals. We start with a definition of time Petri nets: Definition 1. A time Petri net (TPN for short) is a tuple N m0; Ef t; Lf t), where = (P; T; F; cap; w; – P = fp1; : : : ; pnP g is a finite set of places, – T = ft1; : : : ; tnT g is a finite set of transition s.t. P \ T = ;, – F (P T ) [ (T P ) is a flow relation, – cap : P ! IN+ [ f1g is a partial capacity restriction, – w : F ! IN+ is an arc weight function, – m0 : P ! IN with m0(p) cap(p) for each p 2 P is an initial marking, – Ef t : T ! IN, Lf t : T ! IN [ f1g are functions describing the earliest and the latest firing time of a transition, where for each t 2 T we have Ef t(t) Lf t(t).

A TPN N is called k-bounded, for some k 2 IN+, if cap(p) k for each p 2 P , and is called bounded if there is k 2 IN such that N is k-bounded. The value k is called a bound of N . In what follows we consider bounded time Petri nets only.

For a transition t 2 T we define its preset t = fp 2 P j (p; t) 2 F g and postset t = fp 2 P j (t; p) 2 F g, and consider only the nets such that for each transition the preset and the postset are nonempty. Moreover, we restrict to the nets satisfying the condition 8p2P cap(p) < 2 minfw(p; t) j t 2 T s.t. p 2 tg which prevents multiple enabledness of transitions.

We introduce the following notations and definitions: – a marking of N is a function m : P ! IN, – a transition t 2 T is enabled at a marking m (m[ti for short) if ? for each p 2 t it holds w(p; t) m(p), and ? for each p 2 t it holds m(p) w(p; t) + w(t; p) cap(p) if p 2 t \ t , and m(p) + w(t; p) cap(p) otherwise, – en(m) = ft 2 T j m[tig is the set of all the transitions enabled in a marking m of N , – the marking m0 obtained by firing t 2 en(m) at m is given by m0(p) = ><8> mm((pp)) w(p; t) iiff ((pp;; tt)) 622 FF ^^ ((tt;; pp)) 6622 FF ; > m(p) + w(t; p) if (p; t) 62 F ^ (t; p) 2 F >: m(p) w(p; t) + w(t; p) if (p; t) 2 F ^ (t; p) 2 F : The marking is denoted by m[ti as well, if it does not lead to misunderstanding, – newly_en(m; t) = fu 2 T j u 2 en(m[ti) ^ (9p2(t n t)\ um(p) < w(p; u) _ 9p2 t\t \ um(p) w(p; t) < w(p; u) _ 9p2u \ tm(p) + w(u; p) > cap(p))g is a set of transitions which became (newly) enabled by firing t at m. 2.1

Concrete State Spaces and Models

The current state of the net is given by its marking and the time passed since each of the enabled transitions became enabled (which influences the further behaviour of the net). A concrete state of a TPN N is thus a pair (m; clock), where m : P ! IN is a marking, and clock : T ! IR+ is a function which for each transition t 2 en(m) gives the time elapsed since t became enabled most recently. The set of all the states of N is denoted by . The initial state of N is 0 = (m0; clock0), where m0 is the initial marking of N , and clock0(t) = 0 for each t 2 T .

For 2 IR+, let clock + denote the function given by (clock + )(t) = clock(t) + , and let (m; clock) + denote (m; clock + ). The states of N can change due to a passage of time or due to a firing of a transition. The transition relation ! (T [ IR+) of the net N is thus given by: – in a state = (m; clock) a time

2 IR+ can pass leading to a new state 0 = (m; clock0) (denoted ! 0) iff (clock + )(t) Lf t(t) for each t 2 en(m) (time successor relation), – in a state = (m; clock) a transition t 2 T can fire leading to a new state 0 = (m0; clock0) (denoted !t 0) if t 2 en(m), Ef t(t) clock(t) Lf t(t), m0 = m[ti, and for all u 2 T we have clock0(u) = 0 for u 2 newly_en(m; t), and clock0(u) = clock(u) otherwise (action successor relation).

Intuitively, the time successor relation does not change the marking of the net, but increases the clocks of all the transitions, provided no enabled transition becomes disabled by passage of time. Firing of a transition t takes no time (the only change it introduces to the clocks is reseting these related to the newly enabled transitions) and is allowed provided that t is enabled and its clock is not smaller than Ef t(t) and not greater than Lf t(t). The structure ( ; 0; !) is called a concrete state space of N .

A timed run of N starting at a state 0 2 ( 0-run) is a maximal sequence of concrete states, transitions and time passings = 0 !a0 1 !a1 : : :, where i 2 , and ai 2 T [ IR+ for all i 2 IN. A state ? is reachable if there exists a 0-run and i 2 IN such that ? = i, where i is an element of . The set of all the reachable states of N is denoted by ReachN .

Given a set of propositional variables P V , we introduce a valuation function V : ! 2P V which assigns the same propositions to the states with the same markings. We assume the set P V to be such that each q 2 P V corresponds to an (in)equality I(q) of the form m(p) a or m(p) m(p0) a, where p; p0 2 P , 2 f ; <; =; >; g, 2 f+; g, and a 2 f0; 1; : : : ; 2kg, where k is a bound of N . The function V is defined by q 2 V ((m; clock)) iff I(q) holds for m. The structure M (N ) = ( ; 0; !; V ) is called a concrete model of N . 3

Testing Reachability

The reachability problem for a time Petri net N consists in checking, given a property ', whether N can ever be in a state where ' holds. The property is expressed in terms of propositional variables. Therefore, the problem can be translated into testing whether the set ReachN contains a marking of certain features expressed by '. Checking this can be performed by an explicit exploration of the concrete model for N , but such an approach is usually very inefficient.

If a reachable state satisfying ' exists then proving this can be done using a part of the model only. This enables us to apply the bounded model checking method [ 13 ]. The main idea of testing reachability using BMC consists in searching for an reachability witness of a bounded length l (i.e., for a path leading from the initial state to a state satisfying '). One of the possible approaches to this problem consists in generating a logical formula satisfiable iff such a witness exists, and checking its satisfiability using an appropriate solver. The most common choice here is to use a SAT-solver and a propositional formula, but alternatively an SMT-solver (i.e. a solver capable to test satisfiability of a first-order logic over a built-in theory) and the corresponding first-order logic can be used. We apply the second approach.

In order to check whether a state satisfying ' is reachable, we first replace the model M (N ) by a model with a restricted set of timed labels, i.e., with IR+ substituted by [0; cmax + 1], where by cmax we mean the greatest finite value of Ef t and Lf t of the transitions in N . It can be shown that such a model is bisimilar with M (N ). Moreover, we restrict to integer time steps only, as they are sufficient to prove reachability [ 14, 15 ]. Then, we represent the states of the obtained model using integer variables, encode its transition relation in terms of the logic over integer arithmetics, and encode all the paths of a given length l starting at the initial state of N as a formula P ath(l). We encode also the fact that the property ' holds in the last state of a path as a formula encode_prop( l; ') (we omit technical details of the encodings in the current version of the work), and check satisfiability of the formula := P ath(l) ^ encode_prop( l; '). The above procedure is started from the length of a potential witness l = 0, and repeated iteratively up to (at most) l = jM (N )j. The process is stopped when the formula is satisfiable, as this means that reachability of a state satisfying ' is proven, and therefore no further tests are necessary.

As usually in the case of bounded model checking methods, the above procedure can be inefficient if no state satisfying ' exists, since the depth of the part of the model considered (i.e., l) strongly influences the size of the encoding. Proving unreachability should therefore be done using a different algorithm we do not deal with in the current version of the paper. 3.1

Solving Other Reachability-Related Problems

The language of the propositions used enables to express not only simple properties of the form “a place p contains exactly x tokens”, but also more involved ones, corresponding to various features of a marking of the net, e.g., “a place p contains more tokens than a place q”, “the difference between the numbers of tokens in p and p0 is greater than 5” etc. However, augmenting the net with an additional component enables testing also certain time-related properties. p1 p2 time_exceeded

p3 tick [ 1,1 ]

[ 1,1 ]

An example of such a component is shown in Fig. 1. If we set cap(p2) and w(p2; time_exceeded) to a certain value x 2 IN+, the number of tokens in the place p2 corresponds to the number of time units (not greater than x) passed since the net started, and a token in p3 means that the time assumed has been exceeded. So, augmenting the net with this component enables to express in terms of reachability of a marking the properties like “a state satisfying ' is reachable in less / more than x time units”. It is also possible to search for minimal / maximal time in which a state satisfying ' is reached, using the method similar to that described in [ 8 ]. 4

Experimental Results

In this section, we present preliminary experimental results for the described method. The implemented tool consists of a module that generates an SMT input (the translation) for the SMT-solver, and a guiding module that performs the execution of the verification task which calls the generator module and the SMTsolver for the increasing lengths of the paths, until the SMT-solver terminates with a satisfiable formula.

We also provide a comparison with Sift which is a module of the Tina toolbox [ 16 ] providing on-the-fly verification capabilities. The results we present were generated using the switch -D, i.e., reachability was tested on the graph of essential states [ 14 ], similarly as in our method.

The translation module is implemented in C++ language, and the guiding module is implemented as a simple UNIX shell script. The SMT-solver used in the experiments was Z3 (version 4.3.2) [ 17 ]. The experiments were executed on a Linux 3.9.8 system, equipped with AMD X6 FX-6100 processor, and 8GB of memory. However, for all our experiments we assume the time limit of 2000 seconds, and the memory limit of 2000 MiB. 4.1

Fischer’s Mutual Exclusion Benchmark

In this benchmark we consider a net for the Fischer’s mutual exclusion protocol [ 18 ] depicted in Figure 2. In our figures we assume that unless stated (or setx0_1 denoted in the figure) otherwise, the weight of all the arcs is 1, and the capacity restriction is also 1.

The net models n processes with critical sections. When the i-th process enters (leaves) its critical section criticali (for i 2 f1; ; ng), the number of tokens in the counter place is incremented (decremented). We assume that cap(counter) = n. The mutual exclusion property of the protocol depends on the values of the time-delay constants and , i.e., the property is preserved iff < .

For this benchmark, we assume = 2 and = 1, and we test the reachability of a marking m such that m(counter) > 1. The experimental results for this benchmark are presented in Table 1. The time is given in seconds (cpu time), and the memory in MiB. Where the assumed time or memory limit was exceeded, we denote this in the tables with the symbol ?. 4.2

Assembly Line Benchmark sup1 n

n ready1 reset1 [g, h] s1 [a, b]

n − 1 prep1 [c, d] start1 finish1 sup2

n − 1 ready2 s2 [a, b]

n − 2 prep2 reset2 [g, h] st[ca,rdt]2

finish2 idle1 [e, f] asm1 idle2 [e, f] asm2

· · · supn readyn 1

A net for an abstract assembly line inspired by the generalised transfer chain model from [ 19 ] is presented in Figure 3. It consists of n assembly workers, and a supplier that provides resources needed in the assembly process. There are n resource packages which are represented by tokens in places supi for i 2 f1; ; ng. When an i-th worker receives the resource package via the si transition, it first prepares for the assembly process (prepi), then performs the assembly itself (asmi), and when finishing (f inishi) it also delivers the assembled product to the storage (storage). Then, it idles (idlei), and becomes ready again (readyi).

For all p 2 fsup1; ; supn; storage; deliveredg we assume cap(p) = n. However, note that it could also be assumed that cap(supi) = n i + 1 for i 2 f1; ; ng.

In our benchmark, we also assume the following time constraints in the system: a = 0, b = 5, c = 0, d = 1, e = 0, f = 1, g = 0, h = 1, x = 0, and y = 100. Then, we test the reachability of a marking m, where m(done) > 0 and m(storage) > 0. The length of the witness for this property is n + 2, where n is the number of assembly workers. The experimental results for this benchmark are presented in Table 2. Similarly as before, with ? we mark the cases when the assumed time or memory limit was exceeded. n

SMT-BMC TINA (sift) time memory time memory n

SMT-BMC TINA (sift) time memory time memory

It can be seen from the above results that our implementation has much longer execution times than Tina. However, our method requires less memory than the corresponding Tina execution, and the differences are also significant.

One should also comment on the lack of any comparison with the implementation of the SAT-based reachability verification described in [ 8 ]. The paper mentioned provides experimental results for the Fischer’s mutual exclusion protocol obtained on a computer equipped with Intel Pentium Dual CPU (2:00 GHz) and 2 GB of main memory, and confirms verifying the system consisting of 40 processes in 2999:5 seconds and using 1153:2 MB of memory. This seems to be a far better result. However, it should be noticed that the method of [ 8 ] was developed for distributed TPNs, of a semantics aimed at making verification more efficient than in the standard case (i.e., of the one in which clocks are assigned to the processes of the net instead of to the transitions which enables to reduce their number from 6n to n + 1). The distributed nets are also 1-safe, which reduces further the complexity of their description. 5

Final Remarks

We have presented a preliminary version of a reachability verification method for (bounded) time Petri nets, based on bounded model checking and SMT. In our future work we are going to build upon this method an approach allowing to verify more involved properties. In the preliminary comparison with Tina our method performed efficiently in terms of the memory consumption when testing the reachability property, which is very promising for the mentioned extension of our work.

Acknowledgements. Artur Me¸ski acknowledges the support of the EU, European Social Fund. Project PO KL “Information technologies: Research and their interdisciplinary applications” (UDA-POKL.04.01.01-00-051/10-00).

References

1. Merlin , P. , Farber , D.J.: Recoverability of communication protocols - implication of a theoretical study . IEEE Trans. on Communications 24 ( 9 ) ( 1976 ) 1036 - 1043

2. Berthomieu , B. , Diaz , M. : Modeling and verification of time dependent systems using time Petri nets . IEEE Trans. on Software Eng . 17 ( 3 ) ( 1991 ) 259 - 273

3. Berthomieu , B. , Vernadat , F. : State class constructions for branching analysis of time Petri nets . In: Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03) . Volume 2619 of LNCS., Springer-Verlag ( 2003 ) 442 - 457

4. Boucheneb , H. , Hadjidj , R.: CTL model checking for time Petri nets . Theoretical Computer Science 353 ( 1 ) ( 2006 ) 208 - 227

5. Lime , D. , Roux , O.H. : Model checking of time Petri nets using the state class timed automaton . Discrete Event Dynamic Systems 16 ( 2 ) ( 2006 ) 179 - 205

6. Me¸ski, A. , Penczek , W. , Półrola , A. , Woźna-Szcześniak , B. , Zbrzezny , A. : Bounded model checking approaches for verificaton of distributed time Petri nets . In: Proc. of the Int. Workshop on Petri Nets and Software Engineering (PNSE'11) , University of Hamburg ( 2011 ) 72 - 91

7. Penczek , W. , Półrola , A. : Abstractions and partial order reductions for checking branching properties of time Petri nets . In: Proc. of the 22nd Int. Conf. on Applications and Theory of Petri Nets (ICATPN'01) . Volume 2075 of LNCS ., Springer-Verlag ( 2001 ) 323 - 342

8. Penczek , W. , Półrola , A. , Zbrzezny , A. : SAT-based (parametric) reachability for a class of distributed time Petri nets . In: Trans. on Petri Nets and Other Models of Concurrency IV. Volume 6550 of LNCS . Springer-Verlag ( 2010 ) 72 - 97

9. Virbitskaite , I.B. , Pokozy , E.A. : A partial order method for the verification of time Petri nets . In: Fundamental of Computation Theory. Volume 1684 of LNCS . Springer-Verlag ( 1999 ) 547 - 558

10. Wan , M. , Ciardo , G.: Symbolic reachability analysis of integer timed Petri nets . In: Proc. 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM) . ( 2009 ) 595 - 608

11. Yoneda , T. , Ryuba , H.: CTL model checking of time Petri nets using geometric regions . IEICE Trans. Inf. and Syst . 3 ( 1998 ) 1 - 10

12. Boyer , M. , Diaz , M. : Multiple enabledness in Petri nets with time . In: Proc. of the 9th Int. Workshop on Petri Nets and Performance Models (PNPM'01) . ( 2001 ) 219 - 228

13. Biere , A. , Cimatti , A. , Clarke , E. , Zhu , Y. : Symbolic model checking without BDDs . In: Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99) . Volume 1579 of LNCS., Springer-Verlag ( 1999 ) 193 - 207

14. Popova-Zeugmann , L. : Time Petri nets state space reduction using dynamic programming . Journal of Control and Cybernetics 35 ( 3 ) ( 2006 ) 721 - 748

15. Janowska , A. , Penczek , W. , Półrola , A. , Zbrzezny , A. : Towards discrete-time verification of time Petri nets with dense-time semantics . In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'11) , Bialystok University of Technology ( 2011 ) 215 - 228

16. Berthomieu , B. , Ribet , P.O. , Vernadat , F. : The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets . International Journal of Production Research 42 ( 14 ) ( 2004 )

17. de Moura , L. , Bjørner , N.: Z3: An efficient SMT solver . In: Proc. of the 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08) . Volume 4963 of LNCS., Springer-Verlag ( 2008 ) 337 - 340

18. Abadi , M. , Lamport , L. : An old-fashioned recipe for real time . In: REX workshop on Real-Time: Theory in Practice . Volume 600 of LNCS., Springer-Verlag ( 1991 ) 1 - 27

19. Tsinarakis , G. , Tsourveloudis , N. , Valavanis , K. : Modular Petri net based modeling, analysis, synthesis and performance evaluation of random topology dedicated production systems . Journal of Intelligent Manufacturing 16 ( 1 ) ( 2005 ) 67 - 92