Fundamenta Informaticae - Volume 43, issue 1-4

Authors: Burkhard, Hans-Dieter | Starke, Peter | Czaja, Ludwik

Article Type: Other

DOI: 10.3233/FI-2000-43123419

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. i-ii, 2000

Authors: Andreeva, Maria V. | Bozhenkova, Elena N. | Virbitskaite, Irina B.

Article Type: Research Article

Abstract: The intention of the paper is to extend the testing methodology to a model of event structures with a dense time domain. Alternative characterizations of timed testing relations are provided. We also present algorithms for deciding timed testing for a subclass of the model under consideration. The key to our decision algorithms is that timed testing equivalences can be reduced to appropriate symbolic bisimulations.

Keywords: Concurrency Theory, Real Time Processes, Timed Event Structures, Testing, Bisimulation, Decidability

DOI: 10.3233/FI-2000-43123401

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 1-20, 2000

Authors: Bednarczyk, Marek A. | Borzyszkowski, Andrzej M. | Somla, Rafał

Article Type: Research Article

Abstract: The problem of finite completeness of categories of Petri nets is studied. Since Petri nets have finite products, the problem reduces to the issue of the existence of equalizers. We show that the categories of Petri nets with general and Winskel morphisms do not admit equalizers, and hence are not finitely complete. The main positive result of the paper states that reachable Petri nets with multiplicative morphisms form a finitely complete category. As an application of this result, some well-known categories are shown to be finitely complete. For instance, since all morphisms between reachable safe Petri nets are multiplicative, it …follows that the category of reachable safe Petri nets is finitely complete. Show more

Keywords: Categories of Petri nets, products, equalizers, (finite) completeness

DOI: 10.3233/FI-2000-43123402

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 21-48, 2000

Authors: Czaja, Ludwik | Kudlek, Manfred

Article Type: Research Article

Abstract: In this paper we define a certain class of process languages viewing processes as bipartite graphs with an associative operation (sequential composition) on them. They describe finite evolutions of Petri nets. When extended to sets, we get an ω-complete semiring such that rational, linear, and algebraic sets of such processes can be defined as least fixed points of systems of equations. With a norm of processes also iteration lemmata can be obtained. Finally, we also present a related structure of directed acyclic graphs.

Keywords: formal languages, iteration lemmata, processes, Petri nets

DOI: 10.3233/FI-2000-43123403

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 49-60, 2000

Authors: Farwer, Berndt

Article Type: Research Article

Abstract: Object based Petri nets are becoming increasingly popular in many fields of computer science. The possibility to model real-world objects as separate Petri nets supports the need for modular design of complex systems. So far object net approaches have been based on the presumption that the object nets' structure remains unchanged in all processes. This paper sheds some light on possible extensions of high-level Petri nets to incorporate the dynamical evolution of Petri net structures. The exposition is based on the Linear Logic encoding of Petri nets ([1], [12]) and coloured Petri nets ([4]). It provides a basic semantics for …modifying net structures which can be employed in a framework of nets within nets, i.e. situations where Petri nets (so-called token nets) themselves are used as tokens in an underlying environment net. Show more

DOI: 10.3233/FI-2000-43123404

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 61-79, 2000

Authors: Foremniak, Adrianna | Starke, Peter H.

Article Type: Research Article

Abstract: Structural analysis explores the relation between local structural properties and the global functionality of nets. Here we consider Signal-Event systems under a generalized firing rule. The free-choice property and the deadlock-trap property are known from Petri net theory. We define them for Signal-Event nets and draw some consequences for liveness properties of Signal-Event systems.

Keywords: structural deadlock, structural trap, deadlock-trap property, extended free choice nets, extended simple nets, homogeneous nets, (place-)liveness of a net

DOI: 10.3233/FI-2000-43123405

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 81-104, 2000

Authors: Haar, Stefan

Article Type: Research Article

Abstract: This paper investigates Occurrence (Petri) Nets on two levels: their structural theory and their interpretation in branching unfolding semantics of Petri Net systems. The key issue is the decomposition of occurrence nets into substructures given by the node relations associated with causal ordering, concurrency, and conflict. In addition to lines and cuts, which have long been studied in the context of causal nets ([1]), we introduce and study branches, trails, choices, and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. On the semantic level, we introduce partial order logics …to be interpreted on two different kind of frames, given by substructures of occurrence nets: on the frame of cuts, the CTL* type logics BFC and BLC, and the “non-branching” logic LLC, taylored to the frame given by the lattice of choices. Show more

Keywords: Concurrency, Occurrence (Petri) nets, Semantics, Partial Order Logics

DOI: 10.3233/FI-2000-43123406

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 105-127, 2000

Authors: Hannebauer, Markus

Article Type: Research Article

Abstract: Several interesting practical problems in process control, planning and scheduling can be expressed and solved using the model of constraint satisfaction problems. At least four drawbacks of this classical model directly relate to areas of distribution: complexity, scalability, privacy and robustness. Hence, research on distributed constraint satisfaction problems is a new direction in the area of multi-agent systems. A typical engineering task in distributed constraint satisfaction is the design of the distribution itself. A careful look at this task reveals that the design of distribution is critical to the quality and efficiency of the problem solving process and is itself …an optimization problem. In this article we formalize different variants of this configuration problem and prove them to be all at least NP-complete. For solving these problems, we present two local operators, agent melting and agent splitting, that can be combined to allow for an autonomous and dynamic reconfiguration of the organizational structure of the problem-solving agents. We prove sequences of these operators to be sufficient for solving any given configuration problem. We also briefly describe what practical steps are necessary to exploit the rather theoretical result of the proof in realistic applications. Show more

Keywords: multi-agent systems, distributed constraint satisfaction, autonomous dynamic reconfiguration, partitioning, agent melting, agent splitting

DOI: 10.3233/FI-2000-43123407

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 129-151, 2000

Authors: Lanotte, Ruggero | Maggiolo-Schettini, Andrea | Peron, Adriano

Article Type: Research Article

Abstract: We propose Timed Cooperating Automata (TCAs), an extension of the model Cooperating Automata of Harel and Drusinsky, and we investigate some basic properties. In particular we consider variants of TCAs based on the presence or absence of internal activity, urgency and reactivity, and we compare the expressiveness of these variants with that of the classical model of Timed Automata (TAs) and its extensions with periodic clock constraints and with silent moves. We consider also closure and decidability properties of TCAs and start a study on succinctness of their variants with respect to that of TAs.

Keywords: Timed automata, Expressiveness, Closure properties, Succinctness

DOI: 10.3233/FI-2000-43123408

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 153-173, 2000

Authors: Latvala, Timo | Heljanko, Keijo

Article Type: Research Article

Abstract: We consider the verification of linear temporal logic (LTL) properties of Petri nets, where the transitions can have both weak and strong fairness constraints. Allowing the transitions to have weak or strong fairness constraints simplifies the modeling of systems in many cases. We use the automata theoretic approach to model checking. To cope with the strong fairness constraints efficiently we employ Streett automata where appropriate. We present memory efficient algorithms for both the emptiness checking and counterexample generation problems for Streett automata.

Keywords: Verification, model checking, fairness, Streett automata, counterexamples

DOI: 10.3233/FI-2000-43123409

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 175-193, 2000

Authors: Lomazova, Irina A.

Article Type: Research Article

Abstract: Nested Petri nets is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. Decidability of some crucial for verification problems shows that, in spite of their ”unflat” structure, nested Petri nets maintain significant properties of ordinary Petri nets. A comparison with some other Petri net models is given. The formalism allows generalization to a recursive case, when a nested Petri net may generate its own copy as its element. Two simple examples illustrate the approach.

Keywords: hierarchical multi-agent systems, nested Petri nets, well-structured transition systems, decidibility

DOI: 10.3233/FI-2000-43123410

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 195-214, 2000

Authors: Münch, Ines | Lindemann - v.Trzebiatowski, Gabriela

Article Type: Research Article

Abstract: Conceptual modeling is an important basis for developing general purpose systems for information and service management. In this paper, we present concepts for the analysis and design of a system of agents in which agents represent interests of individuals or groups. In particular, we develop a semantic model of agent domain knowledge by introducing analytical concepts for service scheduling which is the envisioned application of our prototypical system ChariTime.

Keywords: agent-oriented design, conceptual modeling, service scheduling

DOI: 10.3233/FI-2000-43123411

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 215-226, 2000

Authors: Nepomniaschaya, Anna S. | Dvoskina, Maria A.

Article Type: Research Article

Abstract: In this paper we propose a natural straight forward implementation of Dijkstra's shortest path algorithm on a model of associative parallel processors of the SIMD type with bit-serial (or vertical) processing (the STAR-machine). In addition, we show how to extend this implementation for restoring the shortest path from the source vertex to a given vertex. These algorithms of implementation are represented as the corresponding STAR procedures whose correctness is verified and time complexity is evaluated.

Keywords: Dijkstra's shortest path algorithm, the single-source shortest path problem, a directed weighted graph, associative parallel processing, time complexity

DOI: 10.3233/FI-2000-43123412

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 227-243, 2000

Authors: Penczek, Wojciech | Szreter, Maciej | Gerth, Rob | Kuiper, Ruurd

Article Type: Research Article

Abstract: The ”state explosion problem” can be alleviated by using partial order reduction techniques. These methods rely on expanding only a fragment of the full state space of a program, which is sufficient for verifying the formulas of temporal logics LTL−X or CTL−X* (i.e., LTL or CTL* without the next state operator). This is guaranteed by preserving either a stuttering maximal trace equivalence or a stuttering bisimulation between the full and the reduced state space. Since a stuttering bisimulation is much more restrictive than a stuttering maximal trace equivalence, resulting in less powerful reductions for CTL−X* , …we study here partial order reductions that preserve equivalences ”in-between”, in particular a stuttering simulation which is induced by the universal fragment of CTL:−X* , called ACTL−X* The reductions generated by our method preserve also branching simulation and weak simulation, but surprisingly, they do not appear to be included into the reductions obtained by Peled's method for verifying LTL−X properties. Therefore, in addition to ACTL−X* reduction method we suggest also an improvement of the LTL−X reduction method. Moreover, we prove that reduction for concurrency fair version of ACTL−X* is more efficient than for ACTL−X* . Show more

DOI: 10.3233/FI-2000-43123413

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 245-267, 2000

Authors: Peters, James F. | Skowron, Andrzej | Suraj, Zbigniew

Article Type: Research Article

Abstract: The paper deals with an automatic concurrent control design method derived from the specification of a discrete event control system represented in the form of a decision table. The main stages of our approach are: the control specification by decision tables, generation of rules from the specification of the system behavior, and converting rules set into a concurrent program represented in the form of a Petri net. Our approach is based on rough set theory [17].

DOI: 10.3233/FI-2000-43123414

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 269-290, 2000

Authors: Polkowski, Lech | Skowron, Andrzej

Article Type: Research Article

Abstract: Rough Mereology has been proposed as a paradigm for approximate reasoning in complex information systems. Its primitive notion is that of a predicate of rough inclusion which gives for any two entities of discourse the degree in which one of them is a part of the other. Rough Mereology may be regarded as an extension of Rough Set Theory as it proposes to argue in terms of similarity relations induced from a rough inclusion instead of reasoning in terms of more strict indiscernibility relations. Rough Mereology is also a generalization of Mereology i.e. a theory of reasoning based on the …notion of a part. Classical languages of mathematics are of two-fold kind: the language of set theory (naive or formal) expressing classes of objects as sets consisting of ”elements”, ”points” etc. suitable for objects perceived as built of ”atoms” and applied to structures perceived as discrete and the language of part relations suitable for e.g. continuous objects like solids, regions, etc. where two objects are related to each other by saying that one of them is a part of the other. Mereological theories for reasoning about complex structures are at the heart of Qualitative Spatial Reasoning. In this paper, we study basic aspects of Rough Mereology in Information Systems. Mereology makes the distinction between entities perceived as individuals (singletons), to which the part predicate may be applied, and entities perceived as distributive classes (sets, lists, general names etc.) of entities. This distinction is made formal and precise within Ontology i.e. Theory of Being based on the primitive notion of the copula is which is also a basic ingredient of theories for Spatial Reasoning. The practical aim of Ontology is to elaborate a system of concepts (notions, names, sets of entities) about which the reasoning is carried out. Therefore, we begin our study with an analysis of a simple rough set-based Ontology (the template ontology) in Information Systems and in this setting we present our approach to Mereology in Information Systems. In this framework we introduce Rough Mereology and we present some ways for defining rough inclusions. We demonstrate applications of Rough Mereology to approximate reasoning taking as the case subject Qualitative Spatial Reasoning. We address here some of its mereo-topological as well as mereo-geometrical aspects. Show more

Keywords: rough sets, information systems/tables, ontology, mereology, rough mereology, spatial reasoning, mereo-topology, mereo-geometry

DOI: 10.3233/FI-2000-43123415

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 291-320, 2000

Authors: Roch, Stephan

Article Type: Research Article

Abstract: Signal-event nets provide a modular modeling technique based on Petri nets. Actions of a module can be activated or can be prevented by another module through condition arcs. One-sided synchronization of modules is done by signal-events, which cause the execution of actions in steps. But due to condition arcs and signal-events simultaneous firing of steps may lead to markings, which are not reachable by conventional sequential interleaving. We give a criterion, in which situations simultaneous firing of steps can be safely omitted, without missing reachable markings.

Keywords: Discrete event systems, signal-event nets, reachability analysis

DOI: 10.3233/FI-2000-43123416

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 321-330, 2000

Authors: Schröter, Kay | Lindemann - v.Trzebiatowski, Gabriela | Fritsche, Lutz

Article Type: Research Article

Abstract: Fast and easy access to all relevant data is of most importance in medical diagnostics and therapy. Electronic patient records can fulfil these requirements much better than common paper-based records. This article describes the TBase2 system, an example of such an electronic patient record. It was developed in close cooperation with the Department of Nephrology at the university hospital Charité in Berlin. Due to its flexibility TBase2 can easily be adapted to the demands of other departments. Beside supporting the daily care for patients, TBase2 also gathers detailed data of high validity ideally suited for medical research.

Keywords: electronic patient record, web-based applications

DOI: 10.3233/FI-2000-43123417

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 343-353, 2000

Authors: Varpaaniemi, Kimmo

Article Type: Research Article

Abstract: The stubborn set method is one of the methods that try to relieve the state space explosion problem that occurs in state space generation. Spending some time in looking for “good” stubborn sets can pay off in the total time spent in generating a reduced state space. This article shows how the method can exploit tools that solve certain problems of logic programs. The restriction of a definition of stubbornness to a given state can be translated into a variable-free logic program. When a stubborn set satisfying additional constraints is wanted, the additional constraints should be translated, too. It is …easy to make the translation in such a way that each acceptable stubborn set of the state is represented by at least one stable model of the program, each stable model of the program represents at least one acceptable stubborn set of the state, and for each pair in the representation relation, the number of certain atoms in the stable model is equal to the number of enabled transitions of the represented stubborn set. So, in order to find a stubborn set which is good w.r.t. the number of enabled transitions, it suffices to find a stable model which is good w.r.t. the number of certain atoms. The article also presents a new NP-completeness result concerning stubborn sets. Show more

Keywords: reachability analysis, reduced state space generation, stubborn sets, variable-free logic programs, stable models, NP-completeness

DOI: 10.3233/FI-2000-43123418

Citation: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 355-375, 2000