Fundamenta Informaticae - Volume 93, issue 1-3

Article Type: Other

DOI: 10.3233/FI-2009-0083

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

Authors: Balicki, Krzysztof | Szpyrka, Marcin

Article Type: Research Article

Abstract: The paper presents a formal definition of XCCS – a graphical extension of CCS process calculus. The aim of this extension is to supply graphical means for creating models and thus to eliminate problems typical for modelling in textual manner inherent to CCS process algebra. XCCS diagrams consist of two layers, a graphical one that represents the structure of a modelled system and algebraic one that describes behaviour of individual agents. The graphical layer takes the …form of a directed graph, while the algebraic one is a set of sequences of algebraic equations similar to those in the CCS calculus. The formal definition presented in the paper deals with both parts of such models. At the end of the paper we define the Synchronization Relation and present the Basic Conversion Algorithm that converts XCCS diagrams into CCS scripts. Show more

Keywords: XCCS process algebra, formal definition, synchronization relation, Basic Conversion Algorithm

DOI: 10.3233/FI-2009-0084

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

Authors: Barbuti, Roberto | Maggiolo-Schettini, Andrea | Milazzo, Paolo | Tini, Simone

Article Type: Research Article

Abstract: P Systems are computing devices inspired by the structure and the functioning of a living cell. A P System consists of a hierarchy of membranes, each of them containing a multiset of objects, a set of evolution rules, and possibly other membranes. Evolution rules are applied to the objects of the same membrane with maximal parallelism. In this paper we present an extension of P Systems, called P Systems with Membrane Channels (PMC Systems), in which …membranes are enriched with channels and objects can pass through a membrane only if there are channels on the membrane that enable such a passage. We show that PMC Systems are universal even if only the simplest form of evolution rules is considered, and we give two application examples. Show more

DOI: 10.3233/FI-2009-0085

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 17-31, 2009

Authors: Barylska, Kamila | Ochma´nski, Edward

Article Type: Research Article

Abstract: The notion of persistency, based on the rule "no action can disable another one" is one of the classical notions in concurrency theory. We propose two ways of generalization of this notion: the first is "no action can kill another one" and the second "no action can kill another enabled one". We study the three notions in the context of place/transition nets, the fundamental class of Petri nets. We prove that the …three classes of persistency form an increased strict hierarchy. The final section of the paper deals with decision problems about persistency. We show that the set reachability problem is decidable for rational convex sets, and using this result we prove that all kinds of persistency are decidable in the class place/transition nets. Show more

DOI: 10.3233/FI-2009-0086

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 33-43, 2009

Authors: Bellia, Marco | Occhiuto, M. Eugenia

Article Type: Research Article

Abstract: M_parameters extend Java by allowing methods to have methods as parameters. [8] furnishes a semantics of m parameters and applications in OO programming. In this paper, we present an implementation of the extended language based on program preprocessing. We also discuss the integration of the extended programs with ordinary Java programs, and hence Java API. Furthermore, mc parameters are defined: they are a variant of m parameters for which the class hierarchy of the method passed …as parameter must be provided in the formal and actual parameter. Semantics for mc parameters is given but, in this case, an implementation with callbacks [20] is proposed. Eventually, we discuss how mc_parameters deal with overloaded methods. Show more

DOI: 10.3233/FI-2009-0087

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 45-64, 2009

Authors: Budzyńska, Katarzyna | Kacprzak, Magdalena | Rembelski, Paweł

Article Type: Research Article

Abstract: The aim of the paper is to present the software tool Perseus and show how it can be used to examine multi-agent systems where the ability to persuade is specified. Especially we want to study the issues such as: what arguments individuals use to successfully convince others, what type of a persuader guarantees a victory etc. This work describes implementation of the tool and discusses what questions about persuasion process Perseus can answer and how it …is done. Show more

DOI: 10.3233/FI-2009-0088

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 65-79, 2009

Authors: Bulling, Nils | Jamroga, Wojciech

Article Type: Research Article

Abstract: Alternating-time Temporal Logic (ATL) is probably themost influential logic of strategic ability that has emerged in recent years. The idea of ATL is centered around cooperation modalities: ≪A≫γ is satisfied if the group A of agents has a collective strategy to enforce temporal property γ against the worst possible response from the other agents. So, the semantics of ATL shares the "all-or-nothing" attitude of many logical approaches to computation. Such …an assumption seems appropriate in some application areas (life-critical systems, security protocols, expensive ventures like space missions). In many cases, however, one might be satisfied if the goal is achieved with reasonable likelihood. In this paper, we try to soften the rigorous notion of success that underpins ATL. Show more

DOI: 10.3233/FI-2009-0089

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 81-96, 2009

Authors: Czaja, Ludwik | Kudlek, Manfred

Article Type: Research Article

Abstract: We investigate relations between transition graphs and net structures. Whereas for a given net structure there always exists a reachability graph, the inverse problem to find a net structure for a given transition graph is not solvable in general. We present sufficient and necessary conditions for several classes of transition graphs such as general, pseudo-bounded, bounded and elementary transition graphs, corresponding to general and (pseudo-)bounded P/T nets or C/E nets. We also give maximal and …minimal solutions within an algebraic structure of net structures. The entire investigation is formulated in the framework of multiset theory. Show more

DOI: 10.3233/FI-2009-0090

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 97-110, 2009

Authors: Doroshenko, Anatoliy | Yatsenko, Olena

Article Type: Research Article

Abstract: An approach to formalized development of parallel programs using ontologies and algebra- algorithmic facilities is proposed. Ontology gives opportunity to describe the skeleton of the program representing main objects in the given subject domain, i.e. data, functions to process data and relations between functions. Once the skeleton of the program has been built, further development can be done in automated manner with the Integrated toolkit for Design and Synthesis (IDS) developed by the authors, which is …based on using algorithmic algebras facilities. The application of the approach is illustrated with an example of developing parallel MPI program in the subject domain of sorting algorithms. Show more

Keywords: ontology, algebra of algorithms, designing and synthesis of programs, parallel programs

DOI: 10.3233/FI-2009-0091

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 111-125, 2009

Authors: Gribovskaya, Natalya | Virbitskaite, Irina

Article Type: Research Article

Abstract: Timed transition systems are a widely studied model for real-time systems. The intention of the paper is to show the applicability of the general categorical framework of openmaps in order to prove that timed delay equivalence is indeed an equivalence relation in the setting of timed transition systems with invariants. In particular, we define a category of the model under consideration and an accompanying (sub)category of observations to which the corresponding notion of open maps is …developed. We then use the open maps framework to obtain an abstract equivalence relation which is established to coincide with timed delay bisimulation. Show more

Keywords: timed transition systems, timed delay equivalence, category theory, open maps

DOI: 10.3233/FI-2009-0092

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 127-142, 2009

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