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