Fundamenta Informaticae - Volume 60, issue 1-4

Authors: Burkhard, Hans-Dieter | Lindemann, Gabriela | Czaja, Ludwik | Suraj, Zbigniew

Article Type: Other

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. vii-viii, 2004

Authors: Mazurkiewicz, Antoni

Article Type: Research Article

Abstract: In general, a negotiation within a group of participants is a process, which starting with participants in some arbitrary (initial) states eventually come to an agreement with all participants being in the negotiated state. The formal method used for discussing the considered issue are local computations; in general, they consist in transforming states of whole structures by way of transforming states of some of their substructures. Negotiation procedures are local computations that act according to negotiation …protocols. The paper aims to discuss communication structures that admit negotiations limited to direct communications between at most two negotiating partners (bilateral negotiations). As a formal model of the communication structures graphs are used, with nodes representing participants of negotiations, edges the direct links between them, and a total (linear) ordering of nodes as the goal of negotiations; in our setup substructures subjected to transformations consist of two adjecent nodes only. There are known protocols that can solve particular problems; the question arises whether the same problems can be solved by local computations using substructures of size at most two. The present paper aims to offer an answer to this question. Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 1-16, 2004

Authors: Mosses, Peter D.

Article Type: Research Article

Abstract: Structural Operational Semantics (SOS) allows transitions to be labelled. This is fully exploited in SOS descriptions of concurrent systems, but usually not at all in conventional descriptions of sequential programming languages. This paper shows how the use of labels can provide significantly simpler and more modular descriptions of programming languages. However, the full power of labels is obtained only when the set of labels is made into a category, as in the recently-proposed MSOS variant of …SOS. Show more

Keywords: Structural operational semantics, SOS, modularity, MSOS, natural semantics

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 17-31, 2004

Authors: Pawlak, Zdzisław

Article Type: Research Article

Abstract: We proposed in this paper to use some ideas of Jan Łukasiewicz, concerning independence of logical formulas, to study dependencies in databases.

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 33-39, 2004

Authors: Ambroszkiewicz, Stanisław

Article Type: Research Article

Abstract: There are two general approaches to integration of heterogeneous applications. The first one corresponds to business-to-business point of view, whereas the second one to the client's point of view. The first one is based on the assumption that applications are composed, orchestrated, or choreographed in order to create sophisticated business processes, whereas the second one assumes that applications are composed (typically on the fly) in order to realize clients' requests. In this work the client's point …of view is taken and a new experimental technology for service description and composition in open and distributed environment is proposed. The technology consists of description language called Entish, and composition protocol called entish 1.0. Show more

Keywords: service-oriented architecture, service description and composition, software agents

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 41-66, 2004

Authors: Barbuti, Roberto | Cataudella, Stefano | Tesei, Luca

Article Type: Research Article

Abstract: In this paper we investigate the use of abstract interpretation techniques for statically preventing race conditions. To this purpose we enrich the concurrent object calculus concζ by annotating terms with the set of "locks" owned at any time. We use an abstract form of the object calculus to check the absence of race conditions. We show that abstract interpretation is more flexible than type analyses, and it allows to certify as "race free" a larger class …of programs. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 67-79, 2004

Authors: Bernardeschi, Cinzia | De Francesco, Nicoletta | Lettieri, Giuseppe

Article Type: Research Article

Abstract: This paper presents a technique for verifying secure information flow in concurrent programs consisting of a number of independently executing sequential processes with private memory. Communications between processes are synchronous. Moreover, processes are open systems that can accept inputs from the environment and produce outputs towards the environment. The technique is based on an abstract interpretation. First we define a concrete instrumented …semantics where each value is annotated with the security level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 81-98, 2004

Authors: Doroshenko, Analoliy | Tseitlin, Georgy

Article Type: Research Article

Abstract: An approach based on algebraic treatment of programs and advanced transition system operational semantics is described for asynchronous communication of parallel distributed/shared memory programs. The approach aimes at efficient synchronization and combines compile- and run-time data flow analysis to improves computation and communication overlapping. A number of semantic models of data exchanges of increasing power for asynchronous communication in distributed environment are constructed. Two programming abstractions, exchange environs and coordination expressions, aimed …to reduce communication and synchronization overhead are derived from the theory. The program models constructed give more theoretical insight into the nature of parallelism of computation and communication and have immediate practical influence on parallel programming. Particularly automatic resolution of some classes of communication deadlocks are allowed and enhancement of data parallel par Show more

Keywords: concurrency of computation and communication, program abstractions, coordination expressions

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 99-111, 2004

Authors: Farwer, Berndt | Köhler, Michael

Article Type: Research Article

Abstract: The Petri-net-based formalism of mobile object-net systems (Mons) is used to model concurrent systems with dynamically changing environments, such as mobile objects. The tokens in Mons are themselves Petri nets, which gives the formalism an additional (vertical) dimension of nesting. Traditional Petri nets have essentially a horizontal structure, given by the fact that markings are multisets. The question arises, whether Mons can be regarded as a canonical extension of such Petri nets. Due to the nested …nature of Mons, the answer is not obvious. We first give the formal definition of Mons and then prove some properties of the formalism, showing that, with respect to interleaving semantics (i.e. firing sequences), Mons can indeed be viewed as a canonical extension of traditional Petri nets. We then define Mons processes, also as a canonical extension of standard Petri net processes. Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 113-129, 2004

Authors: Farwer, Berndt | Kudlek, Manfred

Article Type: Research Article

Abstract: The present paper continues work from [7]. One goal of this work is to find a class of (object) Petri nets of lesser power than Turing machines, such that there exists a universal Petri net within that class. Another goal is to surpass the restricted synchronisation of transitions in object and system nets in the case of value semantics. Finally, an encoding of the proposed class of object Petri nets into linear logic Petri nets (LLPNs) is given, which …directly leads to a specification that can be model-checked by existing tools. Show more

Keywords: universal Petri net, universal machine, object Petri net, higher-order Petri net, synchronisation, value semantics

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 131-142, 2004

Authors: Fryc, B. | Pancerz, K. | Peters, J.F. | Suraj, Z.

Article Type: Research Article

Abstract: In 1990 Shyi-Ming Chen et al. presented a new approach to knowledge representation using fuzzy Petri nets (FPN). A fuzzy Petri net model allows a structural representation of knowledge and has a systematic procedure for supporting fuzzy reasoning. In this paper we propose an algebraic (matrix) representation of FPNs. We use this representation in a fuzzy reasoning algorithm which is simple to implement in modern programming languages such as C++, C# or Java. Furthermore, there exists …MATLAB - a computer system which makes it possible to solve many computing problems, especially those with matrix and vector formulations. We present also an approach enabling us to carry out a fuzzy reasoning process using the MATLAB environment. Show more

Keywords: algebraic representation, fuzzy Petri nets, fuzzy reasoning, knowledge representation

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 143-157, 2004

Authors: Gomolińska, Anna

Article Type: Research Article

Abstract: The aim of the paper is to introduce degrees of satisfiability as well as a graded form of the meaning of formulas and their sets in the approximation space framework.

Keywords: granulation of information, Pawlak information systems, approximation space, graded meaning of formulas

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 159-172, 2004

Authors: Heckel, Martin | Zendulka, Jaroslav

Article Type: Research Article

Abstract: This paper deals with an idea of the use of data mining approach in texture analysis. A new method based on association rules is proposed. This method utilizes the multiresolution analysis of an analyzed image texture and works at the texture primitive level. Within this method, a technique for feature vector construction without any a priori knowledge of textures different from the analyzed one is presented. The contribution also contains some results of texture image segmentation …experiments. Show more

Keywords: data mining, association rules, texture analysis, texture primitive

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 173-186, 2004

Authors: Janowska, Agata | Janowski, Paweł

Article Type: Research Article

Abstract: This paper presents a method of slicing timed systems to create reduced models for model checking verification. The reduction is made at the very beginning of the verification process and this makes it beneficial and effective in handling the state explosion problem. The method uses techniques of static analysis to …examine the syntax of a program and to remove irrelevant fragments of the code. The timed extension of the classical slicing definition is given and applied to Intermediate Language of the verification system Verics and Estelle specification language. Show more

Keywords: static analysis, program slicing, system verification, timed systems, timed automata

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 187-210, 2004

Authors: Konikowka, Beata | Penczek, Wojciech

Article Type: Research Article

Abstract: A multi-valued version of CTL^* (mv-CTL^*), where both the propositions and the accessibility relation are multi-valued, taking values in a complete lattice with a complement, is considered. Contrary to all the existing model checking results for multi-valued modal logics, our lattices are not required to be finite. A set of restrictions is provided under which there is a direct translation from mv-CTL^* to CTL^* model checking problem for designated values. Bisimulation induced by mv-CTL^* is …characterized. Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 211-224, 2004

Authors: Lomazowa, Irina A.

Article Type: Research Article

Abstract: A community of interacting automata is a set of nondeterministic finite automata which can execute actions autonomously, synchronize with each other, or generate new members of the community. Thus interacting automata allow to model distributed systems with nonlimited number of distributed agents. We show that the formalism of interacting automata has a clear …semantics and nice semantic properties. Show more

Keywords: distributed systems, finite automata, interaction, semantical properties, systems with dynamic structure

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 225-235, 2004

Authors: Ochmański, Edward

Article Type: Research Article

Abstract: The fairness hierarchy and conspiracies, the notions introduced by Best, are studied in the context of elementary nets. Proving that sequential as well as persistent systems are conspiracy-free, we indicate two main roots of conspiracies: distributed memory and conflicts. Using the notion of marking-fairness, due to Merceron, …we prove that T0-fairness + M0-fairness = T∞-fairness. This result gives a method of a local control ensuring globally fair executions. Next we show how to check, if a given elementary net is conspiracy-free, and prove the obtained criterion to be effectively decidable. Finally, we give a characterization of live concurrent systems, using the notion of ∞-fairness. Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 237-250, 2004

Authors: Pancerz, Krzysztof | Suraj, Zbigniew

Article Type: Research Article

Abstract: This paper presents an approach to discovering concurrent models from data tables using the ROSECON software system. The acronym ROSECON comes from "ROugh SEts and CONcurrency". The models created using ROSECON have the form of Coloured Petri Nets. The ROSECON system is based on the rough set theory. The models derived by ROSECON can be used to determine different properties concerning structures and behaviours of systems. Running examples illustrate some directions one might take in the …study of behavioural patterns in information system tables. Show more

Keywords: rough set tools, Coloured Petri Nets, software systems

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 251-268, 2004

Authors: Polak, Michał | Majdzik, Paweł | Banaszak, Zbigniew | Wójcik, Robert

Article Type: Research Article

Abstract: This paper is addressing an issue of distributed systems designing aimed at automated prototyping of Cyclic Concurrent Processes Systems. In such systems concurrent processes compete for access to shared system resources. In order to ensure that a system is deadlock and starvation-free, certain conditions must be satisfied. In this paper, these conditions guarantee that for a given pair (an initial state, a set of dispatching rules) the system - belonging to a specific class - has …a steady cyclic state. However, system designers are interested in values of performance indices, such as a rate of resources or processes utilization or the period of the system cycle. Nowadays, the values of performance indices are provided mainly as a result of a simulation process, which requires much more processor power than in case of an analytical method. Thus, in this paper the authors focus on providing a procedure that enables building analytical models of Cyclic Concurrent Processes Systems belonging to a system class considered in the paper. To reach this aim the max-plus algebra formalism is employed. Both the conditions ensuring a cyclic process flow and steps of the procedure are the basis of a software tool, which can be used by designers to prototype systems of desired values of the performance indices. Thanks to the computer program the designers receive a useful tool that helps to validate and allocate distributed control procedures, even in a complex system, which is a composition of simpler systems. The procedure together with the software tool is the main outcome of this paper. Show more

Keywords: cyclic process, modelling, (max,+) algebra, performance evaluation

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 269-289, 2004

Authors: Polkowski, Lech | Semeniuk-Polkowska, Maria

Article Type: Research Article

Abstract: Communicating Sequential Processes (CSP), is a theoretical framework for discussing concurrent phenomena [7]. In this note, we begin an investigation into the nature of sets of communicating sequential processes. Sets of sequential processes arise naturally when one considers processes contained within specified bounds which provides their approximate description. Adopting the trace formalism, we may express those bounds in a natural way by means of containment of traces. We endow families of process traces and a …fortiori, families of processes, with a rough set topology. We show in this note that basic operators on processes preserve exact sets of processes and they are non-expansive (i.e., non-destructive in terminology of [7]) with respect to the metric D on rough sets [6], [5], restricted to exact sets of processes. Show more

Keywords: communicating sequential processes, rough set theory, exact sets of processes, constructive and non-destructive mappings on exact sets of processes

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 291-305, 2004

Authors: Półrola, Agata | Penczek, Wojciech

Article Type: Research Article

Abstract: The paper presents three methods for applying partitioning algorithms, used for generating abstract models for timed automata, to the case of time Petri nets. Each of these methods is based on a different approach to the concrete semantics of a net, and can potentially be more efficient than the others in a particular case. Besides the theoretical description, we provide some …preliminary experimental results, obtained from the implementation integrated with the model checking tool VerICs Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 307-331, 2004

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: In recent years, a number of classical results connecting rational languages with finite semigroups have been extended to infinite-word languages using the notion of an ω-semigroup: a semigroup augmented with an associative infinite product. This paper takes a closer look at the associative infinite product itself. It suggests some improvements and presents a couple of new facts.

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 333-350, 2004

Authors: Skowron, Andrzej | Synak, Piotr

Article Type: Research Article

Abstract: We outline some results of our current research on developing a methodology for solving problems of spatio-temporal reasoning. We consider classifiers for complex concepts in spatio-temporal reasoning that are constructed hierarchically. We emphasise the fact that the construction of such hierarchical classifiers should be supported by domain knowledge. Approximate reasoning networks (AR networks) are proposed for approximation of reasoning schemes expressed in natural language. Such reasoning schemes are extracted from knowledge bases …representing domain knowledge. This approach makes it possible to induce classifiers for complex concepts by constructing them along schemes of reasoning extracted from domain knowledge. Show more

Keywords: complex object, concept approximation, pattern, rough sets, spatio-temporal reasoning, classifier, network of classifiers

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 351-366, 2004

Authors: Tini, Simone | Maggiolo-Schettini, Andrea

Article Type: Research Article

Abstract: We give an algorithm for synthesizing Generalized Mealy Machines from LTL-formulae. The main novelty of the paper is that the algorithm is compositional. Its complexity coincides with the lower bound of the synthesis problem.

Keywords: mealy machines, LTL, synthesis

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 367-382, 2004

Authors: Virbitskaite, Irina B. | Gribovskaya, Natalya S.

Article Type: Research Article

Abstract: The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of timed extensions of partial order models, in order to transfer general concepts of equivalences to the models. In particular, we define categories of timed event structures, whose morphisms are to be thought of as simulations, and accompanying (sub)categories of observations, to which the corresponding notions of open maps are developed. We then use the …open maps framework to obtain abstract bisimilarities which are established to coincide with timed extensions of well-known partial order based equivalences. Show more

Keywords: category theory, open maps, timed event structures, timed partial order equivalences

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 383-399, 2004

Authors: Wolski, Marcin

Article Type: Research Article

Abstract: We investigate Galois connections and their relations to the major theories of (qualitative) data analysis: Rough Set Theory (RST), Formal Concept Analysis (FCA) and John Stuart Mill Reasoning (JSM-Reasoning). Polarities, a type of contravariant Galois connections, and their relationships with data analysis has been already well-known. This paper shows how axialities, a type of covariant Galois connections, are …related to problems adressed by data analysis and prove that they give rise to a number of interesting lattices. Show more

Keywords: galois connection, polarity lattice, axiality, concept, rough set, lattice

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 401-415, 2004

Authors: Zbrzezny, Andrzej

Article Type: Research Article

Abstract: The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a~state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the property is translated to a propositional formula and satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a …state satisfying the property has been found or all the states of the timed automaton have been searched. In this paper we propose some improvements of the encoding of the transition relation for timed automata. The improvements are partially based on a new discretization scheme. The efficiency of the improved encoding is strongly supported by the experimental results. We also introduce a method for checking unreachability. Show more

Citation: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 417-434, 2004