Fundamenta Informaticae - Volume 54, issue 2-3

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

Article Type: Other

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. i-i, 2003

Authors: Abraham, Uri | Pinhas, Tamar

Article Type: Research Article

Abstract: We compare two documents: the Alpha Architecture Reference Manual (from Compaq Computer Corporation) and the TLA^+ specification of the Alpha memory model (by Lamport, Sharma, Tuttle, and Yu). We compare the styles, the languages employed, and the fundamental assumptions (that is the basic frameworks of the two texts). We conclude that the TLA^+ specification is not so much a formalization of the Alpha Reference Manual text as it is a translation into a different framework. We …believe that a formalization of the Alpha Reference Manual can be useful, and we propose one. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 107-135, 2003

Authors: Barbuti, Roberto | Tesei, Luca

Article Type: Research Article

Abstract: We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against …attacks. Show more

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 137-150, 2003

Authors: Coja-Oghlan, Amin | Stehr, Mark-Olivier

Article Type: Research Article

Abstract: Revisiting the view of "Petri nets as monoids" suggested by Meseguer and Montanari, we give a direct proof of the well-known result that the class of Best/Devillers processes, which represents the behavior of Petri nets under the collective token semantics, has a sound and complete axiomatization in terms of symmetric monoidal categories. Using membership equational logic for the axiomatization, we prove the result by an explicit construction of a natural isomorphism between suitable functors. Our interest …in the collective token semantics is motivated by earlier work on the use of rewriting logic as a uniform framework for different Petri net classes, especially including high-level Petri nets, where individuality of tokens can be already expressed at the system level. Show more

Keywords: place/transition nets, Best/Devillers processes, collective token philosophy, membership equational logic, rewriting logic

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 151-164, 2003

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: Proving safety and liveness of parallel systems is of unquestionable importance in system construction activity. A proof method for systems represented by nets (cause-effect structures and Petri nets) is proposed. Its outline is the following. (1) Let a problem specification as a formal theory i.e. a language system with specific relation symbols (operations, in particular), axioms and first-order inference rules be given. For each symbol introduce a class of atomic c-e structures (counterpart of Petri net …transitions) to be the symbol's operational representative. (2) Using algebraic calculus of cause-effect structures, construct - from the atoms - a c-e structure and equivalent net intended to behave in accordance with the axioms (a mechanical step); (3) From the cause-effect structure just constructed, infer an algebraic structure and prove it to be a model (in terms of model theory) of the axiomatic system specifying the problem. Show more

Keywords: Cause-effect structures, Petri nets, specification, correctness, model theory

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 165-183, 2003

Authors: Farwer, Berndt | Kudlek, Manfred | Misra, Kundan

Article Type: Research Article

Abstract: This paper introduces higher-order Petri nets based on multiset rewriting. Some variations of the firing rule for high-level Petri nets following the nets-within-nets paradigm, i.e. allowing Petri nets as tokens, are discussed. All considerations keep in mind the possibile existence of a universal higher-order Petri net.

Keywords: Petri net, multiset rewriting, object net, nets-within-nets paradigm, universal Petri net

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 185-193, 2003

Authors: De Francesco, Nicolette | Santone, Antonella | Tesei, Luca

Article Type: Research Article

Abstract: We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main …point is that we are able to check more carefully the scope of indirect information flows. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 195-211, 2003

Authors: Kacprzak, Magdalena

Article Type: Research Article

Abstract: The paper presents an original logical system for reasoning about groups of interacting, autonomous processes, i.e. multi-agent systems. In the paper, an agent is considered as a couple consisting of a set of methods and of a queue of tasks. We show that the logic is not decidable. It is done by the reduction from the recurring domino problem.

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 213-220, 2003

Authors: Köhler, Michael | Rölke, Heiko

Article Type: Research Article

Abstract: In this work we present the model of "mobile object net systems" -- an algebraic formalisation of the "nets within nets"-paradigm. The formalism of "mobile object nets" is well suited to express the dynamics of open, mobile systems, since it allows tokens to be active. The algebraic theory of "mobile object net systems" covers an integrated view of the two major topics concurrency and locality, which are central in the area of mobile computing. As a …main result of this contribution, we derive an algebraic model in the "Petri nets are monoids" style. It is shown, that mobile object net systems are a conservative extension of the Petri net formalism. Show more

Keywords: concurrency, mobility, nets within nets, Petri nets as monoids

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 221-235, 2003

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

Article Type: Research Article

Abstract: We present Dynamic Hierarchical Machines (DHMs), an extension of Communicating Hierarchical Automata allowing dynamic activation of components. We give an operational semantics of DHMs and we provide examples of modeling in the context of security. We characterize a fragment of DHMs which are equivalent to Recursive Hierarchical Machines and therefore to Pushdown Machines.

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 237-252, 2003

Authors: Schmidt, Karsten

Article Type: Research Article

Abstract: We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.

Keywords: Petri net, state space, distributed verification

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 253-262, 2003

Authors: Skowron, Andrzej | Stepaniuk, Jarosław | Peters, James F.

Article Type: Research Article

Abstract: We discuss the relationships between information systems and classifications as well as between infomorphisms and definability of relations (between whole objects and their parts) in information systems. Infomorphisms between information systems (classifications) IS_1 and IS_2 make it possible to define some formulas over IS_2 by means of formulas over IS_1. The remaining formulas over IS_2 can be approximatively defined by means of formulas over IS_1. The approximation operations are defined using the rough …set approach. We present definitions and examples of such approximations. Show more

Keywords: information systems, classifications, rough set theory, infomorphisms, definability, approximations, approximate reasoning, information nets

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 263-277, 2003

Authors: Varpaaniemi, Kimmo

Article Type: Research Article

Abstract: This article continues research on the stubborn set method that constructs on-the-fly a reduced LTS that is CFFD-equivalent to the parallel composition of given LTSs. In particular, minimization of the number of successor states of a given state is reconsidered. The earlier suggested and/or-graph approach requires solving #P-complete counting problems in order to get the weights for the vertices of the and/or-graph. The "branch-and-bound" decision problem corresponding to the minimization of the sum of the computed weights is "only" NP-complete. …Unfortunately, #P-complete counting does not seem easily avoidable in the general case because it is PP-complete to check whether a given stubborn set produces at most as many successor states as another given stubborn set. Instead of solving each of the subproblems, one could think of computing approximate solutions in such a way that the total effect of the approximations is a useful approximation itself. Show more

Keywords: LTS, stubborn sets, and/or-graphs, approximability in optimization and counting

Citation: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 279-294, 2003