Fundamenta Informaticae - Volume 79, issue 3-4

Authors: Köhler, Michael

Article Type: Research Article

Abstract: In this article I will prove undecidability results for elementary object net systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach which is called the "netswithin-nets" paradigm. EOS are special object net systems which have a two leveled structure.

Keywords: decidability, nets within nets, Petri nets, reachability

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 401-413, 2007

Authors: Köhler, Michael

Article Type: Research Article

Abstract: Agent oriented software engineering is seen as the approach taking object oriented approaches one step ahead. The design of agent systems is based on three fundamental perspectives: the functional, the team-interactional and the organisational perspective. The organisational perspective becomes a central design issue if the number of agents is large or the environment is unstable. While the functional perspective is well founded in the planning theory of artificial intelligence and the interactional perspective is …rooted in the theory of speech-acts and formal ontologies, the organisational perspective is still an active research area with several open questions. In this paper we define a formal organisation model for agent systems based on Petri nets and show how agent oriented software engineering can benefit from this model. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 415-430, 2007

Authors: Kryvyy, Sergiy | Matvyeyeva, Lyudmila

Article Type: Research Article

Abstract: We present in this paper the algorithm which performs the translation of MSC'2000 diagrams into Petri net modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement theMSC'2000 standard with the formal definition of the MSC 〈condition〉 element by means of process algebra. This translation algorithm is the part of the automated verification system which formally specifies and verifies a designed software or hardware system specified in the MSC language and is presented …in [1] and [2]. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 431-445, 2007

Authors: Kudlek, Manfred

Article Type: Research Article

Abstract: The concept of semilinear sets is generalized to commutative semirings. It is shown that the semilinear sets over commutative semirings are exactly the algebraic/rational sets over such structures.

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 447-452, 2007

Authors: Kurkowski, Mirosław | Penczek, Wojciech

Article Type: Research Article

Abstract: In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol proving either reachability or unreachability of an undesired state. We exemplify all our notions …on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS. Show more

Keywords: security protocols, model checking, authentication

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 453-471, 2007

Authors: Lomuscio, Alessio | Raimondi, Franco | Woźna, Bożena

Article Type: Research Article

Abstract: We use MCMAS-X to verify authentication properties in the TESLA secure stream protocol. MCMAS-Xis an extension to explicit and deductive knowledge of the OBDD-based model checker MCMAS a verification tool for multi-agent systems.

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 473-486, 2007

Authors: Mazurkiewicz, Antoni

Article Type: Research Article

Abstract: In the paper triangular graphs are discussed. The class of triangular graphs is of special interest as unifying basic features of complete graphs and trees. The main issue addressed in the paper is to characterize class of triangular graphs (defined globally) by local means. Namely, it is proved that any triangular graph can be constructed from a singleton by successive extensions with nodes having complete neighborhoods. Next, the proved theoretical properties are applied for designing some …local algorithms for triangular graphs: for elections a leader and for constructing their spanning trees. The fairness of these algorithms is proved, which means that any node can be elected and any spanning tree can be constructed by execution of these algorithms. Show more

Keywords: triangular graphs, local computations, leader elections, spanning trees

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 487-495, 2007

Authors: Peters, James F. | Skowron, Andrzej | Stepaniuk, Jaroslaw

Article Type: Research Article

Abstract: The problem considered in this paper is the extension of an approximation space to include a nearness relation. Approximation spaces were introduced by Zdzis?aw Pawlak during the early 1980s as frameworks for classifying objects by means of attributes. Pawlak introduced approximations as a means of approximating one set of objects with another set of objects using an indiscernibility relation that is based on a comparison between the feature values of objects. Until now, the focus has …been on the overlap between sets. It is possible to introduce a nearness relation that can be used to determine the "nearness" of sets of objects that are possibly disjoint and, yet, qualitatively near to each other. Several members of a family of nearness relations are introduced in this article. The contribution of this article is the introduction of a nearness relation that makes it possible to extend Pawlak's model for an approximation space and to consider the extension of generalized approximations spaces. Show more

Keywords: rough sets, approximation, approximation space, classification, feature, nearness relation, neighbourhood, proximity space

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 497-512, 2007

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: Two recent developments in the field of formal languages are Parsing Expression Grammar (PEG) and packrat parsing. The PEG formalism is similar to BNF, but defines syntax in terms of recognizing strings, rather than constructing them. It is, in fact, precise specification of a backtracking recursive-descent parser. Packrat parsing is a general method to handle backtracking in recursive-descent parsers. It ensures linear working time, at a huge memory cost. This paper reports an experiment that consisted …of defining the syntax of Java 1.5 in PEG formalism, and literally transcribing the PEG definitions into parsing procedures (accidentally, also in Java). The resulting primitive parser shows an acceptable behavior, indicating that packrat parsing might be an overkill for practical languages. The exercise with defining the Java syntax suggests thatmore work is needed on PEG as a language specification tool. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 513-524, 2007

Authors: Stepaniuk, Jaroslaw

Article Type: Research Article

Abstract: In this paper, we show that approximation spaces are basic structures for knowledge discovery from multi-relational data. The utility of approximation spaces as fundamental objects constructed for concept approximation is emphasized. Examples of basic concepts are given throughout this paper to illustrate how approximation spaces can be beneficially used in many settings.

Keywords: rough sets, approximation spaces, multi-relational data mining

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 525-539, 2007

Authors: Suraj,, Zbigniew | Fryc, Barbara

Article Type: Research Article

Abstract: Approximate Petri nets (AP-nets) can be used for the knowledge representation and approximate reasoning. The AP-net model is defined on the basis of the rough set approach, fuzzy Petri nets and coloured Petri nets. One of the main advantages of AP-net model is a possibility to present the reachability set of a given AP-net by means of an occurrence graph. Such graphs can serve, among others, for analyzing and evaluating an approximate reasoning realized by using …AP-net model. The main contribution of the paper is to present the algorithms for construction and analysis of occurrence graphs for the AP-nets, especially in the context of searching for the best decision and finding the shortest distance in order to compute such decision. This approach can be applied to the design and analysis of the formal models for expert systems, control systems, communication systems, etc. Show more

Keywords: approximate Petri nets, approximate reasoning, knowledge representation, occurrence graphs

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 541-551, 2007

Authors: Suraj, Zbigniew | Pancerz, Krzysztof

Article Type: Research Article

Abstract: This paper provides new algorithms for computing consistent and partially consistent extensions of information systems. A maximal consistent extension of a given information system includes only objects corresponding to known attribute values which are consistent with all rules extracted from the original information system. A partially consistent extension of a given information system includes objects corresponding to known attribute values which are consistent to a certain degree with the knowledge represented by …rules extracted from the original information system. This degree can be between 0 and 1, 0 for the full inconsistency and 1 for the full consistency. The algorithms presented here do not involve computing any rules true in a given information system. This property differentiates them from methods presented in the earlier papers which concerned extensions of information systems. Show more

Keywords: rough sets, information systems, consistent extensions, partially consistent extensions

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 553-566, 2007

Authors: Wolski, Marcin

Article Type: Research Article

Abstract: The present paper investigates approximation spaces in the context of mathematical structures which axiomatise the notion of nearness. Starting with the framework of information quanta which distinguishes two levels of information structures, namely property systems (the first level) and information quantum relational systems (the second level), we shall introduce the notion of Pawlak property system. These systems correspond bijectively to finite approximation spaces, i.e. their respective information quantum relational systems. Then we …characterise Pawlak property systems in terms of symmetric topological spaces. In the second part of the paper, these systems are defined by means of topological structures based on the concept of nearness. We prove that the category of Pawlak property systems is isomorphic to the category of finite topological nearness spaces and provide its additional topological characterisation. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 567-577, 2007

Authors: Zbrzezny, Andrzej | Półrola, Agata

Article Type: Research Article

Abstract: Reachability analysis for timed automata using SAT-based methods was considered in many papers, occurring to be a very efficient model checking technique. In this paper we show how to apply this method of verification to timed automata with discrete data, i.e., to standard timed automata augmented with integer variables. The theoretical description is supported by some preliminary experimental results.

Citation: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 579-593, 2007