A term rewriting system which effectively preserves recognizability (EPR-TRS) has good mathematical properties. In this paper, a new subclass of TRSs, layered transducing TRSs (LT-TRSs) is defined and its recognizability preserving property is discussed. The class of LT-TRSs contains some EPR-TRSs, e.g., {f(x)f(g(x))} which do not belong to any of the known decidable subclasses of EPR-TRSs. Bottom-up linear tree transducer, which is a well-known computation model in the tree language theory, is a special case of LT-TRS. We present a sufficient condition for an LT-TRS to be an EPR-TRS. Also reachability and joinability are shown to be decidable for LT-TRSs.

Detecting security flaws is important in order to keep the database secure. A security flaw in object-oriented databases means that a user can infer the result of an unpermitted method only from permitted methods. Although a database management system enforces access control by an authorization, security flaws can occur under the authorization. The main aim of this paper is to show an efficient decision algorithm for detecting a security flaw under a given authorization. This problem is solvable in polynomial time in practical cases by reducing it to the congruence closure problem. This paper also mentions the problem of finding a maximal subset of a given authorization under which no security flaw exists.

A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.

Trust negotiation is an authorizing technique based on digital credentials, in which both a user and a server gradually establish trust in each other by repeatedly exchanging their credentials. A trust negotiation strategy is a function that answers a set of credentials to disclose to the other party, depending on policies and the set of already disclosed credentials. The disclosure tree strategy (DTS), proposed by Yu et al., is one of the strategies that satisfies preferable properties. DTS in a simple implementation requires exponential time and space; however, neither an efficient algorithm nor the lower-bound of its complexity was known. In this paper, we investigate the computational complexity of DTS. We formulate subproblems of DTS as problems on derivation trees of a context-free grammar (CFG), and analyze the computational complexity of the subproblems using the concepts of CFGs. As a result, we show that two subproblems EVL and MSET of DTS are NP-complete and NP-hard, respectively, while both are solvable in polynomial time if we modify EVL not to require non-redundancy and MSET not to answer any subset useless for leading the negotiation to success.

This paper presents a method of translating natural language specifications of communication protocols into algebraic specifications. Such a natural language specification specifies action sequences performed by the protocol machine (program). Usually, a sentence implicitly specifies the state of the protocol machine at which the described actions must be performed. The authors propose a method of analyzing the implicitly specified states of the protocol machine taking the OSI session protocol specification (265 sentences) as an example. The method uses the following properties: (a) syntactic properties of a natural language (English in this paper); (b) syntactic properties introduced by the target algebraic specifications, e.g., type constraints; (c) properties specific to the target domain, e.g., properties of data types. This paper also shows the result of applying this method to the main part of the OSI session protocol specification (29 paragraphs, 98 sentences). For 95 sentences, the translation system uniquely determines the states specified implicitly by these sentences, using only (a) and (b) described above. By using (c) in addition, each implicitly specified state in the remaining three sentences is uniquely determined.

It is well-known that pushdown systems (PDS) effectively preserve regularity. This property implies the decidability of the reachability problem for PDS and has been applied to automatic program verification. The backward regularity preservation property was also shown for an extension of PDS by adding registers. This paper aims to show the forward regularity preservation property. First, we provide a concise definition of the register model called register pushdown systems (RPDS). Second, we show the forward regularity preservation property of RPDS by providing a saturation algorithm that constructs a register automaton (RA) recognizing $post^{ast}_calP(L(calA))$ where $calA$ and $calP$ are a given RA and an RPDS, respectively, and $post^{ast}_calP$ is the forward image of the mapping induced by $calP$. We also give an example of applying the proposed algorithm to malware detection.

Register context-free grammars (RCFG) is an extension of context-free grammars to handle data values in a restricted way. In RCFG, a certain number of data values in registers are associated with each nonterminal symbol and a production rule has the guard condition, which checks the equality between the content of a register and an input data value. This paper starts with RCFG and introduces register type, which is a finite representation of a relation among the contents of registers. By using register type, the paper provides a translation of RCFG to a normal form and ϵ-removal from a given RCFG. We then define a generalized RCFG (GRCFG) where an arbitrary binary relation can be specified in the guard condition. Since the membership and emptiness problems are shown to be undecidable in general, we extend register type for GRCFG and introduce two properties of GRCFG, simulation and progress, which guarantee the decidability of these problems. As a corollary, these problems are shown to be EXPTIME-complete for GRCFG with a total order over a dense set.

A program is non-interferent if it leaks no secret information to an observable output. However, non-interference is too strict in many practical cases and quantitative information flow (QIF) has been proposed and studied in depth. Originally, QIF is defined as the average of leakage amount of secret information over all executions of a program. However, a vulnerable program that has executions leaking the whole secret but has the small average leakage could be considered as secure. This counter-intuition raises a need for a new definition of information leakage of a particular run, i.e., dynamic leakage. As discussed in [5], entropy-based definitions do not work well for quantifying information leakage dynamically; Belief-based definition on the other hand is appropriate for deterministic programs, however, it is not appropriate for probabilistic ones.In this paper, we propose new simple notions of dynamic leakage based on entropy which are compatible with existing QIF definitions for deterministic programs, and yet reasonable for probabilistic programs in the sense of [5]. We also investigated the complexity of computing the proposed dynamic leakage for three classes of Boolean programs. We also implemented a tool for QIF calculation using model counting tools for Boolean formulae. Experimental results on popular benchmarks of QIF research show the flexibility of our framework. Finally, we discuss the improvement of performance and scalability of the proposed method as well as an extension to more general cases.

Parallel multiple context-free grammars (pmcfg's) and multiple context-free grammars (mcfg's) were introduced as extensions of context-free grammars to describe the syntax of natural languages. Pmcfg's and mcfg's deal with tuples of strings, and it has been shown that the universal recognition problem for mcfg's is EXP-POLY time-complete where the universal recognition problem is the problem to decide whether G generates w for a given grammar G and string w. In this paper, the universal recognition problems for the class of pmcfg's and for the subclass of pmcfg's with the information-lossless condition are shown to be EXP-POLY time-complete and PSPACE-complete, respectively. It is also shown that the problems for pmcfg's and for mcfg's with a bounded dimension are both -complete and those for pmcfg's and for mcfg's with a bounded degree are both -complete. As a corollary, the problem for modified head grammars introduced by Vijay-Shanker, et al. to define the syntax of natural languages is shown to be in deterministic polynomial time.

We consider the problem of deciding whether a query can be rewritten by a nondeterministic view. It is known that rewriting is decidable if views are given by single-valued non-copying devices such as compositions of single-valued extended linear top-down tree transducers with regular look-ahead, and queries are given by deterministic MSO tree transducers. In this paper, we extend the result to the case that views are given by nondeterministic devices that are not always single-valued. We define two variants of rewriting: universal preservation and existential preservation, and discuss the decidability of them.

Television white spaces (TVWS) are locally and/or temporally unused portions of TV bands. After TVWS regulations were passed in the USA, more and more regulators have been considering efficient use of TVWS. Under the condition that the primary user, i.e., terrestrial TV broadcasting system, is not interfered, various secondary users (SUs) may be deployed in TVWS. In Japan, the TVWS regulations started with broadcast-type SUs and small-area broadcasting systems, followed by voice radio. This paper aims to provide useful insights for more efficient utilization of TVWS as one of the options to meet the continuously increasing demand for wireless bandwidth. TVWS availability in Japan is analyzed using graphs and maps. As per the regulations in Japan, for TV broadcasting service, a protection contour is defined to be 51dBµV/m, while the interference contour for SU is defined to be 12.3dBµV/m. We estimate TVWS availability using these two regulation parameters and the minimum separation distances calculated on the basis of the ITU-R P.1546 propagation models. Moreover, we investigate and explain the effect of two important factors on TVWS availability. One is the measures to avoid adjacent channel interference, while the other is whether the SU has client devices with interference ranges beyond the interference area of the master device. Furthermore, possible options to increase available TVWS channels are discussed.

This paper discusses the decidability of node query preservation problems for tree transducers. We assume a transformation given by a deterministic linear top-down data tree transducer (abbreviated as DLTV) and an n-ary query based on runs of a tree automaton. We say that a DLTV Tr strongly preserves a query Q if there is a query Q' such that for every tree t, the answer set of Q' for Tr(t) is equal to the answer set of Q for t. We also say that Tr weakly preserves Q if there is a query Q' such that for every t, the answer set of Q' for Tr(t) includes the answer set of Q for t. We show that the weak preservation problem is coNP-complete and the strong preservation problem is in 2-EXPTIME. We also show that the problems are decidable when a given transducer is a functional extended linear top-down data tree transducer with regular look-ahead, which is a more expressive transducer than DLTV.

This paper discusses the decidability of determinacy and subsumption of tree transducers. For two tree transducers T1 and T2, T1 determines T2 if the output of T2 can be identified by the output of T1, that is, there is a partial function f such that [[T2]]=f∘[[T1]] where [[T1]] and [[T2]] are tree transformation relations induced by T1 and T2, respectively. Also, T1 subsumes T2 if T1 determines T2 and the partial function f such that [[T2]]=f∘[[T1]] can be defined by a transducer in a designated class that T2 belongs to. In this paper, we show that determinacy is in coNEXPTIME for single-valued linear extended bottom-up tree transducers as the determiner class and single-valued bottom-up tree transducers as the determinee class. We also show that subsumption is in coNEXPITME for these classes, and a bottom-up tree transducer T3 such that [[T2]]=[[T3]]∘[[T1]] can be constructed if T1 subsumes T2.

Several grammars of which generative power is between context-free grammar and context-sensitive grammar were proposed. Among them are macro grammar and tree adjoining grammar. Multiple context-free grammar is also a natural extension of context-free grammars, and is known to be stronger in its generative power than tree adjoining grammar and yet to be recognizable in polynomial time. In this paper, the generative power of several subclasses of variable-linear macro grammars and that of multiple context-free grammars are compared in details.

The deployment of small cells is one of the most effective means to cope with the traffic explosion of cellular mobile systems. However, a small cell system increases the inter-cell interference, which limits the capacity and degrades the cell-edge user throughput. Inter-cell interference coordination (ICIC), such as fractional frequency reuse (FFR), is a well-known scheme that autonomously mitigates inter-cell interference. In the Long Term Evolution (LTE)-Advanced, the three-dimensional (3D) beamforming, which combines conventional horizontal beamforming and vertical beamforming, has been gaining increasing attention. This paper proposes a novel centralized ICIC scheme that controls the direction of narrow 3D beam for each frequency band of each base station. The centralized controller collects information from the base stations and calculates sub-optimum combinations of narrow beams so as to maximize the proportional fair (PF) utility of all users. This paper describes the throughput of the new centralized ICIC scheme as evaluated by computer simulations and shows it has a significant gain in both average user throughput and cell-edge user throughput compared with the conventional ICIC scheme. This paper also investigates the feasibility of the scheme by assessing its throughput performance in a realistic deployment scenario.

Many practical communication protocols provide priority service as well as ordinary service. In such a protocol, the protocol machines can initiate a priority service at most of the states. This characteristic leads an extreme increment of the number of state transitions on the protocol machines and causes state space explosion in verification of safety property of the protocol. This paper describes a method of constructing a communication protocol from composition of a subprotocol for ordinary service and that for priority service. This paper also presents a sufficient condition for a composed protocol to inherit safety property from the subprotocols. By using the composition method and the sufficient condition, the decision problem for safety property of the composed protocol can be reduced to those of the subprotocols. An experimental result of verification of a part of OSI session protocol is also described. The result shows that the method can reduce the computation time for verifying safety property to about 3% against the naive way.

Several grammars have been proposed for representing RNA secondary structure including pseudoknots such as simple linear tree adjoining grammar (sl-tag), extended sl-tag (esl-tag) and RNA pseudoknot grammar (rpg). The main purpose of this paper is to compare the generative power of these grammars by identifying them as subclasses of multiple context-free grammars (mcfg). Specifically, it is shown that the class of languages generated by esl-tag (ESL-TAL) properly includes the class of languages generated by sl-tag (SL-TAL) and the class of languages generated by cfg. Also, we show that the class of languages generated by rpg coincides with the class of languages generated by mcfg with dimension one or two and rank one or two. Furthermore, it is shown that SL-TAL is a full trio and ESL-TAL is a substitution closed full AFL.

One of the most promising compression methods for XML documents is the one that translates a given document to a tree grammar that generates it. A feature of this compression is that the internal structures are kept in production rules of the grammar. This enables us to directly manipulate the tree structure without decompression. However, previous studies assume that a given XML document does not have data values because they focus on direct retrieval and manipulation of the tree structure. This paper proposes a direct update method for XML documents with data values and shows the effectiveness of the proposed method based on experiments conducted on our implemented tool.

Formal series are a natural extension of formal languages by associating each word with a value called a coefficient or a weight. Among them, recognizable series and algebraic series can be regarded as extensions of regular languages and context-free languages, respectively. The coefficient of a word w can represent quantities such as the cost taken by an operation on w, the probability that w is emitted. One of the possible applications of formal series is the string counting in quantitative analysis of software. In this paper, we define the counting problems for formal series and propose algorithms for the problems. The membership problem for an automaton or a grammar corresponds to the problem of computing the coefficient of a given word in a given series. Accordingly, we define the counting problem for formal series in the following two ways. For a formal series S and a natural number d, we define CC(S,d) to be the sum of the coefficients of all the words of length d in S and SC(S,d) to be the number of words of length d that have non-zero coefficients in S. We show that for a given recognizable series S and a natural number d, CC(S,d) can be computed in O(η log d) time where η is an upper-bound of time needed for a single state-transition matrix operation, and if the state-transition matrices of S are commutative for multiplication, SC(S,d) can be computed in polynomial time of d. We extend the notions to tree series and discuss how to compute them efficiently. Also, we propose an algorithm that computes CC(S,d) in square time of d for an algebraic series S. We show the CPU time of the proposed algorithm for computing CC(S,d) for some context-free grammars as S, one of which represents the syntax of C language. To examine the applicability of the proposed algorithms to string counting for the vulnerability analysis, we also present results on string counting for Kaluza Benchmark.