Symbolic BDD-based verification techniques successfully tackle combinatorial explosion in many cases. However, the models to be verified become increasingly larger and more complex, including - for instance - additional features like quantitative requirements and/or a very high number of components. The need to improve performances for verification tools thus remains a challenge. In this work, we extend the framework of Instantiable Transition Systems in order to (i) take into account time constraints in a model and (ii) capture the symmetry of instances which share a common structure, thus significantly increasing the power of our tool. For point (i), we implement timed models with discrete time semantics and for (ii), we introduce scalar sets as a special form of composition. We also report on experiments including comparisons with other tools. The results show a good scale up for our approach.
Context. Model checking is now widely used as an automatic and exhaustive way to verify complex systems. However, this approach suffers from an intrinsic combinatorial explosion, due to both a high number of synchronized components and a high level of expressivity in these components.
Among the different methods proposed to tackle the problem, using decision
diagrams [
With respect to the expressivity issue, we consider the particular problem of introducing explicit time constraints in the components of a system. In this modeling step, the choice of a time domain is important, impacting on the size of the resulting model, the class of properties which can be verified and the performances of the verification.
During the last twenty years, numerous variants of dense time models have been
extensively studied. Among them, Time Petri Nets [
If we now consider a growing number of timed components, the two problems of expressivity and size occur together, but the symbolic DBM encoding only applies to time zones and does not concern the discrete part of the states. Furthermore, the union of DBM may not be convex, thus cannot be encoded as a DBM, so mixing DBM technology with a symbolic encoding of discrete states is difficult.
Directly interpreting models over a discrete time domain is usually easier to handle
than dense time because mechanisms elaborated for model checking of discrete systems
can be reused, even though state space explosion can be worse. The relations between
dense and discrete time analysis have been discussed for various models, showing that,
in many cases, discrete time computation is sufficient to preserve reachability or
timebounded properties [
Contribution. In this work, we modify and extend the framework of Instantiable
Transition Systems proposed in [
We experiment on two classical benchmark examples combining both features, and compare the performances with those of several other tools handling discrete or dense time, showing gains of several orders of magnitude.
Outline. We first recall the definition and semantics of Time Petri Nets in Section 2, along with the train crossing example. Section 3 describes the Instantiable Transition Systems framework with the additional features and briefly presents the encoding technique. Finally, in Section 4, we give the performances obtained with our prototype implementation, with comments and comparisons. 2
To handle time constraints, we propose to use discrete time models. As mentioned in the introduction, this can lead to larger state spaces due to sensitivity to constants. However, the main advantage of this approach is to reduce the problem of timed verification to a plain event-based verification.
Let us first recall the classical definition of Discrete Timed Transition Systems (DTTS), where all standard actions (from some set A) are considered instantaneous and delay transitions are added, in a time domain restricted to the set N of natural numbers. Without loss of generality, we consider only delay steps of exactly one time unit (special action 1 below). Having a single basic operation to handle time delay is more effective in a symbolic setting than attempting to find at each step the maximal integer delay consistent with synchronization of several components in a set of states. Definition 1 (DTTS). Let A be a set of action labels and let 1 ∈/ A be a special action representing a one time unit delay. A Discrete Timed Transition System over A is a tuple T = hS, s0, A, →−i where S is a set of states, s0 ∈ S is the initial state, and →−⊆ S × (A ⊎ {1}) × S is the transition relation (⊎ stands for disjoint union).
We consider the model of Time Petri Nets (TPN) with discrete time semantics.
TPN are used to compactly model concurrent timed behaviors. Besides, regarding the
problem of marking reachability, discrete time semantics capture all possible behaviors
[
We choose an extended definition of TPN because this leads to easier and more
compact modeling abilities. There is a quite strong community of extended TPN users
and our definition below captures a wide superset of what is understood as TPN in the
literature: we consider an enabling predicate and a firing function as syntactic
requirements, instead of defining various sorts of arcs. This homogeneously subsumes
extensions such as reset arcs, read (or test) arcs, inhibitor arcs, and even non-deterministic
extensions like hyper-arcs (because fire maps to 2NPl ), which are offered for instance by
the Rome´o tool [
Definition 2 (TPN). A Time Petri Net is a tuple N = hPl, Tr, A, enabled, fire, ℓ, m0, α, βi where: – Pl is a finite set of places, Tr is a finite set of transitions (with Pl ∩ Tr = 0/ ), – A is a finite set (alphabet) of action labels which contains a distinguished local label ⊤, – enabled : NPl × Tr 7→ {true, f alse} is an enabling predicate, fire : NPl × Tr 7→ 2NPl is a transition firing function, ℓ : Tr 7→ A is a labeling function, – m0 ∈ NPl is the initial marking of the net, – α : Tr 7→ N and β : Tr 7→ N ∪ {∞} are functions satisfying ∀t ∈ Tr, α(t) ≤ β(t) called respectively earliest (α) and latest (β) transition firing times.
For instance, standard Place/Transition nets are usually defined using pre (noted Pre) and post (noted Post) functions : Pl × Tr 7→ N. Then, for a marking m ∈ NPl and a transition t ∈ Tr, enabling is defined by enabled(m,t) iff ∀p ∈ Pl, m(p) ≥ Pre(p,t) and transition firing by fire(m,t) = {m′} with ∀p ∈ Pl, m′(p) = m(p) − Pre(p,t) + Post(p,t). Inhibitor arcs Inh and test arcs Test are defined similarly and add enabling conditions to a transition: enabled(m,t) iff ∀p ∈ Pl, m(p) < Inh(p,t)∧m(p) ≥ Test(p,t). Note that the enabling predicate only considers markings while timing conditions are defined separately. In definition 2, transitions are equipped with labels for further composition of nets (see Section 3).
The classical train crossing example [
In
[
Ex
[
App far Exit [0,0] public local ( )
Definition 3 (Discrete Time Semantics of a TPN). For a Time Petri Net N = hPl, Tr, A, enabled, fire, ℓ, m0, α, βi, the semantics is a transition system S N = hS, s0, A ∪ {1}, →i where: and ∀t′ ∈ Tr, v′(t′) =
0 otherwise – S = NPl × NTr is the set of states. An element s of S is a pair s = hm, vi, where m is the place marking and v is the transition clock valuation. – s0 = hm0, 0i, where the tuple 0 corresponds to the value 0 for all transition clocks. – →−⊆ S × (A ⊎ {1}) × S is the transition relation defined for states hm, vi, hm′, v′i by: The discrete transition relation: hm, vi →−a hm′, v′i iff there is a transition t ∈ Tr such that ℓ(t) = a ∧ enabled(m, t) ∧ v(t) ≥ α(t) and m′ ∈ fire(m, t) ( v(t′) if enabled(m′, t′) ∧ t 6= t′ The delay transition relation:
v(t) otherwise 1 hm, vi −→ hm′, v′i iff m′ = m and for all t ∈ Tr, enabled(m,t) =⇒ v(t) < β(t) (urgent clocks prevent elapse) v(t) + 1 if enabled(m′,t) ∧ β(t) 6= ∞ (normal elapse) v′(t) = v(t) + 1 if enabled(m′,t) ∧ β(t) = ∞ ∧ v(t) < α(t) (only progress up to α)
Note that we use here atomic semantics and a newly disabled criterion to reset disabled transition clocks, ensuring a disabled transition has a clock value set to 0.
The rule (only progress up to α) allows us to handle the infinity problem due to unbounded latest firing times (e.g. for transitions with firing interval [α(t), ∞[). With this strategy, we do not let clocks of the corresponding transitions progress up to more than their lowest significant value α(t). The behavior can thus be accurately represented on a finite support. If the logic used to express properties involves atomic propositions with test of clock values, the rule can be relaxed to let the clock progress be tracked up to the highest value tested in the logic, rather than α(t). 3
This section defines Instantiable Transition Systems (ITS), a framework designed to
exploit the hierarchical characteristics of SDD [
ITS describe a minimal Labeled Transition System (LTS) style formalism using notions of type and instance to emphasize locality of actions and to exploit the similarity of instances of a given type. The composition mechanism is based solely on transition synchronizations (no explicit shared memory or channel).
Notations: The set of finite words over a finite alphabet A is denoted by A⋆, with ε for the empty word and · (or no symbol) for the concatenation operation. We denote by z.X , z.Y . . . the element X (resp. Y . . . ) of a tuple z = hX ,Y, · · ·i.
Definition 4 sets an abstract contract or interface that must be implemented by concrete ITS types.
Definition 4 (ITS Semantics). An ITS type is a tuple τ = hS, A, Locals, Succi where: – S is a set of states; A is a finite set of public action labels; – Locals : S 7→ 2S is a local successors function; – Succ : S × A⋆ 7→ 2S is a transition function satisfying: ∀s ∈ S, Succ(s, ε) = {s}. Let T be a set of ITS types. An ITS instance i is defined by an ITS type type(i) ∈ T and a set of states type(i).S.
Reachability: A state s′ is reachable in an instance i from the state s0 iff ∃s1, . . . sn ∈ type(i).S such that s′ = sn and ∀1 ≤ j ≤ n, s j ∈ type(i).Locals(s j−1).
The two functions Locals and Succ are used for different purposes: Locals represents moves that may occur within an instance autonomously or independently from the rest of the system. Hence it returns states reachable through occurrences of local events. The function Succ produces successors by explicitly synchronizing actions via a word over the alphabet of action labels. Synchronizing on an empty word leaves the state of the instance locally unchanged. Note that Succ is the only way to control the behavior of a (sub)system from outside.
Remark 1. The transition relation of a full system can only be defined in terms of subsystem synchronizations using Succ and of independent local behaviors. A full system is defined by a single instance of a particular type in a specific initial state. Because it is self-contained (there is no notion of environment that could trigger Succ) reachability only depends on the definition of Locals.
Remark 2. Apart from distinguishing the special time delay action label 1, a DTTS is thus simply a labeled transition system and is immediately compatible with the ITS framework, if the DTTS has a local label ⊤. Interpreting timed models such as Time Petri Nets (but also Timed Automata) over discrete time makes it possible to use the ITS model-checking engine, and also profit from the Composite and Scalar set definitions below to build compositional models.
We now define a composite ITS type, designed to offer support for the hierarchical
composition of ITS instances. A version of a composite type was presented in [
Notations: Given a cartesian product Z = Z1 × · · · × Zn of sets Z1, · · · , Zn, we denote by πi the projection operator Z 7→ Zi. For a set I = {i1, . . . , in} of ITS instances (where an arbitrary order is chosen), SI is the set type(i1).S × . . . × type(in).S and AI is the set type(i1).A⋆ × . . . × type(in).A⋆. Cardinality of I is denoted by |I|.
Definition 5 (Composite). A composite is a tuple C = hI, Sync, A, λi where: – I is a finite set of ITS instances, said to be contained by C. We further require that the type of each ITS instance already exists when defining I, in order to prevent circular or recursive type definitions. – Sync ⊂ AI is the finite set of synchronizations; A is a set of action labels, which contains the label ⊤ and λ : Sync 7→ A is the labeling function Notations: The next state function NextI : SI × AI 7→ 2SI , used in definition 6 below, is defined for s, s′ ∈ SI and σ ∈ AI by: s′ ∈ NextI (s, σ) iff ∀i ∈ I, πi(s′) ∈ type(i).Succ(πi(s), πi(σ)) Definition 6 (ITS Semantics of a Composite). The ITS type τ = hS, A, Locals, Succi corresponding to a composite C = hI, Sync, A′, λi, is defined by: – S = SI ; A = A′ \ {⊤}; – Locals : S 7→ 2S is defined for s, s′ ∈ S by: s′ ∈ Locals(s) iff
∃i ∈ I, πi(s′) ∈ type(i).Locals(πi(s)) ∧ ∀ j ∈ I, j 6= i, π j(s′) = π j(s) or ∃σ ∈ Sync, λ(σ) = ⊤, s′ ∈ NextI (s, σ) – Succ : S × A⋆ 7→ 2S is defined for s, s′ ∈ S, w = a1 · · · an ∈ A⋆ by: s′ ∈ Succ(s, w) iff ∃σ1, . . . , σn ∈ Sync, ∃s0, . . . , sn ∈ S, ∀ j ∈ [1..n], λ(σ j) = a j ∧ s j ∈ NextI (s j−1, σ j) ∧ s0 = s ∧ sn = s′.
Definition 6 thus describes an implementation of the generic ITS type contract. It contains either elementary instances (such as LTS, or as we will use later in this paper, a discrete timed transition system), or inductively other instances of composite nature.
Locals(s) is defined as the set of states resulting from the action of Locals in any nested instance (without affecting the other instances), or states reachable from s through the occurrence of any synchronization associated to the local label ⊤.
Succ(s, w) is obtained by composing the effects of each label a in the word w using the cartesian product. So the use of a word can force system progression by firing several action labels in an atomic sequence. Firing an action label corresponds to arbitrarily choosing a synchronization that bears this label, and firing it.
t0: train t1: train
App ε
ε App
ε Exit 1 1 3.2
While the definition of an ITS composite permits hierarchical modeling, the notion
of Scalar Set ITS type, where the synchronizations are defined in a parametric way,
deals with “regular” or symmetrically composed systems. This definition is not more
expressive than the one for a composite but it allows us to build several equivalent
composite representations of a system (see Figures 7 and 8), with a possible impact
on performances. We thus offer a way of describing symmetric models, so that the
manually built recursive encodings presented in [
Definition 7 (Scalar Set). A scalar set is a tuple S = hτ, n, s0, D,CSynci where: – τ = hS, A, Locals, Succi is the ITS type of the contained instances. – n ∈ N is the the number of instances – s0 ∈ τ.S is the initial state of the instances – D is a subset of τ.A × {ANY, ALL} × {public, private}, called the set of delegates, – CSync is a subset of τ.A × τ.A × {public, private}, called the set of circular synchronizations.
A scalar set can thus be seen as a subclass of composite, containing n identical instances of a type τ, and offering only two ways of synchronizing them, ANY and ALL. A delegate d = ha,t, vi of type t = ANY affects exactly one of the contained instances, chosen arbitrarily. In other words, an ANY delegate maps to n synchronization lines: each line affects a single instance with action a. In contrast, a delegate of type t = ALL targets all contained instances simultaneously, and maps to a single synchronization line of as. The visibility v of a delegate gives the labeling function of the composite: the label of the resulting synchronization lines is ⊤ if private is used, or action a otherwise.
For instance, the train group model for 2 trains (see Figure 4) can be expressed as the following scalar set: hTrain, 2, s0, {hApp, ANY, publici, hExit, ANY, publici, h1, ALL, publici}, 0/ i.
A scalar set represents a regular model pattern and produces a homogeneous
representation of parametric models. Furthermore, because this pattern is very constrained,
different semantically equivalent encodings can be considered at the SDD level. In
particular, as introduced in [
Circular synchronizations (CSync in Def. 7) capture another frequent composition pattern: topological rings, where a component synchronizes with its successor in the ring. For instance, Dijkstra’s classical dining philosophers example for N philosophers can be written as: hPhiloFork, N, s0, 0/ , {hgetFork, getLe f t, privatei, hputFork, f inishEating, privatei}i. In this set, PhiloFork is a composite of a Fork and a Philosopher, getFork and putFork are actions that take or return the fork, getLeft and finishEating are actions where the Philosopher acquires or releases his left neighbor’s fork. t0: train t1: train t2: train t3: train
App ε ε ε ε App ε ε ε ε App ε ε ε ε App
ε Exit ε ε ε ε Exit ε ε ε ε Exit 1 1 1 1 λ App App App App
1
In [
With these additional definitions of scalar set, the encoding strategy can be configured by the user at run time, by simply setting an option. Two parameters guide the encoding: The width gives the number of variables at any given level of composite, and the depth gives the number of levels of hierarchy or nesting introduced. The user can choose to bound one or the other and select the more efficient. For instance the flat encoding of Fig. 7 has width 4 and depth 1, while the encoding of Fig. 8 has width 2 and depth 2.
We thus generalize for easy reuse the very favorable encodings from [
The ITS tools can be used for modeling and analysis of ITS specifications. The graphical front-end is an Eclipse plugin built upon Coloane (configure coloane.lip6.fr/nightupdates in eclipse update sites), thus runs on all platforms. The actual analysis tools are provided on ddd.lip6.fr as pre-compiled binaries for common platforms (Linux, MacOS, Windows).
In the modeling environment, TPN can be used as building bricks to define ITS instances. The tool currently features import/export functionality for both Rome´o and Tina formats, full modeling capability, the ability to ”flatten” a composite ITS definition to an equivalent TPN, use of variables in arc labels and time constraints, and CTL model-checking for analysis. To jump-start new users, both examples used in this paper are available directly through the ”New->Example” eclipse menu. Figure 9 shows else end else end
return 0/ return Id
Algorithm 1: Part of the encoding for 1 transition. a screenshot of the modeling tool, where composite and scalar types use a graphical syntax.
The analysis engine of the tool uses the powerful hierarchical set decision diagram (SDD) technology. SDD are a variant of reduced decision diagrams producing a compact representation of very large state spaces. Their main characteristic exploited in this work is that edges of the decision diagram can bear references to SDD, allowing a hierarchical encoding of the state-space.
The semantics of TPN and composite ITS are directly expressed by operations acting on the SDD. The delay transition 1 uses a conjunction (over all transitions) of if-then-else constructs to increment the currently enabled clocks or forbid time elapse if a latest firing time has been reached. An informal presentation is given for this 1 operation on transition ti by Algorithm 1: returning 0/ indicates there are no successors, while returning Id indicates that with respect to this transition no updates to the current state are needed. This algorithm is slightly adapted to take into account infinite latest firing times, as explained in the discrete TPN semantics paragraph above. 4
Fischer’s protocol. This protocol is modeled using two elementary TPN. We use reset (respectively read) arcs, according to their classical definition, which means they allow to reset (resp. check the non-emptiness) the marking of the associated place. The process type (Fig.10) represents the behavior of a single process. The resource type (Fig. 11) is used to block processes in the idle state during the execution of the protocol (i.e. at least one process has already reached wait or cs).
Then, we build a process group (Fig. 12) containing a scalar set of processes in the system, similarly to the approach used for the train group. Finally, this group of processes is composed with an instance of the resource according to the synchronizations defined in Fig. 13. Note (line 3) the use of a word in A⋆ for synchronisation: for a given process to fire Myturn, we need to first reset all go places of the processes, and synchronously Reset the state of the resource.
In view of these performances, we now compare Rome´o/SDD with existing tools.
Dense Time, Explicit data structures. The standard approach for verification of timed
models relies on difference bounded matrices (DBMs), an efficient data structure to
represent time zones under dense time time hypothesis. Its efficiency has led to the
development of several verification tools (so-called timed model-checkers) such as TINA [
Rome´o suffers from the discrete state space explosion (i.e. in number of classes). It was stopped after one day of CPU and consumed a high amount of memory. The performances of UPPAAL without symmetries (not reported due to lack of space in the paper) are similar to those of Rome´o’s. Underlying technology is DBM in both cases.
Thanks to the symmetry management, UPPAAL/sym copes very well with these regular models. It uses a canonization procedure which is costly in time, but can in favorable cases represent only a fraction of the state space. It significantly outperforms all the other tools tested except our own tool. However, computation time grows quicker than memory consumption (possibly due to the canonization complexity) and becomes the limiting factor. idle cs
Deny[0,0]
wait
go waitcs
[
hWantcs, ANY, publici, hMyturn, ANY, publici, hProcess, N, s0, hEndcs, ANY, publici, , 0/ i.
hhR1e,AseLt,LA, LpuLb,lpiuciblici,
Dense Time, Symbolic data structures. To bring the benefits of BDD technology to
model-checking of TA, many fully symbolic encodings that use dedicated BDD-like
data structures have been proposed (e.g. DDD [
We compare in this category to the tool RED, which builds a zone graph using
Clock Restriction Diagrams in a fully symbolic approach. The fully symbolic approach
implemented in RED is fast in CPU time, but also grows very fast in memory. This is
consistent with reports from experiments with RED [
Among the different tools based on standard BDD structures and discrete time
semantics, SMI (based on Kronos) [
However, comparison is difficult because both SMI and Rabbit are old prototypes no longer maintained (current distribution of Rabbit is from 2002). The input of Rabbit is a variant on a classical product of TA, but without the hierarchical characteristics of ITS. Rabbit measures are not reported in the table because we were unable to operate the tool on the Train model. The Fischer model which is part of Rabbit distribution was managed up to 128 processes in 1587 seconds with 842 MB of memory, which is a good result. We could not experiment further with this tool because it does not allow the use of more than 880MB of memory.
Impact of Scalar set. Rome´o/SDD relies on similar principles as Rabbit: discrete time and a fully symbolic representation. The combinatorial explosion due to discrete time is balanced by the efficiency of SDD encoding: over 10500 states can be represented.
Rome´o/SDD is able to handle models up to much higher parameter values than the
other tools. This is due to the use of ITS/SDD that provide: (i) automatic saturation, (ii)
shared representation of subsystems and (iii) the cartesian product style definition of the
transition relation (involving composition of sums). Various strategies (see [
For the Fischer model, we used a setting with a recursive definition of hierarchy in the system bounded by 12 variables per level. In other words, the depth is left unbounded while the width is at most 12. The standard flat setting (depth = 1) was able to reach 200 processes while a setting with groups of about 10 processes let us reach 400 processes (depth fixed at 2, 40 groups of ten process).
Although experimentation on industrial case studies remains to be done, this benchmark shows that appropriate data structures applied to discrete time can deal with models that could not be analyzed before due to combinatorial explosion in time and/or memory. 5
This work proposes an approach to compute the state space for a large number of discrete timed components, which relies on hierarchical set decision diagrams (SDD) and scalar sets defined in the ITS framework. It allows a hierarchical definition of a timed system, and offers an efficient fully symbolic reachability engine thanks to the automatic activation of saturation. Because of its generality, ITS can be reused to encode any formalism with discrete time semantics and mix several timed models within the same specification while enabling efficient state space generation.
Performance comparisons with reference tools, for both discrete and dense time, show gains of several orders of magnitude. This significant improvement is due to our fully symbolic encoding, instead of a classical symbolic approach for time zones only.
SDD and ITS are both available as C++ libraries under the terms of GNU LGPL, at http://ddd.lip6.fr. A new version of Rome´o integrating a SDD engine will soon be available. A front-end to build TPN and their composition is already provided within the Coloane modeling environment. We are currently working at providing full discrete temporal logic model-checking capabilities on top of this reachability computation, with a focus on TCTL. Proceedings of CompoNet and SUMo 2011 32