Fundamenta Informaticae - Volume 42, issue 3-4

Authors: Demri, Stéphane

Article Type: Research Article

Abstract: The nondeterministic information logic NIL has been introduced by Orłowska and Pawlak in 1984 as a logic for reasoning about total information systems with the similarity, the forward inclusion and the backward inclusion relations. In 1987, Vakarelov provides the first first-order characterization of structures derived from information systems and this has been done with the semantical structures of NIL. Since then, various extensions of NIL have been introduced and many issues for information logics about decidability and Hilbert-style proof systems have been solved. However, computational complexity issues have been seldom attacked in the literature mainly because the information logics are …propositional polymodal logics with interdependent modal connectives. We show that NIL satisfiability is a PSPACE-complete problem. PSPACE-hardness is shown to be an easy consequence of PSPACE-hardness of the well-known modal logic S4. The main difficulty is to show that NIL satisfiability is in PSPACE. To do so we present an original construction that extends various previous works by Ladner (1977), Halpern and Moses (1992) and Spaan (1993). Show more

Keywords: information system, multimodal logic, computational complexity, Ladner-like algorithm

DOI: 10.3233/FI-2000-423401

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 211-234, 2000

Authors: Denejko, Piotr | Diks, Krzysztof | Pelc, Andrzej | Piotrów, Marek

Article Type: Research Article

Abstract: We consider the problem of constructing reliable comparator networks built from unreliable comparators. In case of a faulty comparator inputs are directly output without comparison. A trivial lower bound of Ω(logn + k) on the depth of n-input k-fault tolerant sorting network is well known. We are interested in establishing exact lower bounds on the depth of such networks. To this end we consider fairly simple minimum-finding networks. Our main result is the first nontrivial lower bound on depths of networks computing minimum among n > 2 items in the presence of k > 0 faulty comparators. We prove that …the depth of any such network is at least max([logn] + 2k, logn + klog logn/k+1). We also describe a network whose depth nearly matches the lower bound. Show more

Keywords: comparator networks, fault-tolerant networks, minimum-finding networks

DOI: 10.3233/FI-2000-423402

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 235-249, 2000

Authors: Engel, Marcin | Kret, Artur | Mincer-Daszkiewicz, Janina

Article Type: Research Article

Abstract: The Trace Assertion Method (TAM) pioneered by Parnas is a formalism used to specify software module interfaces. The main purpose of the research described in this paper is to recognize the possibilities of linking the TAM editor with one of the existing theorem proving systems and to enable thereby the automated consistency checking of trace specifications. Possible approaches to embedding TAM in the Prototype Verification System (PVS) specification language are discussed and the chosen shallow definitional embedding is described in detail. Proof obligations for the consistency checking of trace specifications are obtained as type correctness conditions generated automatically by the …PVS type checker. Some of these obligations can be proven automatically by PVS, other proofs need human guidance. Possible ways of increasing automation capabilities of the PVS theorem prover are recognized and presented. We share our experience in defining both specialized and general purpose proof strategies. This research may be viewed as a case study in applying the existing general purpose proof system to consistency checking of some application-specific formalism, which might be of interest for the software designer community. Show more

Keywords: Software engineering, Formal methods, Automated theorem proving, Shallow and deep embedding, Axiomatic and definitional embedding, Trace Assertion Method, PVS

DOI: 10.3233/FI-2000-423403

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 251-278, 2000

Authors: Inuiguchi, Masahiro | Tanino, Tetsuzo

Article Type: Research Article

Abstract: A necessity measure N is defined by an implication function. However, specification of an implication function is difficult. Necessity measures are closely related to inclusion relations. In this paper, we propose an approach to necessity measure specification by giving a parametric inclusion relation between fuzzy sets A and B which is equivalent to NA (B) ≥ h. It is shown that, in such a way, we can specify a necessity measure, i.e., an implication function. Moreover, when a necessity measure or equivalently, an implication function is given, then the derivation of an associated parametric inclusion relation is discussed. The associated …parametric inclusion relation cannot be obtained for any implication function but only for implication functions which satisfy certain conditions. Applying our results to necessity measures defined by S-, R- and reciprocal R-implications with continuous Archimedean t-norms, associated parametric inclusion relations are shown. Show more

Keywords: necessity measure, implication function, conjunction function, t-norm, modifier, level cut condition

DOI: 10.3233/FI-2000-423404

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 279-302, 2000

Authors: Kaminski, Michael | Rey, Guy

Article Type: Research Article

Abstract: In this paper we introduce first-order non-monotonic modal logic and study its properties. Our definition is semantical and is based on the intuition similar to that lying behind the definition of first-order default logic. Thus, our definition of first-order non-monotonic modal logic well complies with that of first-order default logic and circumscription, providing a substantial evidence for its acceptance. In addition, our definition implies all properties of propositional non-monotonic modal logic, which supplies an additional support for its adequacy.

DOI: 10.3233/FI-2000-423405

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 303-333, 2000

Authors: Kohn, Markus | Schmeck, Hartmut

Article Type: Research Article

Abstract: In this paper a formal model for asynchronous systems behaviour is presented which is suited for representing all levels of abstraction appearing in the design process. Based on a structural abstraction of asynchronous computation systems called asynchronous nets the behaviour of an asynchronous system can be represented by a set of so called abstract computations. It is shown how basic properties of such systems, and in particular, delay-insensitive behaviour, could be determined by investigating properties of abstract computations. Finally, it is demonstrated that the model enables formal verification of asynchronous systems over different levels of abstraction.

Keywords: Asynchronous Systems, Asynchronous Computations, Formal Methods in Systems Modelling, Abstract Computations, Formal Verification

DOI: 10.3233/FI-2000-423406

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 335-389, 2000

Authors: Schlechta, Karl | Gourmelen, Laurent | Motré, Stéphanie | Rolland, Olivier | Tahar, Bensalah

Article Type: Research Article

Abstract: This paper deals with some fundamental concepts and questions of preferential structures. Traditionally, a model for preferential reasoning is a strict partial order on the set of classical models of the language; in this article it will be a total order on the classical models. Instead of representing non-monotonic inference relations by individual partial orders, we represent them by sets of total orders. We thus stay close to the way completeness proofs are done in classical logic. Our new approach will also justify multiple copies (or labelling functions) present in most work on preferential structures. A representation result for the …finite case is proven; for the infinite case it remains an open question. Show more

DOI: 10.3233/FI-2000-423407

Citation: Fundamenta Informaticae, vol. 42, no. 3-4, pp. 391-410, 2000