Fundamenta Informaticae - Volume 37, issue 3

Authors: Burkhard, Hans-Dieter | Starke, Peter | Czaja, Ludwik

Article Type: Other

DOI: 10.3233/FI-1999-37308

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. i-ii, 1999

Authors: Baar, Thomas | Kindler, Ekkart

Article Type: Research Article

Abstract: The Distributed Algorithms Working Notation (DAWN) was designed for modelling and verifying algorithms in an intuitive way. Nevertheless, DAWN proofs are formal. In this paper, we show that it is possible to check correctness of a DAWN proof fully automatically: For each step in a DAWN proof, we can generate a set of proof obligations which can automatically be checked by help of automated theorem provers. The verification tool ILF provides a uniform interface to many theorem provers—which makes it an ideal partner for DAWN and a basis for building a DAWN-tool.

Keywords: Automated Theorem Provers, Distributed Algorithms, Verification, Z

DOI: 10.3233/FI-1999-37301

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 201-211, 1999

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: Synthesis of elementary Petri net from a given process language (given by an expression in an algebra resembling the algebra of regular languages) is posed and solved. A necessary and sufficient condition for existence of such net is proved.

Keywords: Petri net, process, process language algebra, synthesis problems

DOI: 10.3233/FI-1999-37302

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 213-223, 1999

Authors: Farwer, Berndt

Article Type: Research Article

Abstract: Linear Logic [4] has been shown to incorporate a fragment suitable for representing P/T-nets and giving a semantics to the computations of such nets (e.g. [1], [6], [2]). This result is generalised to coloured nets. Furthermore a new kind of high-level nets is defined: Linear Logic Petri Nets (LLPN). These nets are used as an intuitive semantics to well-known and new high-level net concepts like object systems ([8], [12], and [10]) and agent orientation.

Keywords: Linear Logic, Petri nets, object systems, concurrency

DOI: 10.3233/FI-1999-37303

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 225-246, 1999

Authors: Heljanko, Keijo

Article Type: Research Article

Abstract: McMillan has presented a deadlock detection method for Petri nets based on finite complete prefixes (i.e. net unfoldings). The approach transforms the PSPACE-complete deadlock detection problem for a 1-safe Petri net into a potentially exponentially larger NP-complete problem of deadlock detection for a finite complete prefix. McMillan devised a branch-and-bound algorithm for deadlock detection in prefixes. Recently, Melzer and Römer have presented another approach, which is based on solving mixed integer programming problems. In this work it is shown that instead of using mixed integer programming, a constraint-based logic programming framework can be employed, and a linear-size translation from deadlock …detection in prefixes into the problem of finding a stable model of a logic program is presented. As a side result also such a translation for solving the reachability problem is devised. Correctness proofs of both the translations are presented. Experimental results are given from an implementation combining the prefix generator of the PEP-tool, the translation, and an implementation of a constraint-based logic programming framework, the smodels system. The experiments show the proposed approach to be quite competitive, when compared to the approaches of McMillan and Melzer/Römer. Show more

Keywords: Verification, Petri nets, logic programs, deadlock checking, reachability

DOI: 10.3233/FI-1999-37304

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 247-268, 1999

Authors: Junttila, Tommi A.

Article Type: Research Article

Abstract: The problem of finding symmetry information from algebraic system nets prior to the reachability graph generation is studied. The approach presented is based on well-formedness of transition descriptions, meaning that some data types in a net may be used in a symmetric way. Permutations on the domains of such data types produce symmetries on the state space level of the net, which in turn can be exploited during the reachability analysis. To ensure that the transitions behave symmetrically with respect to the chosen data domain permutations, a sufficient compatibility condition between data domain permutations and the algebraic terms used as …transition guards and arc annotations is proposed. The solution is a general and flexible one as it does not fix the set of applicable operations, enabling the design of customized net classes. To help the process of deciding whether a term is compatible with a data domain permutation, an approximation rule for the compatibility condition is given. Show more

Keywords: Symmetries, algebraic system nets, Petri nets, reachability analysis

DOI: 10.3233/FI-1999-37305

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 269-289, 1999

Authors: Kindler, Ekkart | Peuker, Sibylle

Article Type: Research Article

Abstract: A distributed algorithm is often used as a part of a larger distributed system. Usually, the properties of an algorithm are proven for the algorithm in isolation. Then, it is not obvious how the algorithm behaves when integrated into a larger system. In this paper, we present a simple technique which allows to derive properties of an algorithm which is integrated into a distributed system from the properties of the algorithm in isolation. The technique exploits the fact that some actions of a distributed algorithm do not belong to the algorithm but are triggered by the environment. If these actions …are distinguished and are adequately considered in the verification of the algorithm, basically all properties are still valid for the algorithm as a part of a larger distributed system. This result will be formalized in the setting of the Distributed Algorithms' Working Notation (DAWN). Based on this result, we will give a proof rule which allows to prove liveness properties of a system from liveness properties of the involved distributed algorithm. Show more

Keywords: Distributed Algorithms, Petri Nets, Compositionality, Temporal Logic

DOI: 10.3233/FI-1999-37306

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 291-309, 1999

Authors: Popova-Zeugmann, Louchka | Schlatter, Dirk

Article Type: Research Article

Abstract: In this paper, a parametric description of a transition sequence in a Time Petri net is introduced. The minimal and maximal time duration of a transition sequence are shown to be integers and furthermore the min/max path passes only integer-states. A necessary condition for the reachability of an arbitrary state is given.

Keywords: Time Petri Net, integer state, reachability of a state, parametric description of a transition sequence

DOI: 10.3233/FI-1999-37307

Citation: Fundamenta Informaticae, vol. 37, no. 3, pp. 311-327, 1999