Fundamenta Informaticae - Volume 14, issue 2

Article Type: Other

DOI: 10.3233/FI-1991-14201

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. i-viii, 1991

Authors: Vidyasankar, K.

Article Type: Research Article

Abstract: A database system is a collection of data items, read or written by transactions in a possibly interleaved fashion. An interleaved execution is assumed to be correct if the sequence of the steps of the transactions, called history , is serializable , that is, the effect of the execution is equivalent to that of some serial execution of the same transactions. In this paper we give a new characterization of serializability that brings out the inherent problem of serialization explicitly. We then give a graph-theoretic analogue of serializable histories. We define a new class of graphs, called serializable graphs …, whose properties are such that (i) a serializable graph can be associated with each serializable history, and this can be done for various notions of serializability of histories and for serializability under various sets of constraints, and (ii) a serializable history, in fact a serial one, can be associated with each serializable graph. We use serializable graphs to characterize, in an intuitive manner, serializable histories involving general multi-step transactions, where the same data item can be accessed by several read and write steps of a transaction in an arbitrary manner, and those involving nested transactions. We also define a new notion of serializability for nested transactions. This enables relating several acceptable concurrent executions of transactions, that are not serializable with the traditional transaction concept, to sequential behaviour. Serializability under this notion is also characterized. The main graph-theoretic properties used in these characterizations are a directed cutset matching property and graph contraction. Show more

DOI: 10.3233/FI-1991-14202

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 147-183, 1991

Authors: Becker, Bernd | Sparmann, Uwe

Article Type: Research Article

Abstract: In this paper testability aspects of Recursive Carry Computation adders are considered. The class of RCC-adders has been introduced in [5] and contains a wide range of different adder realizations (e.g., optimal time adders such as the the carry look-ahead adder of [8] and the conditional carry adder of [5]). We show that symbolic computation can be used to define this class and at the same time offers a uniform test approach which can be applied at an early stage of the design process. The class of RCC-adders itself splits into several subclasses which are specified by structural properties …of the overall computation scheme and functional properties of the basic cells. Optimal complete test sets with respect to two commonly used fault models, the single stuck-at fault model and the single cellular fault model, are developed for these RCC-subclasses. The cardinality of the test sets depends on the choice of the fault model and on structural properties of the RCC-subclass. To summarize our results, we finally obtain tables with upper and lower bounds characterizing the test complexity of classes of RCC-adders. The upper bounds are obtained by the effective construction of complete test sets. The cardinality of these sets varies between a logarithmic or linear number of patterns for an n -bit RCC-adder. Show more

DOI: 10.3233/FI-1991-14203

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 185-219, 1991

Authors: Darondeau, Philippe | Degano, Pierpaolo

Article Type: Research Article

Abstract: A notion of semantic action refinement is defined both on Synchronization Trees and on Causal Trees, a class of trees recently devised for giving a full account to causality [DD89]. The branching bisimulation, as introduced in [GW89a], is shown to be preserved under semantic action refinement. As a by-product, the axiomatization of the congruence induced by branching bisimulation which was given in [GW89a] is still valid under action refinement. Both results hold for Synchronization Trees and, with the needed extensions, for Causal Trees.

DOI: 10.3233/FI-1991-14204

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 221-234, 1991

Authors: Koutny, Maciej

Article Type: Research Article

Abstract: We discuss some of the problems concerning bisimulation relations over behaviour expressions representing non-sequential systems. The kind of bisimulation we investigate is derived from the notion of bisimulation relation between two Kripke structures, which provides a full characterisation of semantical equivalence of such structures w.r.t. the CTL* branching time temporal logic without the next-time operator. This new bisimulation on behaviour expressions, called CTL*-bisimulation, induces a congruence on recursion-free behaviour expressions, and in this paper we derive a sound and complete axiom system for this congruence.

DOI: 10.3233/FI-1991-14205

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 235-253, 1991

Authors: Mäkinen, Erkki

Article Type: Research Article

Abstract: This note discusses a hierarchy of different kind of context-free derivations by studying the corresponding Szilard languages. Especially, we introduce the leftmost and rightmost breadth-first derivations which are the counterparts of the well-known (depth-first) leftmost and rightmost derivations. It is shown that the Szilard languages related to different derivation types can be recognized by one-state automata which differ from each others by their memory devices.

DOI: 10.3233/FI-1991-14206

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 255-259, 1991

Authors: Kröger, Fred | Merz, Stephan

Article Type: Research Article

Abstract: We propose a temporal logic based on structures divided into several layers of linear “time scales” and give a sound and complete derivation system. The logic is applied to the formulation and verification of assertions about sequential recursive programs.

DOI: 10.3233/FI-1991-14207

Citation: Fundamenta Informaticae, vol. 14, no. 2, pp. 261-281, 1991