Fundamenta Informaticae - Volume 85, issue 1-4

Authors: Strzałka, Dominik | Grabowski, Franciszek

Article Type: Research Article

Abstract: This paper presents a preliminary analysis of the system behavior that works far from the thermodynamical equilibrium states in the environment with limited resources. The examples of such systems are the real computer systems. Nowadays in such systems the runoff characteristic of the information flow is very turbulent in contradiction to the current existing laminar models. These systems work under constant overload, which means a permanent thermodynamical non-equilibrium (from the thermodynamical point of view). For …such a situation the classical approach to their modeling is still based on Boltzmann-Gibbs (BG) thermodynamics,which is proper only for systems that are in equilibriumstate (sometimes called thermostatic) or very close to it. The changing number of tasks N in such systems and the limited resourcesK of the environment cause its chaotic behavior and generate the dependencies that have got a long-termproperty. Such processes degrade the system performance X and elongate the response time R; in other words degrade the Quality of Service (QoS). To understand the whole behavior of such systems one needs a proper thermodynamical basis that seems to be the Tsallis formula of the non-extensive entropy. Show more

Keywords: limited resources, non-extensive entropy, thermodynamic non-equilibrium

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 455-464, 2008

Authors: Varpaaniemi, Kimmo | Ojala, Leo

Article Type: Research Article

Abstract: Reachability analysis is one of the most successful methods used in design and validation of protocols for classical communication, whereas the predicate/transition-net formalism is one of the most appropriate formalisms for reachability analysis oriented modelling. Quantum teleportation and dense coding are non-classical communication protocols that have been widely researched in the field of quantum computing. In this article, we present predicate/transitionnet models of these two protocols and use the PROD reachability analysis tool for …analysing the models. Show more

Keywords: reachability analysis, predicate/transition-nets, quantum teleportation, dense coding

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 465-479, 2008

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: The paper is devoted to characterizing systems with random behaviours. The characterization is based on considering systems in terms of their possible runs, called processes, where each process is represented by a pomset in an intrinsic, global time independent way and can possibly be obtained by composing sequentially and in parallel other processes.

Keywords: Universe of objects, processes, states, sequential composition, parallel composition, partial category, partial monoid, random behaviour

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 481-496, 2008

Authors: Wolski, Marcin

Article Type: Research Article

Abstract: In this paper we study metric properties of finite approximation spaces and approximation operators from Rough Set Theory. In the first part of the article we examine finite approximation spaces and finite approximation topological spaces regarded as particular instances of two basic types of information structures from the framework of Information Quanta: information quantum relational systems and property systems, respectively. In the second part of the paper is the Marczewski-Steinhaus metric discussed as a certain …distance of sets defined with respect to the approximation operators. We propose two types of á la Marczewski-Steinhaus distance functions: the first type is based on the lower approximation operator; the second one is based on the upper approximation operator. These types can be defined with respect to both finite approximation spaces (information quantum relational systems) and finite approximation topological spaces (property systems), giving us four distancemeasure functions. In order to define a distance of sets which preserves their lower and upper approximations, one can take the sum of two respective functions. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 497-512, 2008

Authors: Zbrzezny, Andrzej

Article Type: Research Article

Abstract: The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.

Keywords: ECTL, Bounded Model Checking, translation to SAT

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 513-531, 2008

Authors: Zbrzezny, Andrzej | Woźna, Bożena

Article Type: Research Article

Abstract: VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known …alternating bit protocol written in Java. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 533-548, 2008

Authors: Zielosko, Beata | Piliszczuk, Marcin

Article Type: Research Article

Abstract: In the paper the accuracy of greedy algorithmfor construction of partial tests (superreducts) and partial decision rules is considered. Results of experiments with greedy algorithm are described.

Keywords: Partial tests, partial reducts, partial decision rules, greedy algorithm

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 549-561, 2008