Fundamenta Informaticae - Volume 93, issue 1-3

Authors: Grochowalski, Piotr | Pancerz, Krzysztof

Article Type: Research Article

Abstract: The paper gives the outline of an ontology for the rough set theory and its applications. This ontology will be applied in intelligent searching the Rough Set Database System. A specialized editor from the Protege system is used to define the ontology.

Keywords: ontology, rough sets, data mining, knowledge discovery, database systems

DOI: 10.3233/FI-2009-0093

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 143-154, 2009

Authors: Gruska, Damas P.

Article Type: Research Article

Abstract: A quantification of process's security by quantification of an amount of information flow is defined and studied in the framework of timed process algebras. The resulting quantified security is compared with other (qualitative) security notions. Unprecise and limited observations are defined and discussed.

Keywords: information flow, information theory, opacity, surprisal, uncertainty, security, unprecise and limited observations

DOI: 10.3233/FI-2009-0094

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 155-169, 2009

Authors: van Hee, Kees M. | Sidorova, Natalia | Voorhoeve, Marc | van derWerf, Jan Martijn

Article Type: Research Article

Abstract: Deleting a record from a database table without modifying other records or tables can easily lead to a violation of the database constraints. The same holds for other database operations. In this paper we generate descriptions of transactions triggered by a given operation, guaranteeing that if the database is in a consistent state before a transaction starts, it will be in a consistent state after it is finished. We describe transactions as models of a special …subclass of Coloured Petri nets where token values are vectors of identifiers. This class is powerful enough to model transaction execution and it allows for some formal analysis, like soundness. Show more

DOI: 10.3233/FI-2009-0095

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 171-184, 2009

Authors: Jakubowska, Gizela | Dembiński, Piotr | Penczek, Wojciech | Szreter, Maciej

Article Type: Research Article

Abstract: In this paper we offer a methodology allowing for simulation of security protocols, implemented in the higher-level language Estelle, using scenarios designed for external attacks. To this aim we apply a translation of specifications of security protocols from Common Syntax to Estelle and an encoding of schemes of attacks into Estelle scenarios. We show that such an intelligent simulation may efficiently serve for validating security protocols.

DOI: 10.3233/FI-2009-0096

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 185-203, 2009

Authors: Kohler-Bußmeier, Michael | Heitmann, Frank

Article Type: Research Article

Abstract: In this work we present object net systems, i.e. Petri nets with nets as token objects, which are equipped with channels that allow to transfer net-tokens in the vertical dimension of the nested marking. These channels are a modelling element powerful enough to describe a direct simulation of counter programs which shows that typical net problems like boundedness, coverability, and reachability are undecidable.

DOI: 10.3233/FI-2009-0097

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 205-219, 2009

Authors: Kudlek, Manfred | Totzke, Patrick | Zetzsche, Georg

Article Type: Research Article

Abstract: Multiset finite Automata, a model equivalent to regular commutative grammars, are extended with a multiset store and the accepting power of this extended model of computation is investigated. This type of multiset automata come in two flavours, varying only in the ability of testing the storage for emptiness. This paper establishes normal forms and relates the derived language classes to each other as well as to known multiset language classes.

Keywords: commutative grammars and automata, Petri nets, multiset rewriting and languages

DOI: 10.3233/FI-2009-0098

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 221-233, 2009

Authors: Kudlek, Manfred | Totzke, Patrick | Zetzsche, Georg

Article Type: Research Article

Abstract: The previously introduced multiset language classes defined by multiset pushdown automata are being explored with respect to their closure properties and alternative characterizations.

Keywords: commutative grammars and automata, Petri nets, multiset rewriting and languages

DOI: 10.3233/FI-2009-0099

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 235-244, 2009

Authors: Kurkowski, Mirosław | Penczek, Wojciech

Article Type: Research Article

Abstract: A new approach to verification of timed security protocols is given. The idea consists in modelling a finite number of users (including an intruder) of the computer network and their knowledge about secrets by timed automata. The runs of the product automaton of the above automata correspond to all the behaviours of the protocol for a fixed number of sessions. Verification is performed using the module BMC of the tool VerICS.

Keywords: timed security protocols, model checking, authentication

DOI: 10.3233/FI-2009-0100

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 245-259, 2009

Authors: Moshkov, Mikhail Ju. | Skowron, Andrzej | Suraj, Zbigniew

Article Type: Research Article

Abstract: The minimal inhibitory rules for information systems can be used for construction of classifiers. We show that almost all information systems from a certain large class of information systems have relatively short minimal inhibitory rules. However, the number of such rules is not polynomial in the number of attributes and the number of objects. This class consists of all k-valued information systems, k ⩾ 2, with the number of objects polynomial in the number of attributes. …Hence, for efficient construction of classifiers some filtration techniques in rule generation are necessary. Another way is to work with lazy classification algorithms based on inhibitory rules. Show more

Keywords: Information systems, minimal inhibitory rules, irreducible inconsistent systems of equations

DOI: 10.3233/FI-2009-0101

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 261-272, 2009

Authors: Nguyen, Linh Anh

Article Type: Research Article

Abstract: We report on our implementation of a tableau prover for the description logic ALC, which is based on the EXPTIME tableau algorithm using global caching for ALC that was developed jointly by us and Goré [9]. The prover, called TGC for "Tableaux with Global Caching", checks satisfiability of a set of concepts w.r.t. a set of global assumptions by constructing an and-or graph, using tableau rules for expanding nodes. We have implemented for TGC a special …set of optimizations which co-operates very well with global caching and various search strategies. The test results on the test set T98-sat of DL'98 Systems Comparison indicate that TGC is an efficient prover for ALC. This suggests that global caching together with the set of optimizations used for TGC is worth implementing and experimenting also for other modal/description logics. Show more

Keywords: automated reasoning, tableaux, description logic, global caching, optimizations

DOI: 10.3233/FI-2009-0102

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 273-288, 2009

Authors: Niewiadomski, Artur | Penczek, Wojciech | Szreter, Maciej

Article Type: Research Article

Abstract: The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the …(prototype) tool BMC4UML and some experimental results are presented. Show more

Keywords: UML, Bounded Model Checking, symbolic verification

DOI: 10.3233/FI-2009-0103

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 289-303, 2009

Authors: Rataj, Artur | Woźna, Bożena | Zbrzezny, Andrzej

Article Type: Research Article

Abstract: The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be build. Therefore, we have developed the J2TADD tool that translates a Java program to a network of TADDs; the paper presents this tool. The J2TADD tool works in two stages. The first one consists …in translation of a Java code to an internal assembly language (IAL). Then, the resulting assembly code is translated to a network of TADDs. We exemplify the use of the translator by means of the following well-known concurrency examples written in Java: race condition problem, dining philosophers problem, single sleeping barber problem and readers and writers problem. Show more

DOI: 10.3233/FI-2009-0104

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 305-324, 2009

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: The paper is an attempt to see how much we can learn about a given Parsing Expression Grammar with the help of classical concepts used in the construction of predictive top-down parsers.

DOI: 10.3233/FI-2009-0105

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 325-336, 2009

Authors: Wegener, Jan-Thierry | Popova-Zeugmann, Louchka

Article Type: Research Article

Abstract: We present Petri nets with time windows (tw-PN) where each place is associated with an interval (window). Every token which arrives at a place gets a real-valued clock which shows its "age". A transition can fire when all needed tokens are "old enough". When a token reaches an "age" equal to the upper bound of the place where it is situated, the "token's age", i.e., clock will be reset to zero. Following …this we compare these time dependent Petri nets with their (timeless) skeletons. The sets of both their reachable markings are equal, their liveness behaviour is different, and neither is equivalent to Turing machines. We also prove the existence of runs where time gaps are possible in the tw-PN, which is an extraordinary feature. Show more

DOI: 10.3233/FI-2009-0106

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 337-352, 2009