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