Generalized Büchi Automata versus Testing Automata for Model Checking

Abstract

Geldenhuys and Hansen have shown that a kind of w-automaton known as testing automata can outperform the Büchi automata traditionally used in the automata-theoretic approach to model checking [8]. This work completes their experiments by including a comparison with generalized Büchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulae (for which testing automata fare better) from verified formulae (where testing automata are hindered by their two-pass emptiness check).

1 Introduction

Unfortunately, having a smaller property automaton A:j does not always imply that the product with the model (AM A:j) will be smaller, and it is the size of this product that really affects the efficiency of the model checking. Instead of targeting smaller property automata, some people have attempted to build automata that are more deterministic [ 21 ]; however even this does not guarantee the product to be smaller.

Hansen et al. [ 11 ] introduced a new kind of w-automaton called Testing Automaton. These automata are less expressive than Büchi automata since are tailored to represent stuttering-insensitive properties (such as any LTL property that does not use the X operator). Also they are often a lot larger than their equivalent Büchi automaton, but surprisingly their good determinism often lead to a smaller product. The reasons why and the conditions under which testing automata perform better are still mysterious [ 8 ]. Objectives The objective of this paper is to evaluate efficiency of LTL model checking with these three kinds of w-automata: classical Büchi Automata (BA), Transition-based Generalized Büchi automata (TGBA), and Testing Automata (TA). Our main motivation is to try to establish some rough rules to choose automatically and a priori the technique that seems most suitable to check a given stuttering-insensitive property on a given model. This is of interest when a tool offers the choice of several techniques, which is the case for our model checker Spot [ 16 ].

Contents Section 2 provides a brief summary of the three w-automaton and pointers to their associated operations for model checking. Then section 3 reports our experimentation procedure and its results before a discussion in section 4. 2

Presentation of the three Approaches

Let AP designate the set of atomic proposition of the model that we might want to use to build a linear-time property. Any state of the model can be labeled by a valuation of these atomic propositions. We denote by K = 2AP the set of these valuations. For instance if AP = fa; bg, then K = 2AP = fa¯b¯; a¯b; ab¯; abg. An execution of the model is simply an infinite sequence of such valuations, i.e., an element from Kw. A property can be seen as a set of sequences, i.e. a subset of Kw.

This section presents the three kinds of automata we compare in this paper: Transitions-based Generalized Büchi Automata, Büchi Automata and Testing Automata. For all of them, we explain how they recognize subsets of Kw to show their differences. We do not detail the actual operations that must be performed to model check a system which each approach because this has already been done in other works. (a) ab¯ j

a¯b a¯b¯ ab 2.1

Transition-based Generalized Büchi Automata

A Transition-based Generalized Büchi Automata (TGBA) [ 10 ] over an alphabet K = 2AP is an w-automaton where transitions are labeled by letters from K and some acceptance conditions. In our context, the TGBA represents the LTL property to verify. Definition 1 A TGBA can be formally represented by a tuple G = hS; I; R; Fi where: – S is finite set of states, – I S is the set of initial states, – F is a finite set of acceptance conditions, – R S 2K 2F S is the transition relation, where each element (si; Ki; Fi; di) represents a transition from state si to state di labeled by the non-empty set of letters Ki, and the set of acceptance conditions Fi.

An execution w = k0k1k2 : : : 2 Kw is accepted by G if there exists an infinite path (s0; K0; F0; s1)(s1; K1; F1; s2)(s2; K2; F2; s3) : : : 2 Rw where: – s0 2 I, and 8i 2 N; ki 2 Ki K (the execution is recognized by the path), – 8 f 2 F; 8i 2 N; 9 j i; f 2 Fj (each acceptance condition is visited infinitely often). Model checking using TGBA When doing model checking with TGBA the two important operations are the translation of the linear-time property j into a TGBA A:j and the emptiness check of the product AM A:j. We know of at least four algorithms that purposedly translate LTL formulae into TGBA [ 10, 3, 4, 22 ]. The one we use is based on Couvreur’s LTL translation algorithm [ 3 ].

Testing a TGBA for emptiness amounts to the search of a strongly connected component that contains at least one occurrence of each acceptance condition. It can be done in two different way: either with a variation of Tarjan or Dijkstra algorithm [ 3 ] or using several nested depth-first searches to save some memory [ 22 ]. The latter proved to be slower [ 5 ], so we are using Couvreur’s SCC-based emptiness check algorithm [ 3 ]. Another advantage of the SCC-based algorithm is that their complexity does not depend on the number of acceptance conditions. Definition 2 A BA over the alphabet K = 2AP is a tuple B = hS; I; R; Fi where: – S is a set of finite set states, – I S is the set of initial states, – F S is a finite set of acceptance states, – R S 2K S is the transition relation where each transition is labeled by a set of letters of K. An execution w = k0k1k2 : : : 2 Kw is accepted by B if there exists an infinite path (s0; K0; s1)(s1; K1; s2)(s2; K2; s3) : : : 2 Rw such that: – s0 2 I, and 8i 2 N; ki 2 Ki (the execution is recognized by the path), – 8i 2 N; 9 j i; s j 2 F (at least one acceptance state is visited infinitely often). Model checking using BA A BA can be obtained from a TGBA by a procedure known as degeneralization [ 3, 10 ]. In a worst case, a TGBA with s states and n acceptance conditions will be degeneralized into a BA with s (n + 1) states (and one acceptance condition). This is what we do in our experiments. Alternatives include the translation of the property into a state-based generalized automaton which can then also be degeneralized, or the translation of the property into an alternating Büchi automaton that is then converted into a BA using the Miyano-Hayashi construction [ 15 ].

The emptiness check algorithms that can deal with TGBA will also work on BA (a BA can be seen as a TGBA by pushing the acceptance conditions on the transition leaving acceptance states). But it can also be done using two nested depth-first searches. The comparison of these different emptiness checks has raised many studies [ 9, 20, 5 ].

Fig. 2 shows the same properties as Fig. 1, but expressed as Büchi automata. The automaton from Fig. 2(a) was built by degeneralizing the TGBA from Fig. 1(a). The worst case of the degeneralization occurred here, since the TGBA with 1 state and n acceptance conditions was degeneralized into a BA with n + 1 states. It is known that no BA with less than n + 1 states can recognize the property Vin=1 G F pi so this Büchi automaton is optimal [ 2 ]. The property a U G b, on the other hand, is easier to express: the BA has the same size as the TGBA. (b) A property, i.e., a set of infinite sequences P Kw, is stuttering-insensitive iff any sequence k0k1k2 : : : 2 P remains in P after repeating any valuation ki. In other words, P is stuttering-insensitive iff

() k0i0 k1i1 k2i2 : : : 2 P for any i0 > 0; i1 > 0 : : :

It is well known that any LTLn X formula (i.e. an LTL formula that does not use the X operator) describes a stuttering-insensitive property. (It is possible to build some stuttering-insensitive LTL formulae using the X operator [ 6 ].)

Testing Automata (TA) were introduced by Hansen et al. [ 11 ] to represent stutteringinsensitive properties. While a Büchi automaton observes the value of the atomic propositions AP, the basic idea of TA is to detect the changes in these values; if a valuation of AP does not change between two consecutive valuations of an execution, the TA can stay in the same state. To detect execution that ends by stuttering in the same TA state, a new kind of acceptance states is introduced: "livelock acceptance states".

If A and B are two valuations, let us note A B the symmetric set difference, i.e. the set of atomic propositions that changed. E.g. ab¯ ab = fbg.

Definition 3 A TA over the alphabet K = 2AP is a tuple T = hS; I;U; R; F; Gi. where: – S is a finite set of states, – I S is the set of initial states, – U : I ! K is a function mapping each initial state to a symbol of K interpreted as a valuation (the initial configuration), – R S K S is the transition relation where each transition (s; k; d) is labeled by a changeset: k 2 K = 2AP is interpreted as a set of atomic propositions that should change between states s and d, – F S is a set of Büchi acceptance states, – G S is a set of livelock acceptance states.

An execution w = k0k1k2 ::: 2 Kw is accepted by T if there exists an infinite sequence (s0; k0 k1; s1)(s1; k1 k2; s2) : : : (si; ki ki+1; si+1) : : : 2 (S K S)w such that: – s0 2 I with U (s0) = k0, – 8i 2 N, either (si; ki ki+1; si+1) 2 R (we are progressing in the testing automaton), or ki = ki+1 ^ si = si+1 (the execution is stuttering and the TA does not progress), – Either, 8i 2 N; (9 j i; k j 6= k j+1) ^ (9l i; sl 2 F) (the automaton is progressing in a Büchi-accepting way), or, 9n 2 N; (sn 2 G ^ (8i n; si = sn ^ ki = kn)) (the sequence reaches a livelock acceptance state and then stay on that state because the execution is stuttering).

Construction of a Testing Automaton from a Büchi Automaton From a BA B = (SB; IB; RB; FB) over the alphabet K = 2AP, we obtain a TA T = (ST ; IT ;UT ; RT ; FT ; GT ) representing the same property in two steps [ 8 ]: 1. Converting B into an intermediate form of T with GT = 0/ : – ST = SB K; IT = IB K; FT = FB K, and GT = 0/ – 8(s; k) 2 IT ; UT ((s; k)) = k – 8(s1; k1) 2 ST ; 8(s2; k2) 2 ST ;

((s1; k1); k1 k2; (s2; k2)) 2 RT () 9k 2 2K ; ((s1; k; s2) 2 RB) ^ (k1 2 k) 2. Filling GT to simplify T . For that, compute all strongly connected components using only stuttering transitions (i.e., transitions labeled by 0/ ). If such a SCC is not trivial (i.e., it contains a cycle) and contains a Büchi acceptance state, then add all its states to GT . Add to IT or GT any state that can respectively reach IT or GT using only stuttering transitions. Finally remove all stuttering transitions from RT . Additionally, the TA can be minimized by merging bisimilar states.

Fig. 3 shows the automaton constructed for a U G b by applying the above construction on the automaton from Fig. 2(b). The TA for G F a ^ G F b is too big to be shown: it has 11 states and 64 transitions. ab¯ ab a¯b fbg

fbg a U G b; ab¯ a U G b; ab

fag a U G b; a¯b fa; bg

fag fag fag

G b; a¯b G b; ab fag ab¯ ab a¯b fbg a U G b; ab¯ a U G b; ab

fag a U G b; a¯b fbg fa; bg fag fag fag G b; b (a) Before reduction.

(b) After reduction by bisimulation. Emptiness check using TA A first difference between the BA and TA approaches appears in the product computation. Indeed, a testing automaton remains in the same state when the Kripke structure executes a stuttering step.

The emptiness check also requires a dedicated algorithm because there are two ways to accept an execution: Büchi acceptance or livelock acceptance. In the algorithm sketched by Geldenhuys and Hansen [ 8 ], a first pass is used with an heuristic to detect both Büchi and livelock acceptance cycles. Unfortunately, in certain cases this first pass fails to report existent livelock acceptance cycles. This implies that when no counterexample is found by the first pass, a second one is required to double-check for possible livelock acceptance cycles. These two passes are annoying when the property is satisfied (no counterexample) since the entire state-space has to be explored twice. Optimizations Looking at Fig. 3 inspires two optimizations. The first one is based on the fact that the construction of testing automata described in previous section will generate a lot of bisimilar states such as (G b; a¯b) and (G b; ab). This is because the construction considers all the elements of K that are compatible with G b. Had the LTL formula been over AP = fa; b; cg, e.g., (a _ c) U G b, then we would have had four bisimilar states: (G b; a¯bc¯), (G b; a¯bc), (G b; abc¯), and (G b; abc). These state are necessarily isomorphic, because they only differ in a and c, some propositions that the formula G b does not observe.

A more efficient way to construct the testing automaton (and to construct the automaton from Fig. 3b directly) would be to consider only the subset of atomic propositions that are observed by the corresponding state of the Büchi automaton or its descendants (if the state is labeled by an LTL formula, the atomic propositions occurring in this formula give an over-approximation of that set).

A second optimization relies on the fact any state that no part of a SCC (also called trivial SCC) can be added to F without changing the language of the automaton. This is true for the three kinds of automata. For instance on Fig. 3 the state (a U G b; a¯b) can be added to F. Since this state is not part of any cycle, it cannot occur infinitely often and therefore cannot change the accepted language of the automaton.

This change allows further simplifications by bisimulation: the state (a U G b; a¯b) is now ab¯ a U G b; ab¯ fa; bg fag obviously equivalent to the (G b; b) state. Fig. 4 shows the resulting automaton. Note that putting fbg fbg G b; b any trivial SCC x in F before preforming bisim- ab a U G b; ab fag ulation could hinder the reduction if x was a¯b isomorphic to some state not in F. However Fig. 4: Reduced TA for a U G b. if x has only successors in F, as in our example, then it can be put safely in F: indeed, it can only be isomorphic to an F-state, or to another trivial SCC that will be added to F. This condition is similar to the one used by Löding before minimizing deterministic weak w-automata [ 14 ]. 3

Experimentation

This section presents our experimentation of the various types of automata within our tool Spot [ 16 ]. We first present the Spot architecture and the way the variation on the model checking algorithm was introduced. Then we present our benchmarks (formulae and models) prior to the description of our experiments.

3.1 Implementation on top of Spot

Spot is a model-checking library offering several algorithms that can be combined to build a model checker [ 7 ]. Fig. 5 shows the building blocks we used to implement the three approaches. The TGBA and BA approaches share the same synchronized product and emptiness check, while a dedicated algorithms is required by the TA approach.

In order to evaluate our approach on “realistic” models, we decided to couple the Spot library with the CheckPN tool [ 7 ]. CheckPN implements Spot’s Kripke structure interface in order to build the state space of a Petri net on the fly. This Kripke structure is then synchronized with an w-automaton (TGBA, BA, or TA) on the fly, and fed to the suitable emptiness check algorithm. The latter algorithm drives the on-the-fly construction: only the explored part of the product (and the associated states of the Kripke structure) will be constructed.

Constructing the state space on-the-fly is a double-edged optimization. Firstly, it saves memory, because the state-space is computed as it is explored and thus, does not need be stored. Secondly, it also saves time when a property is violated because the emptiness check can stop as soon as it has found a counterexample. However, on-thefly exploration is costlier than browsing an explicit graph: an emptiness check algorithm such as the one for TA [ 11 ] that does two traversals of the full state-space in the worst case (e.g. when the property holds) will pay twice the price of that construction.

In the CheckPN implementation of the Kripke structure, the Petri Net marking are compressed to save memory. The marking of a state has to be uncompressed every time we compute its successors, or when we compute the value of the atomic properties on this state. These two operations often occur together, so there is a one-entry cache that prevents the marking from being uncompressed twice in a row. 3.2

Benchmark Inputs

We selected some Petri net models and formulae to compare these approaches. Toy Examples A first class of four models were selected from the Petri net literature [ 1 ]: the flexible manufacturing system (FMS), the Kanban system, the dining philosophers, and the slotted-ring system. All these models have a parameter n. For the dining philosophers, and the slotted-ring, the model are composed of n identical 1-safe subnets. For FMS and Kanban, n only influences the number of tokens in the initial marking.

We chose values for n in order to get state space having between 2 105 to 3 106 nodes. The objective is to have comparable state spaces to be synchronized. Case Studies The following two bigger models, were taken from actual cases studies. They come with some dedicated properties to check.

MAPK models a biochemical reaction: Mitogen-activated protein kinase cascade [ 12 ]. For a scaling value of 8 (that influences the number of tokens in the initial marking), it contains 22 places and 30 transitions. Its state space contains 6:11 106 states. The authors propose to check that from the initial state, it is necessary to pass through states RafP, MEKP, MEKPP and ERKP in order to reach ERKPP. In LTL: F1 = :((:RafP) U MEKP) ^ :((:MEKP) U MEKPP)^

:((:MEKPP) U ERKP) ^ :((:ERKP) U ERKPP)

PolyORB models the core of the μbroker component of a middleware [ 13 ] in an implementation using a Leader/Followers policy [ 18 ]. It is a Symmetric Net and, since CheckPN processes P/T nets only, it was unfolded into a P/T net. The resulting net, for a configuration involving three sources of data, three simultaneous jobs and two threads (one leader, one follower) is composed of 189 places and 461 transitions. Its state space contains 61 662 states3. The authors propose to check that once a job is issued from a source, it must be processed by a thread (no starvation). It corresponds to: F2 = G(MSrc1 ! F(DOSrc1)) ^ G(MSrc2 ! F(DOSrc2)) ^ G(MSrc3 ! F(DOSrc3)) Types of Formulae As suggested by Geldenhuys and Hansen [ 8 ], the type of formula may affect the performances of the various algorithms. In addition to the formulae F1 and F2 above, we consider two classes of formulae: 3 This is a rather small value compared to MAPK but, due to the unfolding, each state is a 189value vector. PolyORB with three sources of data, three simultaneous jobs and three threads would generate 1 137 096 states with 255-value vectors, making the experiment much too slow. – RND: randomly generated LTL formulae (without X operator). Since random formulae are very often trivial to verify (the emptiness check needs to explore only a handful of states), for each model we selected only random formulae that required to explore more than 2000 states with the TGBA approach. – WFair: properties of the form (Vin=1 G F pi) ! j, where j is a randomly generated LTL formula. This represents the verification of j under the weak-fairness hypothesis Vin=1 G F pi. The automaton representing such a formula has at least n acceptance conditions which means that the BA will in the worst case be n + 1 times bigger than the TGBA. For the formulae we generated for our experiments we have n 3:19 on the average.

All formulae were translated into automata using Spot, which was shown experimentally to be very good at this job [ 19 ]. 3.3

Results

These tables separate cases where formulae are verified from cases where they are violated. In the former (left sides of the tables), no counterexample are found and the full state space had to be explored; in the latter (right sides) the on-the-fly exploration of the state space stopped as soon as the existence of a counterexample could be computed.

The numbers displayed in parentheses on both sides of the tables are the number of formulae involved in the experiment. For instance (reading Table 2) we checked Kanban5 against 98 weak-fairness formulae that had no counterexample, and against 102 weak-fairness formulae that had a counterexample. The average and maximum are computed separately on these two sets of formulae.

Column-wise, these tables show the average and maximum sizes (states and transitions) of: (1) the automata A:ji expressing the properties ji; (2) the products A:ji AM of the property with the model; and (3) the subset of this product that was actually explored by the emptiness check. For verified properties, the emptiness check of TGBA and BA always explores the full product so these sizes are equal, while the emptiness check of TA always performs two passes on the full product so it shows double values. On violated properties, the emptiness check aborts as soon as it finds a counterexample, so the explored size is usually significantly smaller than the full product.

The emptiness check values show a third column labeled “T”: this is the time (in hundredth of seconds, a.k.a. centiseconds) spent doing that emptiness check, including the on-the-fly computation of the subset of the product that is explored. The time spent constructing the property automata from the formulae is not shown (it is negligible compared to that of the emptiness check). These tests were performed on a 64bit Linux system running on an Intel Core i7 CPU 960 at 3.20GHz, with 24GB of RAM. Running this entire benchmark with four tasks in parallel took us two days. Ring6 (100) Philo8 (100) Kanban5 (100) FMS5 (70)

T T T T t T eh a y lb .) ap t h e d e T B G T B G T B G T B G o 1 A A B A A B A A B A A B ( : A A A A r C ig o M A M A M A M A M A M A M A M A M A M A M A M A : : 0 7 : : : : : : : : : 9 5 0 2 3 5 5 6 1 d i a 1 1 9 0 1 9 9 0 3 2 3 2 0 0 4 2 4 2 8 0 6 3 6 7 u fi ch 60 36 30 21 67 04 08 92 66 43 66 23 33 47 56 97 56 97 51 32 37 98 12 05 .tr tc ed e 4 3 0 9 7 9 9 3 2 9 2 0 6 8 1 8 1 2 6 4 4 5 3 2 s 3 6 6 4 8 5 8 9 8 4 8 8 0 5 3 8 3 4 0 6 9 9 3 0

2 0 4 6 4 3 1 3 2 4 2 0 8 8 6 9 6 9 5 9 4 1 3 1 o n 1 co t 4 4 4 1 2 1 6 6 8 1 8 5 u o 4 7 3 4 1 4 1 2 8 2 8 2 8 3 6 8 6 8 1 0 3 7 9 6 n y 6 5 7 9 6 7 0 9 3 2 3 1 1 0 9 5 9 5 5 4 1 9 6 9 s t 5 8 8 4 2 6 8 7 0 0 0 9 9 2 4 2 4 2 6 2 0 0 1 8 .t e r a 2 1 n 8 1 7 7 2 1 1 5 2 8 8 4 1 9 7 d 1 3 6 5 1 5 4 6 1 2 1 2 3 4 3 9 3 9 4 8 5 8 6 7 T o 3 2 8 8 8 6 7 6 7 5 7 5 4 5 3 1 7 0 9 6 8 3 8 4 m 0 9 3 2 1 4 2 2 4 8 2 7 4 1 5 0 3 9 0 5 2 0 5 0 p v ro re ( n o f 1 1 1 1 o 4 3 2 2 6 3 3 2 3 2 3 2 2 2 6 3 s A r 1 3 5 8 0 7 0 6 8 9 7 7 4 9 8 8 2 7 3 6 3 7 0 :6 .t u m :8 :5 :0 :6 :1 :3 :7 :6 :0 :8 :6 3 to u 3 3 2 3 1 m l ae 5 5 4 1 3 2 6 6 1 3 2 3 4 2 2 3 0 4

Ring6 (100) Philo8 (100) Kanban5 (100) FMS5 (230) w T h ab en le

Ring6 (100) Philo8 (100) Kanban5 (98) FMS5 (37)

T T T T

T B G T B G T B G T B G th 2 A A B A A B A A B A A B e : A A A A y C

M A M A M A M A M A M A M A M A M A M A M A M A o 0 2 2 f t h e

7 2 2 3 1 1 4 3 5 1 a 20 20 40 44 98 21 46 45 13 47 72 19 64 23 50 31 56 14 60 61 26 58 04 26 .tr to n : : : : : : : 1 9 3 9 7 1 6 : : : 9 1 4 t h 1 2 2 P ree 568 239 688 346 116 632 665 411 691 226 691 911 767 293 037 832 902 370 002 697 338 235 686 917 .ts F reop a 1 5 2 7 4 2 5 3 9 2 9 2 5 5 0 8 1 7 1 4 1 0 0 3 u r pp 12 99 18 29 58 96 09 03 46 31 46 33 24 97 85 71 82 09 96 33 61 10 94 75 ll ty p v 1 1 6 1 2 3 8 2 9 3 1 7 9 5

7 8 0 9 1 8 6 0 3 6 3 0 6 9 5 7 1 3 8 7 0 5 6 7 o 3 3 3 1 5 3 0 6 3 5 3 3 7 0 7 4 2 8 5 6 5 4 6 1 n 6 1 8 5 6 7 0 3 3 7 3 9 2 7 5 5 6 7 1 5 3 6 7 7 c to 1 1 1 1 uo y 3 2 2 1 3 3 2 3 8 2 8 7 1 7 9 5 n 3 6 8 4 1 3 3 2 9 2 9 1 3 8 3 3 0 7 0 9 3 3 8 1 t e 1 5 6 3 1 6 3 8 6 2 6 9 5 4 0 8 9 3 0 3 3 2 6 9 s e x 6 9 8 6 6 2 1 2 1 6 1 1 5 7 7 2 2 0 4 4 8 5 6 7 .t re a 2 1 2 7 4 2 0 6 9 2 9 2 0 1 0 8 1 7 3 8 1 0 0 3 E x m 2 9 1 2 5 9 1 0 4 3 4 3 4 9 8 7 8 0 9 6 6 1 9 7 m am 4 8 8 9 8 6 8 7 6 1 6 3 8 4 5 1 2 9 2 6 1 0 4 5

1 1 1 1 1 1 1 1 2 3 1 2 7 2 4 6 0 5 9 4 tin le 8 3 7 2 3 2 0 1 8 1 8 1 7 4 3 6 8 3 0 2 3 3 1 3 e ) w 8 6 1 3 8 0 0 9 5 2 5 0 5 8 0 7 6 0 3 8 8 4 4 0 s i 0 6 9 7 7 7 9 3 8 1 8 7 6 0 7 0 2 7 0 3 1 7 9 7 tr s t 5 3 2 0 7 2 7 8 4 9 4 2 9 7 9 5 4 1 5 9 6 1 9 8 . c h 4 6 0 9 1 8 2 1 3 6 3 0 3 8 5 7 1 3 7 5 0 5 6 7 h w 7 6 3 1 5 3 0 2 3 5 3 3 4 1 7 4 2 8 0 3 5 4 6 1 ec 2 1 8 5 6 7 0 7 3 7 3 9 4 5 5 5 6 7 2 1 3 6 7 7 k e a 2 1 1 3 1 1 1 k 5 1 3 2 3 1 1 6 6 1 3 0 2 1 4 3 7 3 6 - 6 1 1 4 5 4 0 6 5 2 5 2 6 8 9 1 2 7 5 2 3 7 2 1 T fa 2 2 6 7 3 1 2 1 7 5 8 2 5 9 6 8 1 8 1 3 9 0 8 9 i 9 1 8 6 1 3 6 5 7 4 1 5 1 1 2 3 4 8 5 1 4 8 2 1 r n : : : 7 6 5

P , 1 2 1 4 1 6 1 2 ro w 5 2 6 2 2 2 3 1 8 6 3 8 3 5 7 5 4 7 1 9 p h 1 1 6 1 5 9 2 8 3 9 1 3 1 3 1 4 9 4 0 3 4 2 4 9 e en 31 66 14 21 37 30 08 89 96 52 60 88 41 56 44 80 00 48 47 93 77 79 31 53 .ts F try 4 2 6 8 1 9 4 7 9 5 2 3 7 2 8 1 3 2 6 1 3 2 9 8 u v c 2 4 4 2 8 0 5 5 0 4 7 5 1 8 4 1 2 0 9 8 0 1 7 2 ll i o 2 1 5 6 6 9 9 2 0 0 9 6 2 0 8 0 0 9 2 6 8 9 3 8 u rp lo 1 3 1 4 1 7 1 3 a n 3 1 4 1 1 1 2 1 9 6 0 8 6 5 1 2 8 5 1 8 o t te 0 2 2 2 6 5 6 6 4 6 0 2 0 1 0 2 6 5 5 6 4 4 9 9 ud ed rex 617 753 264 263 628 158 288 548 826 664 319 386 156 208 344 246 308 983 762 529 271 786 221 505 .tr tc (a am 56 56 88 60 86 05 19 51 32 87 16 79 98 29 05 56 72 40 99 78 60 14 81 05 cou p 6 2 6 3 8 2 7 3 2 9 0 6 4 8 1 8 6 1 5 6 7 5 3 9 n le 1 te s 1 1 6 2 3 7 5 re od 397 72 321 93 138 72 99 11 092 31 841 11 361 641 401 135 598 625 237 612 543 156 568 726 .ts axm p e 1 t e x 1 4 2 3 4 5 in ix i 4 5 4 1 0 1 3 3 4 3 0 1 8 3 1 3 e s ts 4 1 3 1 4 1 6 1 6 7 2 6 0 4 0 1 5 8 8 3 5 s t 9 4 0 6 7 0 1 2 0 3 6 2 3 0 9 3 6 4 4 2 7 9 7 1 tr s )s l( 8 1 0 8 9 5 9 4 7 2 7 2 6 0 3 5 0 9 5 6 5 4 9 7 . c e 4 5 1 1 9 1 8 6 4 7 6 5 3 4 3 3 0 7 2 8 5 3 7 6 h tf 3 4 1 0 0 3 6 7 6 2 3 4 9 6 3 7 2 3 2 6 0 8 9 2 ec ) 8 9 4 5 0 0 1 5 5 4 2 0 4 3 6 6 9 8 3 0 4 8 0 6 k ( n o 4 1 9 2 2 1 1 2 3 4 0 4 1 3 4 5 3 5 T 0 4 4 3 2 2 0 1 6 1 5 4 4 8 1 0 1 6 6 3 9 1 5 8 4 5 5 9 3 0 3 5 0 3 8 6 0 4 5 5 0 5 4 5 3 3 9

Ring6 (100) Philo8 (100) Kanban5 (102) FMS5 (163) p l e s d o n o t e x i s t ( l e f t ) o r w h e n t h e y d o ( r i g h t ) .

PolyORB 3/3/2 MAPK 8

a F2 WFair (100) RND (100) F1 WFair (100) RND (100) T b T T T T T T le T B G T B G T B G T B G T B G T B G

p 1 2 1 1 2 2 r 3 1 0 1 6 1 7 6 6 o 4 4 1 8 0 6 2 5 1 6 1 6 d u 2 1 1 2 1 1 1 2 8 1 1 1 5 5 5 2 0 4 2 1 6 1 1 1 s A 5 7 9 7 0 3 1 9 9 6 6 :5 .t u

:5 :8 :6 :4 :0 2 to 2 1 m 7 4 3 1 6 2 3 2 a 65 62 79 67 02 29 06 63 04 59 56 52 .tr to

n : : : : : : 0 7 4 6 2 5 4 1 6 2 2 3 1 5 1 2 1 9 8 3 0 9 8 7 3 0 4 8 3 0 9 5 0 8 1 2 6 4 3 0 0 2 9 4 7 3 8 5 3 1 2 9 7 s 4 4 4 5 3 7 9 1 6 8 6 7 .t F 6 4 8 1 9 9 4 0 8 2 4 3 u 2 5 0 0 9 6 7 7 4 8 3 5 l 7 7 8 9 6 9 8 6 8 7 0 2 l

p 6 2 7 2 4 1 4 1 7 1 3 1 r 2 4 7 5 7 0 9 7 2 8 9 6 o 3 3 7 8 4 5 1 6 3 6 2 8 d

u 2 8 6 1 6 6 4 0 8 2 5 6 3 9 6 7 2 9 8 4 6 3 7 77 .tr tc 7 4 7 6 9 8 8 7 8 7 1 2 3 3 4 2 1 7 5 6 2 7 5 9 1 6 0 8 5 6 4 6 8 0 5 3 7 5 9 5 1 5 9 4 6 3 0 7 6 3 1 6 6 2 1 8 6 8 7 8 3 3 0 4 4 2 3 9 5 1 9 4 6 4 0 6 0 0 2 7 : : : : : 3 4 2 3 2 3 1 2 1 1 3 1 5 1 4 4 6 8 4 5 6 1 0 5 0 0 9 8 8 3 6 2 7 9 5 8 1 0 5 7 3 2 6 0 6 1 7 9 4 8 3 0 2 7 8 4 5 7 1 2 1 9 3 5 5 4 6 9 4 1 7 7 8 0 8 0 5 9 4 5 2 9 2 5 2 5 2 1 3 0 7 5 6 9 6 4 3 4 3 7 3 9 4 2 2 0 4 0 5 0 2

WFair (100) RND (100) WFair (100) RND (100)

Discussion

Although the state space of cases studies can be very different from random state spaces [ 17 ], a first look at our results confirms two facts already observed by Geldenhuys and Hansen using random state spaces [ 8 ]: (1) although the TA constructed from properties are usually a lot larger than BA, the average size of the full product is smaller thanks to the more deterministic nature of the TA. (2) For violated properties, the TA approach explores less states and transitions on the average than the BA.

We complete this picture by showing run times, by separating verified properties from violated properties, and by also evaluating the TGBA approach.

On verified properties, the results are very straightforward to interpret: the BA are slightly worse than the TGBA because they have to be degeneralized. In fact, the average number of acceptance conditions needed in random formulae (Table 1 and 3) is so close to 1 that the degeneralization barely changes the sizes of the automata. With weak-fairness formulae (Table 2 and 3), the number of acceptance conditions is greater, so TGBA are favored over BA. Surprisingly, both TGBA and BA, although they are not tailored to stuttering-insensitive properties like TA, appear more effective to prove that a stuttering-insensitive property is verified. In the three tables, although the full product of the TA approach is smaller than the other approaches, it has to be explored twice (as explained in section 2.3): the emptiness-check consequently explores more states and transitions. This double exploration is not enough to explain the big runtime differences. Two other subtler implementation details contribute to the time difference: – To synchronize a transition of a Kripke structure with a transition (or a state in case of stuttering) of a TA, we must compute the symmetric difference l(s) l(d) between the labels of the source and destination states. The same synchronization in the TGBA and BA approaches requires to know only the source label. Computing these labels is a costly operation in CheckPN because Petri net marking are compressed in memory to save space. Although we implemented some (limited) caching to alleviate the number of such label computation, profiling measures revealed the TA approach was 3 times slower than the TGBA and BA approaches, but that labels where computed 9 times more. – A second implementation difference, this time in favor of the TA approach, is that transitions of testing automata are labeled by elements of K, while transitions of TGBA and BA are labeled by elements of 2K . That means that once l(s) l(d) 2 K has been computed, we can use a hash table to immediately find matching transitions of the testing automaton. In the TGBA and BA implementations, we linearly scan the list of transitions of the property automaton until we find one compatible with l(s). The BA and TGBA approaches could be improved by replacing each transition labeled by an element of 2K by many transitions labeled by an elements of K, and then using a hash table, but we have not implemented it yet.

In an implementation where computing labels is cheap, the run time should be proportional to the number of transitions explored by the emptiness check, so it is important not to consider only the run time provided by our experiments.

On violated properties, it is harder to interpret these tables because the emptiness check will return as soon as it finds a counterexample. Changing the order in which non-deterministic transitions of the property automaton are iterated is enough to change the number of states and transitions to be explored before a counterexample is found: in the best case the transition order will lead the emptiness check straight to an accepting cycle; in the worst case, the algorithm will explore the whole product until it finally finds an accepting cycle. Although the emptiness check algorithms for the three approaches share the same routines to explore the automaton, they are all applied to different kinds of property automata, and thus provide different transition orders.

This ordering luckiness explains why the BA approach sometimes outperforms the TGBA approach: one very bad case is enough to bias the average case. For instance this occurred on the Philo8 model with random formulae: the worst TGBA case explored 4 times more transitions than the BA case, although the full product was twice smaller.

We believe that the TA, since they are more deterministic, are less sensible to this ordering. They also explore a smaller state space on the average. This smaller exploration is not always tied a good runtime because of the extra computation of labels discussed previously. Again, looking at the average number of transition explored by the emptiness check indicates that the TA approach would outperform the others if the computation of labels was cheap.

Finally in all of our experiments the TA approach has always found the counterexample in the first pass of the emptiness check algorithm. This supports Geldenhuys and Hansen’s claim that the second pass was seldom needed for debugging (less than 0:005% of the cases in their experiments [ 8 ]). 5

Conclusion

Geldenhuys and Hansen have evaluated the performance of the BA and TA approaches with small random Kripke structures checked against LTL formulae taken from the literature [ 8 ]. In this work, we have completed their experiments by using actual models and different kinds of formulae (random formulae not trivially verifiable, random formulae expressing weak-fairness formulae, and a couple of real formulae), by evaluating the TGBA approach, and by distinguishing violated formulae and verified formulae in the benchmark.

For verified formulae, we found that the state space reduction achieved by the TA approach was not enough to compensate for the two-pass emptiness check this approach requires. It is therefore better to use the TGBA approach to prove that a stutteringinsensitive formula is verified and TA approach in an earlier “debugging phase”.

When the formulae are violated, the TA approach usually processes less transitions than the BA approach and TGBA to find a counterexample. This approach should therefore be a valuable help to debug models (i.e. when counterexamples are expected). This is especially true on random formulae. With weak-fairness formulae, generalized automata are advantaged and are able to beat the TA on the average in 3 of our 6 examples (Philo8, Ring6, PolyORB 3/2/2).

Future work We plan to combine the ideas of TA and TGBA approaches. We believe it would be interesting to have testing automata with transition-based generalized acceptance conditions. We think the LTL translation algorithm we use to produce TGBAs could be adjusted to product such automata directly. Proceedings of CompoNet and SUMo 2011 80

References

1. G. Ciardo , G. Lüttgen, and R. Siminiceanu . Efficient symbolic state-space construction for asynchronous systems . In Proc. of ICATPN'00 , vol. 1825 of LNCS , pp. 103 - 122 . Springer.

2. J. Cichon´, A. Czubak , and A. Jasin ´ski. Minimal Büchi automata for certain classes of LTL formulas . In Proc. of DEPCOS'09 , pp. 17 - 24 . IEEE Computer Society.

3. J.-M. Couvreur . On-the-fly verification of temporal logic . In Proc. of FM'99 , vol. 1708 of LNCS, pp. 253 - 271 . Springer.

4. J.-M. Couvreur . Un point de vue symbolique sur la logique temporelle linéaire . In Actes du Colloque LaCIM 2000 , vol. 27 of Publications du LaCIM, pp. 131 - 140 . Université du Québec à Montréal, Aug. 2000 .

5. J.-M. Couvreur , A. Duret-Lutz , and D. Poitrenaud . On-the-fly emptiness checks for generalized Büchi automata . In Proc. of SPIN'05 , vol. 3639 of LNCS, pp. 143 - 158 . Springer.

6. J. Dallien and W. MacCaull. Automated recognition of stutter-invariant LTL formulas . Atlantic Electronic Journal of Mathematics , ( 1 ): 56 - 74 , 2006 .

7. A. Duret-Lutz and D. Poitrenaud . SPOT: an extensible model checking library using transition-based generalized Büchi automata . In Proc. of MASCOTS'04 , pp. 76 - 83 . IEEE Computer Society Press.

8. J. Geldenhuys and H. Hansen . Larger automata and less work for LTL model checking . In Proc. of SPIN'06 , vol. 3925 of LNCS, pp. 53 - 70 . Springer.

9. J. Geldenhuys and A. Valmari . Tarjan's algorithm makes on-the-fly LTL verification more efficient . In Proc. of TACAS'04 , vol. 2988 of LNCS, pp. 205 - 219 . Springer.

10. D. Giannakopoulou and F. Lerda . From states to transitions: Improving translation of LTL formulae to Büchi automata . In Proc. of FORTE'02 , vol. 2529 of LNCS, pp. 308 - 326 .

11. H. Hansen , W. Penczek , and A. Valmari . Stuttering-insensitive automata for on-the-fly detection of livelock properties . In Proc. of FMICS'02 , vol. 66 ( 2 ) of Electronic Notes in Theoretical Computer Science. Elsevier.

12. M. Heiner , D. Gilbert , and R. Donaldson . Petri nets for systems and synthetic biology . In Proc. of SFM'08 , vol. 5016 of LNCS, pp. 215 - 264 . Springer.

13. J. Hugues , Y. Thierry-Mieg , F. Kordon , L. Pautet , S. Barrir , and T. Vergnaud . On the formal verification of middleware behavioral properties . In Proc. of FMICS'04 , vol. 133 of Electronic Notes in Theoretical Computer Science, pp. 139 - 157 . Elsevier.

14. C. Löding . Efficient minimization of deterministic weak w-automata . Information Processing Letters , 79 ( 3 ): 105 - 109 , 2001 .

15. S. Miyano and T. Hayashi . Alternating finite automata on w-words . Theoretical Computer Science , 32 : 321 - 330 , 1984 .

16. MoVe/LRDE. The Spot home page: http://spot.lip6.fr, 2011 .

17. R. Pelánek . Properties of state spaces and their applications . International Journal on Software Tools for Technology Transfer (STTT) , 10 ( 5 ): 443 - 454 , 2008 .

18. I. Pyarali, M. Spivak , R. Cytron , and D. C. Schmidt . Evaluating and optimizing thread pool strategies for RT-CORBA . In Proc. of LCTES'00 , pp. 214 - 222 . ACM.

19. K. Y. Rozier and M. Y. Vardi . LTL satisfiability checking . In Proc. of SPIN'07 , vol. 4595 of LNCS, pp. 149 - 167 . Springer.

20. S. Schwoon and J. Esparza . A note on on-the-fly verification algorithms . In Proc. of TACAS'05 , vol. 3440 of LNCS. Springer.

21. R. Sebastiani and S. Tonetta . "more deterministic" vs. "smaller" Büchi automata for efficient LTL model checking . In Proc. of CHARME'03 , vol. 2860 of LNCS, pp. 126 - 140 . Springer.

22. H. Tauriainen . Automata and Linear Temporal Logic: Translation with Transition-based Acceptance . PhD thesis , Helsinki University of Technology, Espoo, Finland, Sept. 2006 .

23. M. Y. Vardi . An automata-theoretic approach to linear temporal logic . In Proc. of Banff '94 , vol. 1043 of LNCS, pp. 238 - 266 . Springer.