Fundamenta Informaticae - Volume 72, issue 1-3

Article Type: Other

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

Authors: Andreeva, Maria V. | Virbitskaite, Irina B.

Article Type: Research Article

Abstract: The intention of the paper is to develop a framework for weak observational equivalences in the setting of a real-time partial order model. In particular, we introduce a family of equivalences of linear time – branching time spectrum based on interleaving, causal tree and partial order semantics, in the setting of a dense time extension of stable event structures with internal actions. We study the relationships between the equivalences showing, on one hand, the discriminating power …of the approaches of the spectrum and, on the other hand, the coincidence of some semantics in a concrete approach. Furthermore, when dealing with particular subclasses of the model under consideration, there is no difference between more concrete and more abstract observations. Show more

Keywords: Real-Time Systems, Comparative Concurrency Semantics, Observational Equivalences, Timed Event Structures

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

Authors: Barbuti, Roberto | Maggiolo-Schettini, Andrea | Milazzo, Paolo | Troina, Angelo

Article Type: Research Article

Abstract: The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent elements and operators of sequencing, looping, containment and parallel composition. The looping operator allows tying up the ends of a sequence, thus creating a circular sequence which can represent a membrane. We show that a membrane calculus recently proposed can be encoded into CLS. We use our calculus to …model interactions among bacteria and bacteriophage viruses, and to reason on their properties. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 21-35, 2006

Authors: Bazan, Jan G.

Article Type: Research Article

Abstract: This paper introduces an approach to behavioral pattern identification as a part of a study of temporal patterns in complex dynamical systems. Rough set theory introduced by Zdzisław Pawlak during the early 1980s provides the foundation for the construction of classifiers relative to what are known as temporal pattern tables. It is quite remarkable that temporal patterns can be treated as features that make it possible to approximate complex concepts. This article introduces what are known …as behavior graphs. Temporal concepts approximated by approximate reasoning schemes become nodes in behavioral graphs. In addition, we discuss some rough set tools for perception modeling that are developed for a system for modeling networks of classifiers. Such networks make it possible to recognize behavioral patterns of objects changing over time. They are constructed using an ontology of concepts delivered by experts that engage in approximate reasoning about concepts embedded in such an ontology. We also present a method that we call a method for on-line elimination of non-relevant parts (ENP). This method was developed for on-line elimination of complex object parts that are irrelevant for identifying a given behavioral pattern. The article includes results of experiments that have been performed on data from a vehicular traffic simulator useful in the identification of behavioral patterns by drivers. Show more

Keywords: Behavior, complex patterns, identification, rough sets, concept approximation, dynamical system

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 37-50, 2006

Authors: Bednarczyk, Marek A. | Jamroga, Wojciech | Pawłowski, Wiesław

Article Type: Research Article

Abstract: Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest – the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problemof model checking properties of a class of the logic on Petri hypernets is shown to be PSPACE-complete.

Keywords: dynamic mobile agents, dynamic mobile agents, temporal logics, model checking

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 51-63, 2006

Authors: Chrz�stowski-Wachtel, Piotr

Article Type: Research Article

Abstract: When we model workflows with Petri nets, we call a workflow net sound, if it neither makes any transition dead nor it produces trash tokens in such a way that for every input token exactly one token appears eventually on the output place. We assume that the initial marking consists always of one token on the input place. However, sometimes it is necessary to take into account arbitrary markings, for instance when we make a recovery from an …unexpected situation during the workflow execution. An arbitrary marking is sound if it eventually produces exactly one output token without the possibility to leave any trash tokens. The paper addresses the problem of determining the proper control recovery, when unexpected situation arises, and we must detour from the normal execution. When we create an arbitrary control state during the recovery, it is easy to overlook some consequences and create either trash tokens or a deadlock in the future. The problem of determining if a given marking is sound is addressed in the paper in the context of structured nets. The presented linear solution is a necessary and sufficient condition for soundness of markings in structured nets. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 65-79, 2006

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: A specification of systems based on message passing paradigm is proposed. To this end, an algebraic structure called a semiring of formal polynomials with restricted idempotency of multiplication is taken and fix-point equations specifying (parallel) systems are constructed. Their solution provides an "implementation" of the system, in particular, a Petri net of various kind. Moreover, it determines a global information on capability of sending or receiving a message by objects from a local information on their …readiness to do this. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 81-93, 2006

Authors: Doroshenko, Anatoliy | Shevchenko, Ruslan

Article Type: Research Article

Abstract: In recent years light-weighted formal methods in construction and analysis of complex concurrent software system are of growing interest. In this paper a new rule-action based term rewriting framework, called TermWare, is proposed and its application to software system analysis is described to provide better cost effectiveness of software maintenance under varied requirements and specifications of operation. The main advantage is light-weighted formal model based on not computational semantics but on particular …properties of software system to be analyzed. Such approach eliminates the need in full formal analysis of software system and allows extreme flexibility of applications in two major concerns: high adaptability to changeable environment and easy reengineering and component reuse. The language and formal semantics of the system are defined. A new semantic model, called term system with action, is proposed for TermWare. A case study with some representative examples in source code analysis and software development with TermWare framework is presented. Show more

Keywords: term rewriting, rule-based programming, software system analysis

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 95-108, 2006

Authors: Farwer, Berndt | Köhler, Michael

Article Type: Research Article

Abstract: While it often makes sense to use pointer-based semantics (sometimes called reference semantics) to model components of a system that are in close proximity, this kind of modelling becomes increasingly infeasible for distant components. The notion of distance here is to be seen relative with respect to the system being modelled. We use local and global name spaces to model the necessary paradigm shift for systems of communicating mobile agents. As a concrete example of modelling that requires …discrimination of notions of proximity or distance, we study a scenario of mobile devices with wireless communications capabilities. The communication can be done directly between two agents or via a system of wireless network routers. To model such a system, we introduce object Petri nets that integrate both semantic paradigms found in the literature, i.e. reference semantics and value semantics. Formal definitions are given and some basic properties are proved. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 109-122, 2006

Authors: Farwer, Berndt | Varea, Mauricio

Article Type: Research Article

Abstract: This paper summarises two approaches, Dual Flow Nets (DFN) and Object Petri Nets (OPN), and offers a translation mechanism between them. While the DFN model tackles the separation of control and data flow computing aspects, the OPN model has a more generalised structure. The separation between control and data flow can enhance the readability of models, and allows different tools to operate on distinct parts of the model. The aim of this paper is to show …how the modelling based on control/data-flow analysis can benefit from an object-based Petri net approach. Tool support and a translation mechanism that is faithful are presented, giving an extra dimension (hierarchy) to the existing paradigm of control and data flow interacting in a model. Our methodology provides a comprehensive separation of these two parts, which can be used to feed analysis or synthesis tools, while still being able to reason about both parts through formal methods of verification. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 123-137, 2006

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

Authors: Nowak, Agnieszka | Wakulicz-Deja, Alicja | Bachliński, Sebastian

Article Type: Research Article

Abstract: Optimization of the speech recognition process is aiming at achieving short time of classification (speech to text system), while preserving the content of speech signal description, and all necessary details of speech signal in considered application. The goal of parametrization of the human's speech is to eliminate of those physical features of speech signal, that do not bring any useful information (e.g., frequency of laryngeal tone, timbre of voice). The purpose of the parametrization of a …speech signal is to minimize the volume of information that is to be analyzed. Our experiments suggest that using the cluster analysis method with agglomerative hierarchical technique is very helpful in finding relationships between speech phones. It lets us accelerate the process of speech recognition, simply because it is not necessary to analyze each phone separately and comparing it with an unclassified object. This principle has been carried to hidden Markov models. To organize those models we use the cluster analysis method with hierarchical techniques. Each model represents a single sequence of speech (probably the phone sequence). At the "top" of the structure we have models of phones in the most general context. When we go thru this structure to the bottom, there are models of phones in particular context. By the context we understand the juxtaposition the different phones. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 283-293, 2006

Authors: Nguyen, Trung Thanh | Willis, Claire P. | Paddon, Derek J. | Nguyen, Sinh Hoa | Nguyen, Hung Son

Article Type: Research Article

Abstract: Sunspots are the subject of interest to many astronomers and solar physicists. Sunspot observation, analysis and classification form an important part of furthering the knowledge about the Sun. Sunspot classification is a manual and very labor intensive process that could be automated if successfully learned by a machine. This paper presents machine learning approaches to the problem of sunspot classification. The classification scheme attempted was the seven-class Modified Zurich scheme [18]. The data was obtained by …processing NASA SOHO/MDI satellite images to extract individual sunspots and their attributes. A series of experiments were performed on the training dataset with an aim of learning sunspot classification and improving prediction accuracy. The experiments involved using decision trees, rough sets, hierarchical clustering and layered learning methods. Sunspots were characterized by their visual properties like size, shape, positions, and were manually classified by comparing extracted sunspots with corresponding active region maps (ARMaps) from the Mees Observatory at the Institute for Astronomy, University of Hawaii. Show more

Keywords: sunspot classification, layered learning, rough sets, machine learning

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 295-309, 2006

Authors: Ochmański, Edward | Pieckowska, Joanna

Article Type: Research Article

Abstract: Trace nets are a generalization of elementary nets, proposed by Badouel and Darondeau. They admit phenomena, unknown in traditional nets. For instance, in trace nets does not hold the "diamond property". For this reason, we propose a more precise definition of conflict, applicable to trace nets, and study occurrences of conflicts and existence of conflict-free runs in such nets. Main result of the paper says that any just computation in a trace net, starting from a …conflict state, contains a conflict step. This result allows to construct an algorithm, selecting only conflict-free just computations from among all computations of a given net. All results of the paper hold for elementary nets, as they are a subclass of trace nets. Show more

Keywords: Petri nets, trace nets, conflicts

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 311-321, 2006

Authors: Ochmański, Edward | Stawikowska, Krystyna

Article Type: Research Article

Abstract: The paper deals with star-free languages in free monoids and trace monoids. We introduce the notion of star-free star, fundamental for this paper, and show that the classes of star-free languages and star-free star languages coincide. Then, using this result, we obtain a general characterization of star-free trace languages, containing a result of Guaiana/Restivo/Salemi (star-free=aperiodic in trace monoids), originally proved in a more involved, combinatorial way.

Keywords: star-free languages, traces languages

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 323-331, 2006

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: The notion of an associative omega-product is applied to processes. Processes are one of the ways to represent behavior of Petri nets. They have been studied for some years as an alternative to traces and dependence graphs. One advantage of processes, as compared to traces, is a very simple way to define infinite concatenation. We take a closer look at this operation, and show that it is a free associative omega-product of finite processes. Its associativity …simplifies some arguments about infinite concatenation, as illustrated by the proof of interleaving theorem. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 333-345, 2006

Authors: Shilov, N.V. | Garanina, N.O. | Choe, K.-M.

Article Type: Research Article

Abstract: We present (update+abstraction) algorithm for model checking a fusion of Computation Tree Logic and Propositional Logic of Knowledge in systems with the perfect recall synchronous semantics. It has been already known that the problem is decidable with a non-elementary lower bound. The decidability follows from interpretation of the problem in a so-called Chain Logic and then in the Second Order Logic of Monadic Successors. This time we give a direct algorithm for model checking and detailed …time upper bound where a number of different parameters are taken into count (i.e. a number of agents, a number of states, knowledge depth, formula size). We present a toy experiment with this algorithm that encourages our hope that the algorithm can be used in practice. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 347-361, 2006

Authors: Skowron, Andrzej | Stepaniuk, Jarosław | Peters, James | Swiniarski, Roman

Article Type: Research Article

Abstract: This paper considers the problem of how to establish calculi of approximation spaces. Approximation spaces considered in the context of rough sets were introduced by Zdzisław Pawlak more than two decades ago. In general, a calculus of approximation spaces is a system for combining, describing, measuring, reasoning about, and performing operations on approximation spaces. An approach to achieving a calculus of approximation spaces that provides a basis for approximating reasoning in distributed systems …of cooperating agents is considered in this paper. Examples of basic concepts are given throughout this paper to illustrate how approximation spaces can be beneficially used in many settings, in particular for complex concept approximation. The contribution of this paper is the presentation of a framework for calculi of approximation spaces useful for approximate reasoning by cooperating agents. Show more

Keywords: rough sets, approximation spaces, concept approximation, learning, approximate reasoning

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 363-378, 2006

Authors: Stefanowski, Jerzy | Wilk, Szymon

Article Type: Research Article

Abstract: The paper addresses problems of improving performance of rule-based classifiers constructed from imbalanced data sets, i.e., data sets where the minority class of primary importance is under-represented in comparison to majority classes. We introduced two techniques to detect and process inconsistent examples from the majority classes in the boundary between the minority and majority classes. Both these techniques differ in the way of processing inconsistent boundary examples from the majority classes. The first …approach removes them, while the other relabels them as belonging to the minority class. The experiments showed that the best results were obtained for the filtering technique, where inconsistent majority class examples were reassigned to the minority class, combined with a classifier composed of decision rules generated by the MODLEM algorithm. Show more

Keywords: Knowledge Discovery, Data Mining, Rough Sets, Classification, Class Imbalance, Rule Induction

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 379-391, 2006

Authors: Suraj, Zbigniew | Gayar, Neamat El | Delimata, Pawel

Article Type: Research Article

Abstract: During the past decade methods of multiple classifier systems have been developed as a practical and effective solution for a variety of challenging applications. A wide number of techniques and methodologies for combining classifiers have been proposed in the past years in literature. In our work we present a new approach to multiple classifier systems using rough sets to construct classifier ensembles. Rough set methods provide us with various useful techniques of data classification. …In the paper, we also present a method of reduction of the data set with the use of multiple classifiers. Reduction of the data set is performed on attributes and allows to decrease the number of conditional attributes in the decision table. Our method helps to decrease the number of conditional attributes of the data with a small loss on classification accuracy. Show more

Keywords: multiple classifier systems, k-NN, reduction, feature selection

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 393-406, 2006

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: The paper is concerned with algebras which can be obtained by endowing sets of processes of Petri nets with a sequential and a parallel composition. The considered algebras are categories with additional structures and special properties. It is shown that all structures which enjoy such properties can be represented as algebras of processes of Petri nets.

Keywords: Petri nets, states, processes, sequential composition, parallel composition, category, partial monoid

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 407-420, 2006

Authors: Wolski, Marcin

Article Type: Research Article

Abstract: The present article deals with the problem whether and how the bilattice orderings of knowledge ⩽_k and truth ⩽_t might enrich the theory of rough sets. Passing to the chief idea of the paper, we develop a bilattice-theoretic generalisation of the concept of rough set to be called A-approximation. It is proved that A-approximations (induced by a topological approximation space) together with the knowledge ordering ⩽_k constitute a complete partial …order (CPO) and that the meet and join operations induced by the truth ordering ⩽_t are continuous functions with respect to ⩽_k . Crisp sets are then obtained as maximal elements of this CPO. The second part of this article deals with the categorical and algebraic properties of A-approximations induced by an Alexandroff topological space. We build a *-autonomous category of A-approximations by means of the Chu construction applied to the Heyting algebra of open sets of Alexandroff topological space. From the algebraic point of view A-approximations under ⩽_t ordering constitute a special Nelson lattice and, as a result, provide a semantics for constructive logic with strong negation. Such lattice may be obtained by means of the twist construction over a Heyting algebra which resembles very much the Chu construction. Thus A-approximations may be retrived from very elementary structures in elegant and intuitive ways. Show more

Keywords: rough set, approximation, bilattice, complete partial order, *-autonomous category, Chu construction, Nelson lattice

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 421-435, 2006