Fundamenta Informaticae - Volume 67, issue 1-3

Authors: Burkhard, Hans-Dieter | Czaja, Ludwik | Lindemann, Gabriela | Suraj, Zbigniew

Article Type: Other

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. vii-vii, 2005

Authors: Barbuti, Roberto | Cataudella, Stefano

Article Type: Research Article

Abstract: In this paper we present a use of abstract interpretation techniques for reducing synchronization overhead in an object calculus. First we present the new raconcς calculus, an extension of an already existing calculus for supporting reentrant locks. Then we use an abstract form of this calculus to check when synchronization operations may be safely eliminated from statements. Thus our approach may be used to improve performance in object oriented languages by eliminating locks, without the risks …caused by "manual" optimizations performed by programmers. Show more

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 1-12, 2005

Authors: Barbuti, Roberto | Cataudella, Stefano | Maggiolo-Schettini, Andrea | Milazzo, Paolo | Troina, Angelo

Article Type: Research Article

Abstract: We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a probabilistic transition system can be derived from it. We use the algorithm in the development of an interpreter for the model, which we use to simulate the evolution of molecular systems. In particular, we show the results of the simulation of a real example of …enzymatic activity. Moreover, we apply the probabilistic model checker PRISM to the transition system derived by the model of this example, and we show the results of model checking of some illustrative properties. Show more

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 13-27, 2005

Authors: Bellia, Marco | Occhiuto, M. Eugenia

Article Type: Research Article

Abstract: Higher order programming is considered a good methodology for program design and specification, furthermore it is fundamental for rapid prototyping. The paper is devoted to higher order programming in Java and, more in general, in the OO programming paradigm. We discuss introspection to write higher order programs and compare this technique with other different, interesting approaches, including function emulation and function integration. Finally, we address the problem of embedding, in the OO paradigm, the …mechanisms for method passing and method extraction that are basic to the higher order programming methodology. Show more

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 29-44, 2005

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: A method of constructing net (cause-effect structure and Petri net) from a specification given as an axiomatic system and proving behaviour of the net to conform to the specification is presented and illustrated by two examples.

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 45-64, 2005

Authors: Farwer, Berndt | Köhler, Michael

Article Type: Research Article

Abstract: Composition of modules to larger units is a technique frequently used during the software development life cycle. It is mostly used in a "bottom up" fashion, suggested by the principles of object orientation, where the composition of simple objects to a complex one plays a central role. Composition in Petri nets has been studied in the form of place and transition fusion. Zero-Safe Nets represent a special approach, which allows the use of more …complex synchronisation structures, so-called transactions. The definition of transactions is based on interleaving semantics, i.e. on firing-sequences. Problems arise, since the definition is not closed with respect to the permutation of actions. This paper presents a partial order concurrency semantics for zero-safe nets based on Petri net processes. Using these semantics, a characterisation of such transactions closed with respect to permutation of concurrent actions becomes possible. Show more

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 65-75, 2005

Authors: Gomolińska, Anna

Article Type: Research Article

Abstract: In this paper, we study general notions of satisfiability and meaning of formulas and sets of formulas in approximation spaces. Rather than proposing one particular form of rough satisfiability and meaning, we present a number of alternative approaches. Approximate satisfiability and meaning are important, among others, for modelling of complex systems like systems of adaptive social agents. Finally, we also touch upon derivative concepts of meaning and applicability of rules.

Keywords: information granule, Pawlak information system, approximation space, rough satisfiability/meaning of formulas, rough applicability of a rule

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 77-92, 2005

Authors: Klunder, Barbara | Ochmański, Edward | Stawikowska, Krystyna

Article Type: Research Article

Abstract: Up to now, star-connected rational expressions were considered only as expressions defining trace languages. In this paper we study the class of flat languages defined by this kind of rational expressions. We consider regular languages inducing recognizable trace languages and its subclasses: languages of finite ranks and star-connected languages. Main results are the following: rank of any star-connected language is finite; any star-connected language has an automaton with connected simple cycles; two pumping lemmas for …star-connected languages. Moreover, we show that none of the investigated classes is closed under complement and that the class of languages of finite ranks is not closed under intersection. Finally, we briefly mention some decision problems and formulate several open questions. Show more

Keywords: trace language, star-connected rational expressions, finite automata

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 93-105, 2005

Authors: Kryvyy, Sergiy | Matvyeyeva, Lyudmila | Lopatina, Mariya

Article Type: Research Article

Abstract: Formal Methods are a set of methods and tools based on mathematical modeling and formal logic that are used to specify and verify requirements and architecture of hardware or software systems. They can also include means of automatic proving of key properties of designed software or hardware systems. In this paper automatic system is presented which specifies formally and verify designed software or hardware system specified in MSC language. Automatic system is represented as technological process …that applies the formal modeling technique of Petri nets and is based on linear algebra methods of analysis, namely, solving the systems of linear equations over the set of natural numbers, in order to research the properties of a system under design. The system is first modeled as a Petri net, and then this model is analyzed. The understanding of the system which results from the analysis will lead to a hopefully errorless system. Show more

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 107-120, 2005

Authors: Kudlek, Manfred

Article Type: Research Article

Abstract: It is demonstrated that the introduction of probability into Petri nets increases their power, in particular for their reachability sets. To achieve this the definition of accepted languages by probabilistic finite automata or probabilistic Turing machines with complexity restriction has to be modified.

Citation: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 121-130, 2005