Fundamenta Informaticae - Volume 51, issue 1-2

Authors: Czaja, Ludwik | Burkhard, Hans-Dieter | Starke, Peter

Article Type: Other

Keywords:

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. i-ii, 2002

Authors: Barbuti, Roberto | De Francesco, Nocoletta | Santone, Antonella | Tesei, Luca

Article Type: Research Article

Abstract: The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified …control of an airplane. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 1-11, 2002

Authors: Bono, Viviana | Tiuryn, Jerzy

Article Type: Research Article

Abstract: This paper is devoted to a comprehensive study of polymorphic subtypes with products. We first present a sound and complete Hilbert style axiomatization of the relation of being a subtype in presence of →, × type constructors and the ∀ quantifier, and we show that such axiomatization is not encodable in the system with →,∀ only. In order to give a logical semantics to such a subtyping relation, we propose a new form of a sequent …which plays a key role in a natural deduction and a Gentzen style calculi. Interestingly enough, the sequent must have the form E⊢T, where E is a non-commutative, non-empty sequence of typing assumptions and T is a finite binary tree of typing judgements, each of them behaving like a pushdown store. We study basic metamathematical properties of the two logical systems, such as subject reduction and cut elimination. Some decidability/undecidability issues related to the presented subtyping relation are also explored: as expected, the subtyping over →,×,∀ is undecidable, being already undecidable for the →,∀ fragment (as proved in [15]), but for the ×,∀ fragment it turns out to be decidable. Show more

Keywords: Polymorphic Subtyping, Cartesian Product, Logical Semantics, Sequent

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 13-41, 2002

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: Four semantic domains for Place/Transition Petri nets and their relationships are considered. They are monoids of respectively: firing sequences, processes, traces and dependence graphs. For each of them the analysis and synthesis problem is stated and solved. The monoid of processes is defined in a non-standard way. Nets under consideration involve weights of arrows and capacities (finite or infinite) of places. However, the analysis and synthesis tasks require nets to be pure, i.e. each of their …transition must have the pre-set and post-set disjoint. Show more

Keywords: P/T Petri nets, processes, traces, dependence graphs, analysis, synthesis

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 43-58, 2002

Authors: Dembiński, Piotr | Półrola, Agata

Article Type: Research Article

Abstract: The paper presents a modification of the standard partitioning technique to generate abstract state spaces preserving similarity for Timed Automata. Since this relation is weaker than bisimilarity, most of the obtained models (state spaces) are smaller than bisimilar ones, but still preserve the universal fragments of branching time temporal logics. The theoretical results are exemplified for strong, delay, and observational simulation relations.

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 59-89, 2002

Authors: Farwer, Bernard

Article Type: Research Article

Abstract: In this paper we discuss possibilities of modelling protocols by objects in object-based high-level Petri nets. Some advantages of dynamically modifying the structure of token objects are discussed and the need for further investigations into mathematically rigorous foundations of object net formalisms incorporating facilities for such operations on its token nets is emphasised.

Keywords:

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 91-101, 2002

Authors: Gomolińska, Anna

Article Type: Research Article

Abstract: In this paper we focus upon a comparison of some generalized rough approximations of sets, where the classical indiscernibility relation is generalized to any binary reflexive relation. We aim at finding the best of several candidates for generalized rough approximation mappings, where both definability of sets by elementary granules of information as well as the issue of distinction among positive, negative, and border regions of a set are taken into account.

Keywords: granulation of information, approximation space, rough approximation

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 103-119, 2002

Authors: Lomazova, Irina A.

Article Type: Research Article

Abstract: Nested Petri nets (NP-nets) is a Petri net extension, allowing tokens in a net marking to be represented by marked nets themselves. The paper discusses applicability of NP-nets for modeling task planning systems, multi-agent systems and recursive-parallel systems. A comparison of NP-nets with some other formalisms, such as OPNs of R. Valk, recursive parallel programs of O. Kushnarenko and Ph. Schnoebelen and process algebras is given. Some aspects of decidability for object-oriented …Petri net extensions are also discussed. Show more

Keywords: Petri nets, nested Petri nets, multi-agent systems, task planning systems, recursive-parallel programs, process algebras, decidability

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 121-133, 2002

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

Article Type: Research Article

Abstract: Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular length and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E. Clarke et al. for model checking of linear time temporal logic (LTL). Our paper shows how the concept of bounded model checking can be …extended to ACTL (the universal fragment of CTL). The implementation of the algorithm for Elementary Net Systems is described together with the experimental results. Show more

Keywords: Bounded model checking, logic ACTL (ECTL), bounded semantics, translation to SAT, Elementary Net Systems, system verification

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 135-156, 2002

Authors: Peters, James F. | Skowron, Andrzej | Stepaniuk, Jarosław | Ramanna, Sheela

Article Type: Research Article

Abstract: This article introduces structural aspects in an ontology of approximate reason. The basic assumption in this ontology is that approximate reason is a capability of an agent. Agents are designed to classify information granules derived from sensors that respond to stimuli in the environment of an agent or received from other agents. Classification of information granules is carried out in the context of parameterized approximation spaces and a calculus of granules. Judgment in agents is a …faculty of thinking about (classifying) the particular relative to decision rules derived from data. Judgment in agents is reflective, but not in the classical philosophical sense (e.g., the notion of judgment in Kant). In an agent, a reflective judgment itself is an assertion that a particular decision rule derived from data is applicable to an object (input). That is, a reflective judgment by an agent is an assertion that a particular vector of attribute (sensor) values matches to some degree the conditions for a particular rule. In effect, this form of judgment is an assertion that a vector of sensor values reflects a known property of data expressed by a decision rule. Since the reasoning underlying a reflective judgment is inductive and surjective (not based on a priori conditions or universals), this form of judgment is reflective, but not in the sense of Kant. Unlike Kant, a reflective judgment is surjective in the sense that it maps experimental attribute values onto the most closely matching descriptors (conditions) in a derived rule. Again, unlike Kant's notion of judgment, a reflective judgment is not the result of searching for a universal that pertains to a particular set of values of descriptors. Rather, a reflective judgment by an agent is a form of recognition that a particular vector of sensor values pertains to a particular rule in some degree. This recognition takes the form of an assertion that a particular descriptor vector is associated with a particular decision rule. These considerations can be repeated for other forms of classifiers besides those defined by decision rules. Show more

Keywords: approximation neuron, approximate reason, parameterized approximation space, reflective judgment, pattern recognition, rough sets

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 157-173, 2002

Authors: Raś, Zbigniew W. | Gupta, Shishir

Article Type: Research Article

Abstract: In papers [4,5], query answering system based on distributed knowledge mining was introduced and investigated. In paper by Ras and Wieczorkowska [3], the notion of an action rule was introduced and for its application domain e-business was taken. In this paper, we generalize the notion of action rules in a similar way to handling global queries in [4,5]. Mainly, when values of attributes for a given customer, used in action rules, can not be easily changed …by business user, definitions of these attributes are extracted from other sites of a distributed knowledge system. To be more precise, attributes at every site of a distributed knowledge system are divided into two sets: stable and flexible. Values of flexible attributes, for a given consumer, sometime can be changed and this change can be influenced and controlled by a business user. However, some of these changes (for instance to the attribute ``profit'') can not be done directly to a chosen attribute. In this case, definitions of such an attribute in terms of other attributes have to be learned. These new definitions are used to construct action rules showing what changes in values of flexible attributes, for a given consumer, are needed in order to re-classify this consumer the way business user wants. But, business user may be either unable or unwilling to proceed with actions leading to such changes. In all such cases we may search for definitions of these flexible attributes looking at either local or remote sites for help. Show more

Keywords: knowledge discovery, distributed information systems, e-commerce

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 175-184, 2002

Authors: Richling, Jan | Popova-Zeugmann, Louchka | Werner, Matthias

Article Type: Research Article

Abstract: In this paper, we introduce our concept of composability and present the MSS architecture as an example for a composable architecture. MSS claims to be composable with respect to timing properties. We discuss, how to model and prove properties in such an architecture with time-extended Petrinets. As a result, the first step of a proof of composability is presented as well as a new kind of Petrinet, which is more suitable for modeling architectures like MSS.

Keywords: real time, composability, Petrinets, duration nets, π-PN

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 185-200, 2002

Authors: Suraj, Zbigniew | Peters, J.F. | Rzasa, W.

Article Type: Research Article

Abstract: Decision algorithms useful in classifying meteorological volumetric radar data are the subject of described in the paper experiments. Such data come from the Radar Decision Support System (RDSS) database of Environment Canada and concern summer storms created in this country. Some research groups used the data completed by RDSS for verifying the utility of chosen methods in volumetric storm cells classification. The paper consists of a review of experiments that were made on the data from …RDSS database of Environment Canada and presents the quality of particular classifiers. The classification accuracy coefficient is used to express the quality. For five research groups that led their experiments in a similar way it was possible to compare received outputs. Experiments showed that the Support Vector Machine (SVM) method and rough set algorithms which use object oriented reducts for rule generation to classify volumetric storm data perform better than other classifiers. Show more

Keywords: rough sets, cross-validation, data mining, knowledge discovery, meteorological volumetric radar data, pattern recognition

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 201-214, 2002

Authors: Varpaaniemi, Kimmo

Article Type: Research Article

Abstract: Combinatorial explosion which occurs in parallel compositions of LTSs can be alleviated by letting the stubborn set method construct on-the-fly a reduced LTS that is CFFD- or CSP-equivalent to the actual parallel composition. This article considers the problem of minimizing the number of successor states of a given state in the reduced LTS. The problem can be solved by constructing an and/or-graph with weighted vertices and by finding a set of vertices …that satisfies a certain constraint such that no set of vertices satisfying the constraint has a smaller sum of weights. Without weights, the and/or-graph can be constructed in low-degree polynomial time w.r.t. the length of the input of the problem. However, since actions can be nondeterministic and transitions can share target states, it is not known whether the weights are generally computable in polynomial time. Consequently, it is an open problem whether minimizing the number of successor states is as ``easy'' as minimizing the number of successor transitions. Show more

Keywords: LTS's, CFFD-equivalence, CSP-equivalence, stubborn sets, and/or-graphs

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 215-234, 2002

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: Contextual nets, or Petri nets with read arcs, are models of concurrent systems with context dependent actions. The problem of reachability in such nets consists in finding a sequence of transitions that leads from the initial marking of a given contextual net to a given goal marking. The solution to this problem that is presented in this paper consists in constructing a finite complete prefix of the unfolding of the given contextual net, that is a …finite prefix in which all the markings that are reachable from the initial marking are present, and in searching in each branch of this prefix for the goal marking by solving an appropriate linear programming problem. Show more

Keywords: contextual net, Petri net with read arcs, contextual occurrence net, branching process, unfolding, configuration, history, cut, narking, state, complete prefix, linear programming

Citation: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 235-250, 2002