Fundamenta Informaticae - Volume 29, issue 1-2

Authors: Hotz, Günter | Pitsch, Gisela

Article Type: Research Article

Abstract: Coupled-Context-Free Grammars are a natural generalization of context-free grammars obtained by combining nonterminals to corresponding parentheses which can only be substituted simultaneously. Refering to their generative capacity we obtain an infinite hierarchy of languages that comprises the context-free ones as the first and all those generated by Tree Adjoining Grammars (TAGs) as the second element. The latter is important because today, TAGs are commonly used to model the syntax of natural languages. Here, we present a completely new approach to analyse this language hierarchy. It solves the word problem for the class of languages generated by TAGs in time O(n6 …), n length of the input, by reducing it to the analysis of sequences of parentheses. Show more

DOI: 10.3233/FI-1997-291201

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 1-26, 1997

Authors: Dembiński, Piotr

Article Type: Research Article

Abstract: A truly concurrent and timeless semantics is proposed for a composition of sequential, non-deterministic processes with asynchronous communication. It is shown when this semantics differs from simple interleaving. Implementation-dependent time constraints determine a subset of all computations of the timeless semantics. This set is precisely characterized for given constraints. It is shown how the same set may be generated by a timed transition system, i.e., how to simulate time-constrained and concurrent computations by sequential, non-deterministic system. The paper includes a proof of the correctness of such simulation.

DOI: 10.3233/FI-1997-291202

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 27-50, 1997

Authors: Baeten, J.C.M. | Bergstra, J.A.

Article Type: Research Article

Abstract: We discuss the key notions of discrete time process algebra in the setting of ACP. Time is measured in discrete slices. The emphasis is on absolute, relative and parametric time notation. Note: Partial support received from ESPRIT Basic Research Action 7166, C0NCUR2.

DOI: 10.3233/FI-1997-291203

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 51-76, 1997

Authors: Huzar, Zbigniew | Magott, Jan

Article Type: Research Article

Abstract: The paper contains extensions of specification language LOTOS in three directions: time-consuming actions, real-time and performance evaluation constructions. Time-consuming actions seem to be more natural than instantaneous actions and they are well suited for real-time system specification and for its performance evaluation. The notions of beginning and termination of the time-consuming action enable to impose time restrictions on beginning and termination times of activities. From performance evaluation point of view it is often important to know explicit how long a specific action has been executed (not when the action has been completed only). We have also introduced a time-out as …a specific action. An expressive power of this action has been discussed. We have defined such a performance evaluation extension of LOTOS that can be used as a modelling language for performance evaluation of distributed systems. A true concurrency semantics (in the sense that it refers to the fact that actions with durations may overlap in time) for this extension is defined. Show more

DOI: 10.3233/FI-1997-291204

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 77-96, 1997

Authors: Seda, Anthony Karel

Article Type: Research Article

Abstract: Quasi-metrics have been used in several places in the literature on domain theory and the formal semantics of programming languages. In this paper, we consider the role of quasi-metrics in the fixed point semantics of logic programs, examining in detail a quite general process by which fixed points of immediate consequence operators can be found. This work takes as its starting point: (i) Fitting's recent application of the Banach contraction mapping theorem in logic programming; (ii) a theorem of Rutten which generalizes both the contraction mapping theorem and the Knaster-Tarski theorem; (iii) Smyth's work on totally bounded spaces and compact …ordered spaces as domains of computation. Our results therefore are theoretical and to be viewed as a contribution to the mathematical foundations of computer science. Show more

DOI: 10.3233/FI-1997-291205

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 97-117, 1997

Authors: Düntsch, Ivo | Gediga, Günther

Article Type: Research Article

Abstract: We exhibit some new connections between structure of an information system and its corresponding semilattice of equivalence relations. In particular, we investigate dependency properties and introduce a partial ordering of information systems over a fixed object set U which reflects the sub-semilattice relation on the set of all equivalence relations on U.

DOI: 10.3233/FI-1997-291206

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 119-133, 1997

Authors: Peters, James F.

Article Type: Research Article

Abstract: A linear form of Reed-Roscoe Timed Communicating Sequential Processes mechanized with the Higher Order Logic Proof System is presented. The syntax for the Real-Time Linear CSP (RTLCSP) language is sufficient to describe the behavior of time-constrained communicating processes in real-time systems. The operational semantics of RTLCSP is expressed in terms of inference rules and Coloured Hierarchical Petri nets for a transition system for real-time programs. RTLCSP processes are characterized in terms of an extension of the Lynch-Tuttle signature for communicating processes. The signature of a process is helpful in reasoning about process behavior and in defining the semantics of empty …processes or processes with hidden actions. The linear character of RTLCSP stems from its resource consciousness inasmuch as restrictions are placed on the number of times that a process can be restarted. The complete mechanization of RTLCSP in HOL (called RTLCSP-HOL) is presented in detail. The presentation includes a brief introduction to HOL itself to permit experimentation with RTLCSP-HOL. Sample HOL proofs relative to RTLCSP constructs are also given. Show more

DOI: 10.3233/FI-1997-291207

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 135-163, 1997

Authors: Egly, Uwe

Article Type: Research Article

Abstract: In this paper, we examine different definitional transformations into normal form for intuitionistic logic. In contrast to the classical case, “intuitionistic clauses” may contain implications and quantifiers. Usually, such definitional transformations introduce labels defining subfor-mulae. An obvious optimization is the use of implications instead of equivalences whenever possible, which can reduce the size of the resulting normal form. We compare the optimized transformation with the unoptimized transformation with respect to the shortest cut-free LJ-derivation of the resulting normal forms. The comparison is based on a sequence (Hk )k∈N of formulae for which the following hold: (i) there exist cut-free …LJ-proofs of the unoptimized normal form of Hk with length double-exponential in k, and (ii) any cut-free LJ-proof of the optimized normal form of Hk has length non-elementary in k. The reason for the different behaviour is the simulation of analytic cuts by the unoptimized translation, which is not possible when the optimization is applied. Show more

DOI: 10.3233/FI-1997-291208

Citation: Fundamenta Informaticae, vol. 29, no. 1-2, pp. 165-201, 1997