The search functionality is under construction.
The search functionality is under construction.

Keyword Search Result

[Keyword] POS(1110hit)

1101-1110hit(1110hit)

  • Inductive Inferability for Formal Languages from Positive Data

    Masako SATO  Kazutaka UMAYAHARA  

     
    PAPER

      Vol:
    E75-D No:4
      Page(s):
    415-419

    In this paper, we deal with inductive inference of an indexed family of recursive languages. We give two sufficient conditions for inductive inferability of an indexed family from positive data, each of which does not depend on the indexing of the family. We introduce two notions of finite cross property for a class of languages and a pair of finite tell-tales for a language. The former is a generalization of finite elasticity due to Wright and the latter consists of two finite sets of strings one of which is a finite tell-tale introduced by Angluin. The main theorem in this paper is that if any language of a class has a pair of finite tell-tales, then the class is inferable from positive data. Also, it is shown that any language of a class with finite cross property has a pair of finite tell-tales. Hence a class with finite cross property is inferable from positive data. Further-more, it is proved that a language has a finite tell-tale if and only if there does not exist any infinite cross sequence of languages contained in the language.

  • Subband Image Coding with Biorthogonal Wavelets

    Cha Keon CHEONG  Kiyoharu AIZAWA  Takahiro SAITO  Mitsutoshi HATORI  

     
    PAPER-Image Coding and Compression

      Vol:
    E75-A No:7
      Page(s):
    871-881

    In this paper, subband image coding with symmetric biorthogonal wavelet filters is studied. In order to implement the symmetric biorthogonal wavelet basis, we use the Laplacian Pyramid Model (LPM) and the trigonometric polynomial solution method. These symmetric biorthogonal wavelet basis are used to form filters in each subband. Also coefficients of the filter are optimized with respect to the coding efficiency. From this optimization, we show that the values of a in the LPM generating kernel have the best coding efficiency in the range of 0.7 to 0.75. We also present an optimal bit allocation method based on considerations of the reconstruction filter characteristics. The step size of each subband uniform quantizer is determined by using this bit allocation method. The coding efficiency of the symmetric biorthogonal wavelet filter is compared with those of other filters: QMF, SSKF and Orthonormal wavelet filter. Simulation results demonstrate that the symmetric biorthogonal wavelet filter is useful as a basic means for image analysis/synthesis filters and can give better coding efficiency than other filters.

  • Polynomial Time Inference of Unions of Two Tree Pattern Languages

    Hiroki ARIMURA  Takeshi SHINOHARA  Setsuko OTSUKI  

     
    PAPER

      Vol:
    E75-D No:4
      Page(s):
    426-434

    In this paper, we consider the polynomial time inferability from positive data for unions of two tree pattern languages. A tree pattern is a structured pattern known as a term in logic programming, and a tree pattern language is the set of all ground instances of a tree pattern. We present a polynomial time algorithm to find a minimal union of two tree pattern languages containing given examples. Our algorithm can be considered as a natural extension of Plotkin's least generalization algorithm, which finds a minimal single tree pattern language. By using this algorithm, we can realize a consistent and conservative polynomial time inference machine that identifies unions of two tree pattern languages from positive data in the limit.

  • 45Mbps Multi-Channel Composite TV Coding System

    Shuichi MATSUMOT  Takahiro HAMADA  Masahiro SAITO  Hitomi MURAKAMI  

     
    PAPER

      Vol:
    E75-B No:5
      Page(s):
    358-367

    In recent years, the digitalization of transmission links, such as optical fibre cables, satellite links, and terrestrial microwave links, has been progressed rapidly in many countries. In addition, many types of digital studio equipment have been developed and TV programs can be produced or edited without any picture quality degradation by using such equipment, for example, digital VTR. A high-efficiency bit-reduction coding system is the most promising and effective means for this situation in terms of reducing the cost of digital transmission of TV programs with high picture quality. Considering this background, a new digital coding system has been developed, which makes it possible to transmit up to 4 NTSC TV programs simultaneously over a single DS3 45Mbps link including two high quality sound channels and one 64kbps ancillary data channel for each TV program. The principal bit-reduction technique employed is 2 dimensional intraframe WHT (Walsh Hadamard Transform) coding, which gives higher coding performance for composite TV signals than DCT (Discrete Cosine Transform) coding. In order to attain high picture quality at around 8Mbps for 4 channel transmission, a 3 dimensional adaptive quantization cube which reflects human visual perception sufficiently is employed in the intraframe WHT coding scheme. The hardware has been made compact like a home use VTR. In this paper, first, the algorithm of the coding scheme developed for the coding system is presented, and then the system configuration and its basic coding performance are described.

  • Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--

    Toshimasa WATANABE  Naomoto KATO  Kenji ONAGA  

     
    PAPER

      Vol:
    E75-A No:4
      Page(s):
    478-491

    The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.

  • Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic --Provability and Axiom Sets --

    Toshimasa WATANABE  Naomoto KATO  Kenji ONAGA  

     
    PAPER

      Vol:
    E75-A No:3
      Page(s):
    425-435

    The subject of the paper is to analyze time complexity of the minimum axiom set problem (MASHC) in the Horn clause propositional logic. MASHC is defined by "Given a set H of Horn clauses and a query Q, all in propositional logic, such that Q is provable over H, find an axiom set of minimum cardinality, HH, with respect to Q, where Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens starting from clauses of H under the assumption that all of them are originally assumed to be true". If Q is provable over H then H is called an axiom set (with respect to Q). As stated in the definition of MASHC, detecting if Q is provable over H is required. This leads us to a problem, called the provability detecting problem (PDPHC), defined by "Given a set H of Horn clauses and a query Q in propositional logic, determine if Q is provable over H". First an O(σ) algorithm BFSHC for PDPHC is given based on the breadth-first search, where σ is the formula size of a given set of Horn clauses. For MASHC, it is shown that the problem is NP-complete, and an O(σ) approximation algorithm FMAS is given. Its experimental evaluation is also presented.

  • Deriving Compositional Models for Concurrency Based on de Bakker-Zucker Metric Domain from Structured Operational Semantics

    Eiichi HORITA  

     
    PAPER

      Vol:
    E75-A No:3
      Page(s):
    400-409

    This paper investigates the compositionality of operational models for concurrency induced by labeled transition systems (LTS's). These models are defined on the basis of a metric domain first introduced by de Bakker and Zucker; the domain is a complete metric space consisting of tree-like structures called processes. Transition system specifications (TSS's) define LTS's; the set of states of such a LTS A is the set of terms generated by a signature Σ. For the syntactical operators F contained in Σ, semantic operations (on processes) associated with F are derived from the TSS S by which A is defined, provided that S satisfies certain syntactical restrictions. By means of these operations, the compositionality of the operational model induced by A is established. A similar result was obtained by Rutten from TTS's which define finitely branching LTS's. The main contribution of this paper is generalization of Rutten's result to be applicable to TSS's which are based on applicative languages including recursion, parameterized statements, and value passing, and which define infinitely branching LTS's. A version of typed λ-calculus incorporating µ-notation is employed as a formalism for treating recursion, parameterized statements, and value-passing. Infinitely branching LTS's are needed to treat programming languages including value passing such as CCS.

  • Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications

    Naoshi UCHIHIRA  

     
    PAPER

      Vol:
    E75-A No:3
      Page(s):
    380-391

    A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.

  • Hierarchical Decomposition and Latency for Circuit Simulation by Direct Method

    Masakatsu NISHIGAKI  Nobuyuki TANAKA  Hideki ASAI  

     
    LETTER

      Vol:
    E75-A No:3
      Page(s):
    347-351

    For the efficient circuit simulation by the direct method, network tearing and latency techniques have been studied. This letter describes a circuit simulator SPLIT with hierarchical decomposition and latency. The block size of the latent subcircuit can be determined dynamically in SPLIT. We apply SPLIT to the MOS circuit simulation and verify its availability.

  • Fully Abstract Models for Communicating Processes with respect to Weak Linear Semantics with Divergence

    Eiichi HORITA  

     
    PAPER

      Vol:
    E75-D No:1
      Page(s):
    64-77

    The semantics of a language for communicating processes is investigated, and three full abstractness results for are established. The language contains atomic actions, termination, inaction, sequential composition, alternative composition, parallel composition, action restriction, and a form of guarded recursion. (The guardedness restriction on recursion is needed to establish one of the full abstractness results.) Three Plotkin-style operational semantics WL, CWL, and IWL of the language are defined. These semantics are linear in that the meaning of each program in any of these semantics is a set of action sequences the program may perform, and are weak in that the action sequences are obtained by ignoring (finte sequences of) internal moves. All the three semantics distinguish divergence (an infinite sequence of internal moves) from deadlock. The semantics IWL differs from the other two in that IWL is a so-called interal action semantics taking into account only internal moves under the assumption that the environment allows no (external) communication actions, and hence, the only possible actions for processes are internal moves, whereas the other two semantics take into account communication actions in addition to internal moves. The two semantics WL and CWL differ each other in that CWL is a so- called completed trace semantics, whereas WL is not. Then, two compositional models RF and IRF for the language are proposed, and the full a bstractness of RF (resp. of IRF) w. r. t. WL and CWL (resp. w. r. t. IWL), as expressed in the following, is established:s1s2(*) S[][S[]is a context of ⇒S[s1]S[s2]],where ,RF,WL, RF,CWL, IRF,IWL. A similar full abstractness result has been established by Bergstra, Klop, and Olderog for a language without recursion or internal moves. Moreover, Rutten investigated the semantics of a language similar to , in the framework of complete metric spaces, and showed that the failures model is fully abstract w. r. t. a strong linear semantics L, where L is strong in that it does not abstract from internal moves. The full abstractness of RF w. r. t. CWL, expressed in (*) with ,RF,CWL, is an extension of the result of Bergstra et al. to a language with recursion and internal moves. Also, the full abstractness of IRF w. r. t. IWL, expressed in (*) with ,IRF,IWL, is an extension of the Rutten's result, to the case of weak linear semantics with divergence.

1101-1110hit(1110hit)