Fundamenta Informaticae - Volume 94, issue 3-4

Article Type: Other

DOI: 10.3233/FI-2009-131

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. i-ii, 2009

Authors: Darondeau, Philippe | Koutny, Maciej | Pietkiewicz-Koutny, Marta | Yakovlev, Alex

Article Type: Research Article

Abstract: The unconstrained step semantics of Petri nets is impractical for simulating and modelling applications. In the past, this inadequacy has been alleviated by introducing various flavours of maximally concurrent semantics, as well as priority orders. In this paper, we introduce a general way of controlling step semantics of Petri nets through step firing policies that restrict the concurrent behaviour of Petri nets and so improve their execution and modelling features. In a nutshell, a step firing …policy disables at each marking a subset of enabled steps which could otherwise be executed. We discuss various examples of step firing policies and then investigate the synthesis problem for Petri nets controlled by such policies. Using generalised regions of step transition systems, we provide an axiomatic characterisation of those transition systems which can be realised as reachability graphs of Petri nets controlled by a given step firing policy. We also provide two different decision and synthesis algorithms for PT-nets and step firing policies based on linear rewards of steps, where the reward for firing a single transition is either fixed or it depends on the current net marking. The simplicity of the algorithms supports our claim that the proposed approach is practical. Show more

Keywords: Petri nets, step firing policy, step transition system, regions, synthesis problem

DOI: 10.3233/FI-2009-132

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 275-303, 2009

Authors: Bonchi, Filippo | Brogi, Antonio | Corfini, Sara | Gadducci, Fabio

Article Type: Research Article

Abstract: Web services represent a promising technology for the development of distributed heterogeneous software systems. In this setting, a major issue is to establish whether two services can be used interchangeably in any context. To this aim, our paper first briefly reviews the results contained in a recent article by the same authors, where a suitable notion of behavioural equivalence for Web services was introduced. Our work then extends those results, in order to account for ontologybased …service specifications. Next, a concrete example scenario – a car rental system – is presented, and it is then used to illustrate how the equivalence between services can be fruitfully employed for correctly addressing two prominent, modularity-related problems: the publication of correct service specifications and the replaceability of (sub)services. Show more

DOI: 10.3233/FI-2009-133

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 305-330, 2009

Authors: Bergenthum, Robin | Mauser, Sebastian | Lorenz, Robert | Juhas, Gabriel

Article Type: Research Article

Abstract: In this paper we propose two new unfolding semantics for general Petri nets combining the concept of prime event structures with the idea of token flows developed in [13]. In contrast to the standard unfolding based on branching processes, one of the presented unfolding models avoids to represent isomorphic processes while the other additionally reduces the number of (possibly nonisomorphic) processes with isomorphic underlying runs. We show that both the proposed unfolding models still represent the …complete partial order behavior. Moreover, in both cases it is possible to construct complete finite prefixes for bounded nets through applying the known theory of cut-off events. In particular, canonical prefixes w.r.t. a given cutting context can be defined and computed for bounded nets. We present implementations of construction algorithms for complete finite prefixes of both the unfolding models. Experimental results show that the computed prefixes are much smaller and can be constructed significantly faster than in the case of the standard unfolding. Show more

Keywords: Unfolding, Prime Event Structure, Canonical Prefix, Cutting Context, Petri Net

DOI: 10.3233/FI-2009-134

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 331-360, 2009

Authors: Kristensen, Lars M. | Fleischer, Paul

Article Type: Research Article

Abstract: The Generic Access Network (GAN) architecture is defined by the 3rd Generation Partnership Project (3GPP) and allows telephone services, such as SMS and voice-calls, to be accessed via Internet Protocol (IP) networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN specification relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol (IKEv2) to provide encryption across IP networks, …and thus avoid compromising the security of the telephone networks. The detailed usage of these two Internet protocols (IPSec and IKEv2) is not fully described in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a detailed GAN scenario which describes how IPSec and IKEv2 are to be used during the connection establishment procedure. This paper presents an industrial project where Coloured Petri Nets (CPNs) were used to specify and validate the detailed GAN scenario considered by TietoEnator. Show more

Keywords: Modelling and Validation, Coloured Petri Nets, State Space Methods, Model Checking, Protocol Engineering, Concurrrent Systems, Internet Protocols

DOI: 10.3233/FI-2009-135

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 361-386, 2009

Authors: van derWerf, J.M.E.M. | van Dongen, B.F. | Hurkens, C.A.J. | Serebrenik, A.

Article Type: Research Article

Abstract: The research domain of process discovery aims at constructing a process model (e.g. a Petri net) which is an abstract representation of an execution log. Such a model should (1) be able to reproduce the log under consideration and (2) be independent of the number of cases in the log. In this paper, we present a process discovery algorithm where we use concepts taken from the language-based theory of regions, a well-known Petri net research area. …We identify a number of shortcomings of this theory from the process discovery perspective, and we provide solutions based on integer linear programming. Show more

DOI: 10.3233/FI-2009-136

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 387-412, 2009

Authors: Hamez, Alexandre | Thierry-Mieg, Yann | Kordon, Fabrice

Article Type: Research Article

Abstract: Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data …structures. Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, flexibility to a user defining a symbolic transition relation. We show in this paper how, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We build as an example an SDD model-checker for a compositional formalism: Instantiable Petri Nets (IPN). IPN define a type as an abstract contract. Labeled P/T nets are used as an elementary type. A composite type is defined to hierarchically contain instances (of elementary or composite type). To compose behaviors, IPN use classic label synchronization semantics from process calculi. With a particular recursive folding SDD are able to offer solutions for symmetric systems in logarithmic complexity with respect to other DD. Even in less regular cases, the use of hierarchy in the specification is shown to be well supported by SDD. Experimentations and performances are reported on some well known examples. Show more

Keywords: Hierarchical Decision Diagrams, Model Checking, Saturation

DOI: 10.3233/FI-2009-137

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 413-437, 2009

Authors: Meyer, Roland | Khomenko, Victor | Strazny, Tim

Article Type: Research Article

Abstract: We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of π-Calculus, into Petri nets, which are subsequently used formodel checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, a subset of finite control processes, for which our translation yields safe Petri nets, and show …that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system. Show more

Keywords: finite control processes, safe processes, π-Calculus, mobile systems, model checking, Petri net unfoldings

DOI: 10.3233/FI-2009-138

Citation: Fundamenta Informaticae, vol. 94, no. 3-4, pp. 439-471, 2009