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

Authors: Köhler, Michael

Article Type: Research Article

Abstract: In this article I will prove undecidability results for elementary object net systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach which is called the "netswithin-nets" paradigm. EOS are special object net systems which have a two leveled structure.

Keywords: decidability, nets within nets, Petri nets, reachability

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

Authors: Köhler, Michael

Article Type: Research Article

Abstract: Agent oriented software engineering is seen as the approach taking object oriented approaches one step ahead. The design of agent systems is based on three fundamental perspectives: the functional, the team-interactional and the organisational perspective. The organisational perspective becomes a central design issue if the number of agents is large or the environment is unstable. While the functional perspective is well founded in the planning theory of artificial intelligence and the interactional perspective is …rooted in the theory of speech-acts and formal ontologies, the organisational perspective is still an active research area with several open questions. In this paper we define a formal organisation model for agent systems based on Petri nets and show how agent oriented software engineering can benefit from this model. Show more

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

Authors: Kryvyy, Sergiy | Matvyeyeva, Lyudmila

Article Type: Research Article

Abstract: We present in this paper the algorithm which performs the translation of MSC'2000 diagrams into Petri net modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement theMSC'2000 standard with the formal definition of the MSC 〈condition〉 element by means of process algebra. This translation algorithm is the part of the automated verification system which formally specifies and verifies a designed software or hardware system specified in the MSC language and is presented …in [1] and [2]. Show more

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

Authors: Kudlek, Manfred

Article Type: Research Article

Abstract: The concept of semilinear sets is generalized to commutative semirings. It is shown that the semilinear sets over commutative semirings are exactly the algebraic/rational sets over such structures.

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

Authors: Kurkowski, Mirosław | Penczek, Wojciech

Article Type: Research Article

Abstract: In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol proving either reachability or unreachability of an undesired state. We exemplify all our notions …on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS. Show more

Keywords: security protocols, model checking, authentication

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

Authors: Lomuscio, Alessio | Raimondi, Franco | Woźna, Bożena

Article Type: Research Article

Abstract: We use MCMAS-X to verify authentication properties in the TESLA secure stream protocol. MCMAS-Xis an extension to explicit and deductive knowledge of the OBDD-based model checker MCMAS a verification tool for multi-agent systems.

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

Authors: Mazurkiewicz, Antoni

Article Type: Research Article

Abstract: In the paper triangular graphs are discussed. The class of triangular graphs is of special interest as unifying basic features of complete graphs and trees. The main issue addressed in the paper is to characterize class of triangular graphs (defined globally) by local means. Namely, it is proved that any triangular graph can be constructed from a singleton by successive extensions with nodes having complete neighborhoods. Next, the proved theoretical properties are applied for designing some …local algorithms for triangular graphs: for elections a leader and for constructing their spanning trees. The fairness of these algorithms is proved, which means that any node can be elected and any spanning tree can be constructed by execution of these algorithms. Show more

Keywords: triangular graphs, local computations, leader elections, spanning trees

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

Authors: Peters, James F. | Skowron, Andrzej | Stepaniuk, Jaroslaw

Article Type: Research Article

Abstract: The problem considered in this paper is the extension of an approximation space to include a nearness relation. Approximation spaces were introduced by Zdzis?aw Pawlak during the early 1980s as frameworks for classifying objects by means of attributes. Pawlak introduced approximations as a means of approximating one set of objects with another set of objects using an indiscernibility relation that is based on a comparison between the feature values of objects. Until now, the focus has …been on the overlap between sets. It is possible to introduce a nearness relation that can be used to determine the "nearness" of sets of objects that are possibly disjoint and, yet, qualitatively near to each other. Several members of a family of nearness relations are introduced in this article. The contribution of this article is the introduction of a nearness relation that makes it possible to extend Pawlak's model for an approximation space and to consider the extension of generalized approximations spaces. Show more

Keywords: rough sets, approximation, approximation space, classification, feature, nearness relation, neighbourhood, proximity space

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

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: Two recent developments in the field of formal languages are Parsing Expression Grammar (PEG) and packrat parsing. The PEG formalism is similar to BNF, but defines syntax in terms of recognizing strings, rather than constructing them. It is, in fact, precise specification of a backtracking recursive-descent parser. Packrat parsing is a general method to handle backtracking in recursive-descent parsers. It ensures linear working time, at a huge memory cost. This paper reports an experiment that consisted …of defining the syntax of Java 1.5 in PEG formalism, and literally transcribing the PEG definitions into parsing procedures (accidentally, also in Java). The resulting primitive parser shows an acceptable behavior, indicating that packrat parsing might be an overkill for practical languages. The exercise with defining the Java syntax suggests thatmore work is needed on PEG as a language specification tool. Show more

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

Authors: Stepaniuk, Jaroslaw

Article Type: Research Article

Abstract: In this paper, we show that approximation spaces are basic structures for knowledge discovery from multi-relational data. The utility of approximation spaces as fundamental objects constructed for concept approximation is emphasized. Examples of basic concepts are given throughout this paper to illustrate how approximation spaces can be beneficially used in many settings.

Keywords: rough sets, approximation spaces, multi-relational data mining

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

Authors: Suraj,, Zbigniew | Fryc, Barbara

Article Type: Research Article

Abstract: Approximate Petri nets (AP-nets) can be used for the knowledge representation and approximate reasoning. The AP-net model is defined on the basis of the rough set approach, fuzzy Petri nets and coloured Petri nets. One of the main advantages of AP-net model is a possibility to present the reachability set of a given AP-net by means of an occurrence graph. Such graphs can serve, among others, for analyzing and evaluating an approximate reasoning realized by using …AP-net model. The main contribution of the paper is to present the algorithms for construction and analysis of occurrence graphs for the AP-nets, especially in the context of searching for the best decision and finding the shortest distance in order to compute such decision. This approach can be applied to the design and analysis of the formal models for expert systems, control systems, communication systems, etc. Show more

Keywords: approximate Petri nets, approximate reasoning, knowledge representation, occurrence graphs

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

Authors: Suraj, Zbigniew | Pancerz, Krzysztof

Article Type: Research Article

Abstract: This paper provides new algorithms for computing consistent and partially consistent extensions of information systems. A maximal consistent extension of a given information system includes only objects corresponding to known attribute values which are consistent with all rules extracted from the original information system. A partially consistent extension of a given information system includes objects corresponding to known attribute values which are consistent to a certain degree with the knowledge represented by …rules extracted from the original information system. This degree can be between 0 and 1, 0 for the full inconsistency and 1 for the full consistency. The algorithms presented here do not involve computing any rules true in a given information system. This property differentiates them from methods presented in the earlier papers which concerned extensions of information systems. Show more

Keywords: rough sets, information systems, consistent extensions, partially consistent extensions

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

Authors: Wolski, Marcin

Article Type: Research Article

Abstract: The present paper investigates approximation spaces in the context of mathematical structures which axiomatise the notion of nearness. Starting with the framework of information quanta which distinguishes two levels of information structures, namely property systems (the first level) and information quantum relational systems (the second level), we shall introduce the notion of Pawlak property system. These systems correspond bijectively to finite approximation spaces, i.e. their respective information quantum relational systems. Then we …characterise Pawlak property systems in terms of symmetric topological spaces. In the second part of the paper, these systems are defined by means of topological structures based on the concept of nearness. We prove that the category of Pawlak property systems is isomorphic to the category of finite topological nearness spaces and provide its additional topological characterisation. Show more

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

Authors: Zbrzezny, Andrzej | Półrola, Agata

Article Type: Research Article

Abstract: Reachability analysis for timed automata using SAT-based methods was considered in many papers, occurring to be a very efficient model checking technique. In this paper we show how to apply this method of verification to timed automata with discrete data, i.e., to standard timed automata augmented with integer variables. The theoretical description is supported by some preliminary experimental results.

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