Fundamenta Informaticae - Volume 72, issue 1-3

Article Type: Other

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. i-i, 2006

Authors: Andreeva, Maria V. | Virbitskaite, Irina B.

Article Type: Research Article

Abstract: The intention of the paper is to develop a framework for weak observational equivalences in the setting of a real-time partial order model. In particular, we introduce a family of equivalences of linear time – branching time spectrum based on interleaving, causal tree and partial order semantics, in the setting of a dense time extension of stable event structures with internal actions. We study the relationships between the equivalences showing, on one hand, the discriminating power …of the approaches of the spectrum and, on the other hand, the coincidence of some semantics in a concrete approach. Furthermore, when dealing with particular subclasses of the model under consideration, there is no difference between more concrete and more abstract observations. Show more

Keywords: Real-Time Systems, Comparative Concurrency Semantics, Observational Equivalences, Timed Event Structures

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 1-19, 2006

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

Article Type: Research Article

Abstract: The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent elements and operators of sequencing, looping, containment and parallel composition. The looping operator allows tying up the ends of a sequence, thus creating a circular sequence which can represent a membrane. We show that a membrane calculus recently proposed can be encoded into CLS. We use our calculus to …model interactions among bacteria and bacteriophage viruses, and to reason on their properties. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 21-35, 2006

Authors: Bazan, Jan G.

Article Type: Research Article

Abstract: This paper introduces an approach to behavioral pattern identification as a part of a study of temporal patterns in complex dynamical systems. Rough set theory introduced by Zdzisław Pawlak during the early 1980s provides the foundation for the construction of classifiers relative to what are known as temporal pattern tables. It is quite remarkable that temporal patterns can be treated as features that make it possible to approximate complex concepts. This article introduces what are known …as behavior graphs. Temporal concepts approximated by approximate reasoning schemes become nodes in behavioral graphs. In addition, we discuss some rough set tools for perception modeling that are developed for a system for modeling networks of classifiers. Such networks make it possible to recognize behavioral patterns of objects changing over time. They are constructed using an ontology of concepts delivered by experts that engage in approximate reasoning about concepts embedded in such an ontology. We also present a method that we call a method for on-line elimination of non-relevant parts (ENP). This method was developed for on-line elimination of complex object parts that are irrelevant for identifying a given behavioral pattern. The article includes results of experiments that have been performed on data from a vehicular traffic simulator useful in the identification of behavioral patterns by drivers. Show more

Keywords: Behavior, complex patterns, identification, rough sets, concept approximation, dynamical system

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 37-50, 2006

Authors: Bednarczyk, Marek A. | Jamroga, Wojciech | Pawłowski, Wiesław

Article Type: Research Article

Abstract: Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest – the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problemof model checking properties of a class of the logic on Petri hypernets is shown to be PSPACE-complete.

Keywords: dynamic mobile agents, dynamic mobile agents, temporal logics, model checking

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 51-63, 2006

Authors: Chrz�stowski-Wachtel, Piotr

Article Type: Research Article

Abstract: When we model workflows with Petri nets, we call a workflow net sound, if it neither makes any transition dead nor it produces trash tokens in such a way that for every input token exactly one token appears eventually on the output place. We assume that the initial marking consists always of one token on the input place. However, sometimes it is necessary to take into account arbitrary markings, for instance when we make a recovery from an …unexpected situation during the workflow execution. An arbitrary marking is sound if it eventually produces exactly one output token without the possibility to leave any trash tokens. The paper addresses the problem of determining the proper control recovery, when unexpected situation arises, and we must detour from the normal execution. When we create an arbitrary control state during the recovery, it is easy to overlook some consequences and create either trash tokens or a deadlock in the future. The problem of determining if a given marking is sound is addressed in the paper in the context of structured nets. The presented linear solution is a necessary and sufficient condition for soundness of markings in structured nets. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 65-79, 2006

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: A specification of systems based on message passing paradigm is proposed. To this end, an algebraic structure called a semiring of formal polynomials with restricted idempotency of multiplication is taken and fix-point equations specifying (parallel) systems are constructed. Their solution provides an "implementation" of the system, in particular, a Petri net of various kind. Moreover, it determines a global information on capability of sending or receiving a message by objects from a local information on their …readiness to do this. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 81-93, 2006

Authors: Doroshenko, Anatoliy | Shevchenko, Ruslan

Article Type: Research Article

Abstract: In recent years light-weighted formal methods in construction and analysis of complex concurrent software system are of growing interest. In this paper a new rule-action based term rewriting framework, called TermWare, is proposed and its application to software system analysis is described to provide better cost effectiveness of software maintenance under varied requirements and specifications of operation. The main advantage is light-weighted formal model based on not computational semantics but on particular …properties of software system to be analyzed. Such approach eliminates the need in full formal analysis of software system and allows extreme flexibility of applications in two major concerns: high adaptability to changeable environment and easy reengineering and component reuse. The language and formal semantics of the system are defined. A new semantic model, called term system with action, is proposed for TermWare. A case study with some representative examples in source code analysis and software development with TermWare framework is presented. Show more

Keywords: term rewriting, rule-based programming, software system analysis

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 95-108, 2006

Authors: Farwer, Berndt | Köhler, Michael

Article Type: Research Article

Abstract: While it often makes sense to use pointer-based semantics (sometimes called reference semantics) to model components of a system that are in close proximity, this kind of modelling becomes increasingly infeasible for distant components. The notion of distance here is to be seen relative with respect to the system being modelled. We use local and global name spaces to model the necessary paradigm shift for systems of communicating mobile agents. As a concrete example of modelling that requires …discrimination of notions of proximity or distance, we study a scenario of mobile devices with wireless communications capabilities. The communication can be done directly between two agents or via a system of wireless network routers. To model such a system, we introduce object Petri nets that integrate both semantic paradigms found in the literature, i.e. reference semantics and value semantics. Formal definitions are given and some basic properties are proved. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 109-122, 2006

Authors: Farwer, Berndt | Varea, Mauricio

Article Type: Research Article

Abstract: This paper summarises two approaches, Dual Flow Nets (DFN) and Object Petri Nets (OPN), and offers a translation mechanism between them. While the DFN model tackles the separation of control and data flow computing aspects, the OPN model has a more generalised structure. The separation between control and data flow can enhance the readability of models, and allows different tools to operate on distinct parts of the model. The aim of this paper is to show …how the modelling based on control/data-flow analysis can benefit from an object-based Petri net approach. Tool support and a translation mechanism that is faithful are presented, giving an extra dimension (hierarchy) to the existing paradigm of control and data flow interacting in a model. Our methodology provides a comprehensive separation of these two parts, which can be used to feed analysis or synthesis tools, while still being able to reason about both parts through formal methods of verification. Show more

Citation: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 123-137, 2006