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