Fundamenta Informaticae - Volume 30, issue 1

Authors: Gasarch, William | Velauthapillai, Mahendran

Article Type: Research Article

Keywords: Inductive inference, queries

DOI: 10.3233/FI-1997-30101

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 1-9, 1997

Authors: Kiehn, Astrid | Hennessy, Matthew

Article Type: Research Article

Abstract: We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPPr , Basic Parallel Processes with communication, obtained by omitting the restriction operator from CCS. Decision procedures are given for both strong and weak versions of location equivalence and ST-bisimulation.

Keywords: process algebra, observation equivalence, non-interleaving semantics, decidability

DOI: 10.3233/FI-1997-30102

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 11-30, 1997

Authors: Madlener, Klaus | Otto, Friedrich

Article Type: Research Article

Abstract: Following the course set by A. Markov (1951), S. Adjan (1958), and M. Rabin (1958), C. Ó'Dúnlaing (1983) has shown that certain properties of finitely generated Thue congruences are undecidable in general. Here we prove that many of these undecidability results remain valid even when only finitely generated Thue congruences on a fixed two-letter alphabet Σ2 are considered. In contrast to a construction given by P. Schupp (1976) which applies to groups only, we use a modified version of a technical lemma from A. Markov's original paper. Based on this technical result we can carry the result of A. …Sattler-Klein (1996), which says that certain Markov properties remain undecidable even when they are restricted to finitely generated Thue congruences that are decidable, over to the alphabet Σ2 . Show more

Keywords: Thue congruence, finitely presented monoid, Markov property, two-letter alphabet

DOI: 10.3233/FI-1997-30103

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 31-44, 1997

Authors: Paun, Gheorghe

Article Type: Research Article

Abstract: This paper is an up-to-dated survey of results about the power of controlled extended H systems of various types. Such systems are finite generative devices based on the splicing operation, which, in turn, is a model of the DNA recombination. When no control is imposed on the splicing operation, we get a characterization of regular languages. When a control is considered, we obtain characterizations of recursively enumerable languages. We briefly discuss here H systems with control mechanisms similar to those in regulated rewriting area in formal language theory. We do not present proofs, but only definitions, results, and bibliographical information. …Looking for characterizations of families in Chomsky hierarchy other than those of regular and of recursively enumerable languages, we closely investigate the H systems with permitting context conditions. We disprove a conjecture of Chakaravarthy and Krithivasan: such systems of radius one and using only one-sided context conditions can generate all context-free languages (the conjecture was that a characterization of linear languages is obtained). Some open problems are also mentioned. Show more

DOI: 10.3233/FI-1997-30104

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 45-57, 1997

Authors: Peltier, Nicolas

Article Type: Research Article

Abstract: The use of regular tree grammars to represent and build models of formulae of first-order logic without equality is investigated. The combination of regular tree grammars with equational constraints provides a powerful and general way of representing Herbrand models. We show that the evaluation problem (i.e. the problem of finding the truth value of a formula in a given model) is decidable when models are represented in the way we propose. We also define a method to build such representations of models for first-order formulae. These results are a powerful extension of our former method for simultaneous search for refutations …and models. Show more

Keywords: Automated Deduction, Model Building, Tree Automata, Regular Tree Grammars

DOI: 10.3233/FI-1997-30105

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 59-81, 1997

Authors: Trakhtenbrot, B.A.

Article Type: Research Article

DOI: 10.3233/FI-1997-30106

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 83-95, 1997

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: A correspondence between processes of Petri nets and partitioned matrices over freely generated semirings is described. This correspondence implies a correspondence between operations of composing processes sequentially and in parallel and operations of multiplying and juxtaposing the respective partitioned matrices. It results in a characterization of partitioned matrices corresponding to processes of a given net and, consequently, allows one to represent processes by their matrices.

Keywords: Petri net, process, sequential composition, parallel composition, interchange, partitioned matrix, multiplication, juxtaposition

DOI: 10.3233/FI-1997-30107

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 97-107, 1997

Authors: Zhang, Yan | Foo, Norman Y.

Article Type: Research Article

Abstract: Recent work on reasoning about action has shown that there exists an interesting connection between action specifications and state constraints — it is possible to extract state constraints from action specifications. This work provides us another way to describe the behaviour of dynamic systems. In this paper, we address the problem of generating action invariants from action specifications, and generalizing action invariants into state constraints. We first propose a persistence-based formalism of actions, and show that the generation of action invariants is achieved from action specifications by reasoning about persistence. We then investigate the generalization of action invariants into state …constraints. Blocks world examples illustrate the general procedure throughout. Show more

Keywords: knowledge representation, logics for artificial intelligence, reasoning about action

DOI: 10.3233/FI-1997-30108

Citation: Fundamenta Informaticae, vol. 30, no. 1, pp. 109-123, 1997