Fundamenta Informaticae - Volume 88, issue 3

Article Type: Other

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. i-ii, 2008

Authors: Boyer, Marc | Roux, Olivier H.

Article Type: Research Article

Abstract: In this paper, we consider safe Time Petri Nets where time intervals (strict and large) are associated with places (P-TPN), arcs (A-TPN) or transitions (T-TPN). We give the formal strong and weak semantics of these models in terms of Timed Transition Systems. We compare the expressiveness of the six models w.r.t. (weak) timed bisimilarity (behavioral semantics). The main results of the paper are : (i) with strong semantics, A-TPN is strictly more expressive than P-TPN and …T-TPN ; (ii) with strong semantics P-TPN and T-TPN are incomparable ; (iii) T-TPN with strong semantics and T-TPN with weak semantics are incomparable. Moreover, we give a complete classification by a set of 9 relations explained in Fig. 19 (p. 247). Show more

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 225-249, 2008

Authors: Lazić, Ranko | Newcomb, Tom | Ouaknine, Joël | Roscoe, A.W. | Worrell, James

Article Type: Research Article

Abstract: We study data nets, a generalisation of Petri nets in which tokens carry data from linearlyordered infinite domains and in which whole-place operations such as resets and transfers are possible. Data nets subsume several known classes of infinite-state systems, including multiset rewriting systems and polymorphic systems with arrays. We show that coverability and termination are decidable for arbitrary data nets, and that boundedness is decidable for data nets in which whole-place operations are restricted …to transfers. By providing an encoding of lossy channel systems into data nets without whole-place operations, we establish that coverability, termination and boundedness for the latter class have non-primitive recursive complexity. The main result of the paper is that, even for unordered data domains (i.e., with only the equality predicate), each of the three verification problems for data nets without whole-place operations has non-elementary complexity. Show more

Keywords: Petri nets, infinite-state systems, program verification, computational complexity

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 251-274, 2008

Authors: Ganty, Pierre | Raskin, Jean-François | Van Begin, Laurent

Article Type: Research Article

Abstract: Current algorithms for the automatic verification of Petri nets suffer from the explosion caused by the high dimensionality of the state spaces of practical examples. In this paper, we develop an abstract interpretation based analysis that reduces the dimensionality of state spaces that are explored during verification. In our approach, the dimensionality is reduced by trying to gather places that may not be important for the property to establish. If the abstraction that is obtained is …too coarse, an automatic refinement is performed and a more precise abstraction is obtained. The refinement is computed by taking into account information about the inconclusive analysis. The process is iterated until the property is proved to be true or false. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 275-305, 2008

Authors: Koutny, Maciej | Pietkiewicz-Koutny, Marta

Article Type: Research Article

Abstract: We investigate the synthesis problem for ENCL-systems, defined as Elementary Net Systems extended with context (inhibitor and activator) arcs and explicit event localities. Since colocated events are meant to be executed synchronously, the behaviour of such systems is captured by step transition systems, where arcs are labelled by sets of events rather than by single events. We completely characterise transition systems generated by ENCL-systems after extending the standard notion of a region – defined as a …certain set of states – with explicit information about events which, in particular, are responsible for crossing its border. As a result, we are able to construct, for each such transition system, a suitable ENCL-system generating it. Show more

Keywords: theory of concurrency, Petri nets, elementary net systems, localities, net synthesis, step sequence semantics, structure and behaviour of nets, theory of regions, transition systems, inhibitor arcs, activator arcs, context arcs

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 307-328, 2008

Authors: Rosa-Velardo, Fernando | de Frutos-Escrig, David

Article Type: Research Article

Abstract: We study the relationship between name creation and replication in a setting of infinitestate communicating automata. By name creation we mean the capacity of dynamically producing pure names, with no relation between them other than equality or inequality. By replication we understand the ability of systems of creating new parallel identical threads, that can synchronize with each other. We have developed our study in the framework of Petri nets, by considering several extensions of P/T nets. …In particular, we prove that in this setting name creation and replication are equivalent, but only when a garbage collection mechanism is added for idle threads. However, when simultaneously considering both extensions the obtained model is, a bit surprisingly, Turing complete and therefore, more expressive than when considered separately. Show more

Keywords: Petri nets, pure names, infinite state systems, decidability, multithreading, security, choreography

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 329-356, 2008

Authors: Billington, Jonathan | Vanit-Anunchai, Somsak

Article Type: Research Article

Abstract: The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build …complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed. Show more

Keywords: Internet Protocols, DCCP, Coloured Petri Nets, Formal Specification, Evolutionary Modelling

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 357-385, 2008

Authors: van Hee, Kees | Serebrenik, Alexander | Sidorova, Natalia | van der Aalst, Wil

Article Type: Research Article

Abstract: Most information systems that are driven by processmodels (e.g., workflowmanagement systems) record events in event logs, also known as transaction logs or audit trails. We consider processes that not only keep track of their history in a log, but also make decisions based on this log. To model such processes we extend the basic Petri net framework with the notion of history and add guards to transitions evaluated on the process history. We show that some …classes of historydependent nets can be automatically converted to classical Petri nets for analysis purposes. Some of these classes are characterized by the form of the guards (e.g., LTL+Past guards), while others by restrictions on the underlying classical Petri net. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 3, pp. 387-409, 2008