Fundamenta Informaticae - Volume 13, issue 2

Article Type: Other

DOI: 10.3233/FI-1990-13201

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. i-viii, 1990

Authors: Mauw, S. | Veltink, G.J.

Article Type: Research Article

Abstract: Traditional methods for programming sequential machines are inadequate for specifying parallel systems. Because debugging of parallel programs is hard, due to e.g. non-deterministic execution, verification of program correctness becomes an even more important issue. The Algebra of Communicating Processes (ACP) is a formal theory which emphasizes verification and can be applied to a large domain of problems ranging from electronic circuits to CAM architectures. The manual verification of specifications of small size has already been achieved, but this cannot easily be extended to the verification of larger industrially relevant systems. To deal with this problem we need computer tools to …help with the specification, simulation, verification and implementation. The first requirement for building such a set of tools is a specification language. In this paper we introduce PSFd (Process Specification Formalism – draft) which can be used to formally express processes in ACP. In order to meet the modern requirements of software engineering, like reusability of software, PSFd supports the modular construction of specifications and parameterization of modules. To be able to deal with the notion of data, ASF (Algebraic Specification Formalism) is embedded in our formalism. As semantics for PSFd a combination of initial algebra semantics and operational semantics for concurrent processes is used. A comparison with programming languages and other formal description techniques for the specification of concurrent systems is included. Show more

DOI: 10.3233/FI-1990-13202

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. 85-139, 1990

Authors: Maggiolo-Schettini, Andrea | Winkowski, Józef

Article Type: Research Article

Abstract: Timed Petri nets and their behaviours are considered. A concept of a seminet is introduced. which generalizes the concept of a net, and suitable operations on seminets are defined, which allow constructing seminets from atoms corresponding to places and transitions. The behaviours of seminets are given in the form of so called configuration systems, a notion close to labelled event structures. Such behaviours can be combined with the aid of operations corresponding to those on seminets. In particular, the behaviour of a compound seminet can be obtained by combining the behaviours of components.

Keywords: timed Petri net, seminet, composition, hiding, synchronization structure, configuration, timed configuration system, delayed configuration, eager configuration system, eager kernel

DOI: 10.3233/FI-1990-13203

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. 141-170, 1990

Authors: Căzănescu, Virgil Emil | Ştefănescu, Gheorghe

Article Type: Research Article

Abstract: We develope a formalism for the algebraic study of flowchart schemes and their behaviours, based on a new axiomatic looping operation, called feedback. This formalism is based on certain flownomial expressions . Such an expression is built up from two types of atomic schemes (i.e., elements in a double-ranked set X considered as unknown computation processes, and elements in a “theory” T considered as known computation processes) by using three operations: sum, composition, and feedback. Flownomial expressions are subject to certain rules of identification. The axiomatization of flowchart schemes is based on the fact that a flowchart scheme …may be identified with a class of isomorphic flownomial expressions in normal form. The corresponding algebra for flowchart schemes is called biflow . This axiomatization is extended to certain types of behaviour. We present axiomatizations for accessible flowchart schemes, reduced flowchart schemes, minimal flowchart schemes with respect to the input behaviour, minimal flowchart schemes with respect to the input-output behaviour etc. Some results are new, others are simple translations in terms of feedback of previous results obtained by using Elgot’s iteration or Kleene’s repetition. The paper also contains some historical comments. Show more

DOI: 10.3233/FI-1990-13204

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. 171-210, 1990

Authors: Fülop, Z. | Vágvölgyi, S.

Article Type: Research Article

Abstract: The concept of top-down tree automata with prefix look-ahead is introduced. It is shown that a tree language is the set of irreducible trees of a left-linear term rewriting system if and only if it can be recognized by a one-state deterministic top-down tree automaton with pre fix look-ahead.

DOI: 10.3233/FI-1990-13205

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. 211-226, 1990

Authors: Krynicki, Michał

Article Type: Research Article

Abstract: In papers [4,5] Pawlak introduced the notion of a rough set and approximation space. In [6] Pawlak formulated some concept of rough logic. The notion of the approximate truth was considered by many philosophers and logicians and in the last time by computer scientists. This was motivated by some research in artificial intelligence as for example expert systems, approximate reasoning methods and information system with imprecise information. The concept of rough logic introduced in [6] based on the notion of approximate truth determined by rough sets. Following these ideas Rasiowa and Skowron in [7] proposed the apropriate first order …logic for concepts of rough definability. We denote this logic by L R . In [9] Szczerba proposed some logic with additional quantifier as rough concepts logic. We denote this logic by L(Q R ) . The aim of this paper is a comparizing of these two logics with respect to their expressive power and giving some propositions of some modificated versions of rough concepts logics. We use more or less standard notation. By [a ]R we denote the equivalence class of the element a with respect to the equivalence relation R. We write L ⩽ L ′ if expressive power of the logic L is weaker then t.he expressive power of the logic L ′ (i.e. each class of models definable by a sentence from L is also definable by a sentence from L ′ ). If L ⩽ L ′ and L ′ ⩽ L then we say that L and L ′ are equivalent and denote this by L ≡ L ′ . If L ⩽ L ′ but L ≢ L ′ then we write L < L ′ . Show more

DOI: 10.3233/FI-1990-13206

Citation: Fundamenta Informaticae, vol. 13, no. 2, pp. 227-235, 1990