Fundamenta Informaticae - Volume 9, issue 4

Article Type: Other

DOI: 10.3233/FI-1986-9401

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. i-vi, 1986

Authors: Gerth, Rob | De Roever, W.P.

Article Type: Research Article

Abstract: An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete. This characterization is based on the fundamental notions of cooperation and interference, but does not use them as second order notions. The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between disjoint processes, as opposed to the interference freedom test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then, the cooperation test has been applied to characterize synchronous communication in Hoare’s Communicating Sequential Processes, Ichbia’s Ada, and Wirth’s …Modula-2, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for a new monitor based programming language for concurrency (Communicating Modules, CM) which combines distributed message passing between processes with interference through local variables of a process which are shared between its sub-processes. As such this is a first step towards the formal verification of object oriented systems. In this context, we also show how the method, traditionally cauched in terms of proof outlines, can be rendered syntax directed in a precise and formal way. In a separate paper, the proof system has been shown to be sound and (relatively) complete. Show more

DOI: 10.3233/FI-1986-9402

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. 371-399, 1986

Authors: Winskel, Glynn

Article Type: Research Article

DOI: 10.3233/FI-1986-9403

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. 401-419, 1986

Authors: Fernandez, C. | Nielsen, M. | Thiagarajan, P.S.

Article Type: Research Article

Abstract: This paper presents some results on non-sequential processes using the language of net theory. The results are concerned with the relationship between various formalizations of the intuition that the causality relation enforced by a process should be in some sense “finitely realizable”. The formalizations proposed are of very different flavours, based on notions of observability, approximability, state space covering and discreteness.

DOI: 10.3233/FI-1986-9404

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. 421-454, 1986

Authors: Ehrenfeucht, A. | Hoogeboom, H.J. | Rozenberg, G.

Article Type: Research Article

Abstract: Selective substitution grammars provide a rather general framework for the grammatically oriented formal language theory (see, e.g., [R1], [K], and [KR]). They were generalized in [R2] to coordinated table selective substitution systems (ds systems) which provide a convenient unifying framework for both grammars and machines (automata) . The present paper investigates coordinated pair (cp) systems which form a subclass of cts systems corresponding in a very natural way to push-down automata: thus cp systems generate context-free languages (all and only). This paper investigates the structure of computations in cp systems.

DOI: 10.3233/FI-1986-9405

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. 455-480, 1986

Authors: Harrison, Michael A.

Article Type: Research Article

Abstract: In this paper, we consider the problem of finding iteration theorems for various subfamilies of deterministic languages. Because deterministic languages are constrained in their generation, it is not possible to merely “pump substrings” as in the general context free case. We lay out, in detail, a collection of techniques for proving theorems of this type for deterministic context free languages.

DOI: 10.3233/FI-1986-9406

Citation: Fundamenta Informaticae, vol. 9, no. 4, pp. 481-508, 1986