Fundamenta Informaticae - Volume 72, issue 1-3

Authors: Gomolińska, Anna

Article Type: Research Article

Abstract: We discuss the problem of rough ingredients and parts of concepts of an indiscernibility-based approximation space. The notion of a (rough) ingredient is extended to the notion of a possible (rough) ingredient, and analogously in the case of parts. The term "possible" means that a concept is perceived as a candidate for a future substitute of some ingredient. Our approach is in line with rough mereology except for allowing the empty concept for the sake of …simplicity. Show more

Keywords: approximation space, concept, closeness, rough mereology, ingredient/part

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 139-154, 2006

Authors: Grabowski, Franciszek | Strzalka, Dominik

Article Type: Research Article

Abstract: This paper deals with new analytical and experimental aspects of influence of data structure and algorithm on sort dynamics. Traditional analysis of data structure-algorithm interface which based on computational complexity is incomplete because do not considers of dynamical effects in area between extremely best and worst cases of computing time. The main aim of this paper are investigations of the impact of long-term dependencies in data structure on sort efficiency. This approach treats interface data …structure-algorithm as the complex system in opposition to the classical computational analysis which treats this interface as simple deterministic system. This new approach makes possibilities to determine power spectral density of sorting process and test the existence of 1/f noise in this process which in fact is not noise but reflects the intrinsic dynamic (data flow disturbances inside system) of selforganized computer system. The idea presented in this paper shows how complex system behavior provide a good perspective to analysis of whole computer system as well. Show more

Keywords: insertion sort, dynamics, 1/f noise

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 155-165, 2006

Authors: Gruska, Damas P.

Article Type: Research Article

Abstract: A formal model for an analysis of an information flow in interconnection networks is presented. It is based on timed process algebra which can express also network properties. The information flow is based on a concept of deducibility on composition. Robustness of systems against network timing attacks is defined. A variety of different security properties which reflect different security requirements are defined and investigated.

Keywords: security, information flow, timing attack, interconnection network

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 167-180, 2006

Authors: Janowska, Agata | Janowski, Paweł

Article Type: Research Article

Abstract: The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL_{-X} *.

Keywords: timed systems, Timed Automata, static analysis, program slicing

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 181-195, 2006

Authors: Kacprzak, Magdalena

Article Type: Research Article

Abstract: The paper introduces an original formalization of distributed systems which work in a concurrent way, especially multi-agent systems (MAS). The described deductive system, called RA-MAS, is based on elements of branching time temporal logic, epistemic logic and algorithmic logic. The established operators and modalities allow to compare different multi-agent systems on the basis of the same formal system. Moreover, the logic provides tools for modelling and characterizing mental features of agents as well as …different forms of cooperation. The main aim of the paper is to present axiomatization and prove a strong completeness result for the logic. The proof is inspired by a combination of the algebraic method of Rasiowa and Sikorski for classical logic with the Kripke method for modal logic. Show more

Keywords: multi-agent systems, deductive system, completeness

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 197-213, 2006

Authors: Kacprzak, Magdalena | Lomuscio, Alessio | Niewiadomski, Artur | Penczek, Wojciech | Raimondi, Franco | Szreter, Maciej

Article Type: Research Article

Abstract: We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.

Keywords: verification, Dining Cryptographers Protocol, bounded model checking, binary decision diagrams, SAT-solver

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 215-234, 2006

Authors: Klunder, Barbara

Article Type: Research Article

Abstract: Star-connected rational expressions were considered only as expressions defining trace languages. In this paper we continue the study of the class of flat languages defined by this kind of rational expressions. We strengthen results of [4] and prove that any star-connected language has an automaton with cycles which are composition of connected cycles. This condition is sufficient for star-connected languages provided that the dependency relation is transitive. As a consequence we obtain for every alphabet stronger …pumping lemma for star-connected languages. Finally, the product of two automata inherits this property from the components and thus for alphabet with transitive dependency relation the set of all star-connected languages is closed under intersections. Show more

Keywords: trace language, star-connected rational expressions, finite automata

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 235-243, 2006

Authors: Köhler, Michael | Rölke, Heiko

Article Type: Research Article

Abstract: Petri nets can be dualised by interchanging the role of places and transitions. This notion of duality is applicable only for unmarked Petri nets, since a marked place would be translated to a marked transition – which is meaningless – in the dual net. In this presentation we study the formalism of super-dual nets which are a generalisation of Petri nets. Super-dual nets allow for marked transitions also. The properties and the relation to other net formalism is …studied. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 245-254, 2006

Authors: Kudlek, Manfred

Article Type: Research Article

Abstract: It is shown that there don't exist quantum vector addition systems on various underlying structures for every number of productions. However, if the underlying vector space is restricted, such quantum vector addition systems exist.

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 255-261, 2006

Authors: Kurkowski, Mirosław | Srebrny, Marian

Article Type: Research Article

Abstract: In this paper we introduce a new, complete and decidable knowledge logic of authentication with a well defined semantics, intended for model checking verification of properties of authentication protocols. It is a version of the old BAN logic but with no belief modality, no modality at all, and with clearly expressible knowledge predicate. The new logic enjoys carefully defined and developed knowledge sets of the participants, with a potential intruder's knowledge and a well defined algorithm …of gaining, extracting and generating knowledge. The semantics is provided with a computation structure modelling a considered authentication protocol as a transition system. We provide a sound and complete axiomatization of the new logic and prove its decidability. From a pure mathematical logic standpoint, the new logic is a simple quantifier-free first order extension of the classical propositional calculus, while it is not a typical logic of knowledge, nor is it an extension of the BAN-logic. As the correctness property of an authentication protocol we require that the agents identify themselves by showing that they know the right keys. Show more

Keywords: verification, formal methods, authentication, security, knowledge

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 263-282, 2006