Fundamenta Informaticae - Volume 79, issue 3-4

Article Type: Other

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. i-i, 2007

Authors: Mazurkiewicz, Antoni

Article Type: Research Article

Abstract: In the paper two notions related to local (distributed) computations are identified and discussed. The first one is the notion of reducible graphs. A graph is reducible if it can be reduced to a singleton by successive removing its removable nodes; the removing procedure should be local in the sense that to decide whether a node is removable or not it is sufficient to inspect its neighborhood. The second is the notion of compositional systems, consisting of …a set of objects together with a composition operation which to each pair of local objects (like local votes, partial trees, partial orderings, local consensus, local processes etc.) assigns their possible compositions; a sequence of such composition operations leads to a global object (like a global vote, a full spanning tree, a total ordering, a global consensus, a synchronized process, etc). Combining these two notions gives rise to a generic distributed algorithm for composing different local objects assigned to nodes of a reducible graph into one global object assigned to all nodes. Correctness of the composing algorithm, i.e. its proper termination and its impartiality is proved. Show more

Keywords: Local algorithms, distributed data, computation networks, distributed computing

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 265-282, 2007

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: The nets considered here are an extension of Petri nets in two aspects. In the semantic aspect, there is no one firing rule common to all transitions, but every transition is treated as an operator on data stored in its entry places and return results in its exit places. A state (marking) is a mapping of places (variables) into a given data structure, while interpretation is a mapping of transitions into a set of state transformers. Locality of …transition's activity is like in Petri nets. In the structural aspect, entry and exit places to a transition are ordered. A concatenation of such nets is defined, hence their calculus (a monoid). This allows for combining small nets into large ones, in particular designing a computation and control parts separately, then putting them together into one. Such extended nets may produce, in particular, other nets. A number of properties of the operation on nets and their decomposition are demonstrated. Show more

Keywords: Concurrency, Petri nets, interpretation, computation and control

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 283-293, 2007

Authors: Dietze, Roxana | Kudlek, Manfred | Kummer, Olaf

Article Type: Research Article

Abstract: It is shown that the boundedness problem for a certain class of basic object nets and a corresponding class of multiset rewriting systems is decidable. To achieve this result Dickson's Lemma for a certain class of multisets, and a modified Karp Miller algorithm, is applied. This presents another class of nets with different decidability behaviour for reachability and boundedness.

Keywords: Object Petri nets, multiset rewriting, Dickson's lemma, Karp Miller algorithm

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 295-302, 2007

Authors: Farwer, Berndt | Kudlek, Manfred | Rölke, Heiko

Article Type: Research Article

Abstract: We define Concurrent Turing Machines (CTMs) as Turing machines with Petri nets as finite control. This leads to machines with arbitrary many tape heads, thus subsuming any class of (constant) k-head Turing machines. Space, time, and head complexity classes are introduced and discussed showing the difference of various acceptance conditions that are defined for CTMs. Nevertheless, we show that CTMs can be simulated by TMs. Concurrent Turing machines correspond to a class of multiset …rewriting systems. The definition of a CTMs as a rewrite theory avoids the need for encoding multisets as words and using an equivalence relation on configurations. Multiset rewriting lends itself to be used in rewriting systems and tools like the rewriting engine Maude. For the rewriting system, a configuration is given by a varying sequence of strings and multisets. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 303-317, 2007

Authors: Gomolińska, Anna

Article Type: Research Article

Abstract: In this article, we aim at extension of similarity-based approximation spaces to the case, where both similarity and dissimilarity of objects are taken into account. Apart from the wellknown notions of lower rough approximation, upper rough approximation, and variable-precision positive regions of concepts, adapted to our case, the notions of exterior, possibly negative region, and ignorance region of concepts are introduced and investigated.

Keywords: approximation space, concept approximation, similarity relation, dissimilarity relation

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 319-333, 2007

Authors: Gruska, Damas P.

Article Type: Research Article

Abstract: A formal model for description of passive and active timing attacks is presented, studied and compared with other security concepts. It is based on a timed process algebra and on a concept of observations which make only a part of system behaviour visible. From this partial information which contains also timing of actions an intruder tries to deduce some private system activities.

Keywords: process algebras, timing attacks, information flow

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 335-346, 2007

Authors: van Hee, Kees | Oanea, Olivia | Serebrenik, Alexander | Sidorova, Natalia | Voorhoeve, Marc | Lomazova, Irina A.

Article Type: Research Article

Abstract: In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is …always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction. Show more

Keywords: verification, adaptive workflow, soundness, circumspectness

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 347-362, 2007

Authors: Jakubowska, Gizela | Penczek, Wojciech

Article Type: Research Article

Abstract: In this paper we offer a novel methodology for verifying correctness of (timed) security protocols. The idea consists in computing the time of a correct execution of a session and finding out whether the Intruder can change it to shorter or longer by an active attack. Moreover, we generalize the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. An implementation of our method is described. As case studies …we verify generalized (timed) authentication of KERBEROS, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol,Wide Mouthed Frog, and NSPK. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 363-378, 2007

Authors: Janowska, Agata | Penczek, Wojciech

Article Type: Research Article

Abstract: The paper presents a method of abstraction for timed systems. To extract an abstract model of a timed system we propose to use static analysis, namely a technique called path compression. The idea behind the path compression consists in identifying a path (or a set of paths) on which a process executes a sequence of transitions that do not influence a property being verified, and replacing this path with a single transition. The method is property …driven since it depends on a formula in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL^*_{-X} . Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 379-399, 2007