Regular Path Expressions in Feature Logic

We examine the existential fragment of a feature logic, which is extended by regular path expressions. A regular path expression is a subterm relation, where the allowed paths for the subterms are restricted to any given regular language. In the area of computational linguistics, this notion has been introduced as "functional uncertainty". We will prove that satisfiability is decidable by constructing a quasi-terminating rule system.     

随机正则(k,r)-SAT问题的可满足临界

研究k-SAT问题实例中每个变元恰好出现r=2s次,且每个变元对应的正、负文字都出现s次的严格随机正则（k,r）-SAT问题.通过构造一个特殊的独立随机实验,结合一阶矩方法,给出了严格随机正则（k,r）-SAT问题可满足临界值的上界.由于严格正则情形与正则情形的可满足临界值近似相等,因此得到了随机正则（k,r）-SAT问题可满足临界值的新上界.该上界不仅小于当前已有的随机正则（k,r）-SAT问题的可满足临界值上界,而且还小于一般的随机k-SAT问题的可满足临界值.因此,这也从理论上解释了在相变点处的随机正则（k,r）-SAT问题实例通常比在相应相变点处同规模的随机k-SAT问题实例更难满足的原因.最后,数值分析结果验证了所给上界的正确性.     

On the complexity of the two-variable guarded fragment with transitive guards

We investigate the complexity of the satisfiability problem for the two-variable guarded fragment with transitive guards. We prove that the satisfiability problem for the monadic version of this logic without equality is 2EXPTIME-hard. It is in fact 2EXPTIME-complete, since as shown by Szwast and Tendera, the whole guarded fragment with transitive guards is in 2EXPTIME. We also introduce a new logic—the guarded fragment with one-way transitive guards and prove that the satisfiability problem for the two-variable version of this logic is EXPSPACE-complete. The two-variable guarded fragment with transitive guards can be seen as a counterpart of some branching temporal logics with both future and past operators, while the two-variable guarded fragment with one-way transitive guards corresponds to some branching temporal logics without past operators. Therefore, our results reveal the difference in the complexity of the reasoning about the future only and both the future and the past, in the two-variable guarded fragment with transitive guards.     

Deciding Regular Grammar Logics with Converse Through First-Order Logic

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF², which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF² include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF² without extra machinery such as fixed-point operators.     

SLS算法求解平衡正则(k,2r)-CNF公式

可满足性问题的求解算法和结构性质研究是计算机科学中重要问题之一，为寻求某些CNF公式子类问题有效算法或算法改进途径，对公式的结构加以某些限制，其中限定子句长度为恒定常数和变元出现次数是常见的处理方式。研究具有正则结构且每个变元正负出现均衡的结构化公式的可满足性问题求解，其随机生成模型的构建及随机实验测试有助于观察解分布状况。并且，随机局部搜索算法在求解具有一定规则结构CNF公式实例中具有良好效率。本文集中研究平衡正则(k, 2r)-CNF公式的求解问题，即限制每个子句的长度为k，每个变元出现的次数为偶数2r,并且每个变元正负出现的次数在相等情况下的可满足性问题求解。给出BR(n,  k, 2r)模型，以此模型来生成具有特殊结构的平衡正则(k, 2r)-CNF公式实例，利用随机局部搜索算法求解问题。通过限制初始指派的0文字和1文字各占一半且均匀生成，以WalkSAT算法和NSAT算法做实验对比，发现对于平衡正则(k, 2r)-CNF公式，实例具有明显效率。     

The satisfiability problem in regular CNF-formulas

 In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a Davis–Putnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers.     

One-Unambiguous Regular Languages

The ISO standard for the Standard Generalized Markup Language (SGML) provides a syntactic meta-language for the definition of textual markup systems. In the standard, the right-hand sides of productions are based on regular expressions, although only regular expressions that denote words unambiguously, in the sense of the ISO standard, are allowed. In general, a word that is denoted by a regular expression is witnessed by a sequence of occurrences of symbols in the regular expression that match the word. In an unambiguous regular expression as defined by Booket al.(1971,IEEE Trans. Comput.C-20(2), 149–153), each word has at most one witness. But the SGML standard also requires that a witness be computed incrementally from the word with a one-symbol lookahead; we call such regular expressions 1-unambiguous. A regular language is a 1-unambiguouslanguage if it is denoted by some 1-unambiguous regular expression. We give a Kleene theorem for 1-unambiguous languages and characterize 1-unambiguous regular languages in terms of structural properties of the minimal deterministic automata that recognize them. As a result we are able to prove the decidability of whether a given regular expression denotes a 1-unambiguous language; if it does, then we can construct an equivalent 1-unambiguous regular expression in worst-case optimal time.     

Regular patterns, regular languages and context-free languages

In this paper we consider two questions. First we consider whether every pattern language which is regular can be generated by a regular pattern. We show that this is indeed the case for extended (erasing) pattern languages if alphabet size is at least four. In all other cases, we show that there are patterns generating a regular language which cannot be generated by a regular pattern. Next we consider whether there are pattern languages which are context-free but not regular. We show that, for alphabet size 2 and 3, there are both erasing and non-erasing pattern languages which are context-free but not regular. On the other hand, for alphabet size at least 4, every erasing pattern language which is context-free is also regular. It is open at present whether there exist non-erasing pattern languages which are context-free but not regular for alphabet size at least 4.     

Regular Model Checking using Widening Techniques

In this paper, we consider symbolic model checking of safety properties of linear parametrized systems. Sets of configurations are represented by regular languages and actions by regular relations. Since the verification problem amounts to the computation of the reachability set, we focus on the computation of R^*(φ) for a regular relation R and a regular language φ. We present a technique called regular widening that allows, when it terminates, the computation of either the reachability set R^*(φ) of a system or the transitive closure R^* of a regular relation. We show that our method can be uniformly applied to several parametrized systems. Furthermore, we show that it is powerful enough to simulate some existing methods that compute either R^* or R^*(φ) for each R (resp. φ) belonging to a subclass of regular relations (resp. belonging to a subclass of regular languages).     

一类布尔方程组的可满足性阈值研究*

以一类布尔方程组形式的NP问题可满足性阈值估计为研究目的,通过将高斯消去算法与摘叶算法相结合的方法给出了一种求解该问题的完全算法,并通过不同参数条件下对大量随机实例进行数值实验得到了原问题可满足性阈值的算法估计值。所得研究结果不仅首次给出了该问题的可满足性阈值估计,而且可以作为相关启发式完全算法的设计依据。     

A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case

2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper we extend 2LS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We call the resulting language 2LSmf. We prove that 2LSmf is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of 2LS. Furthermore, we prove that the language 2LSmf is stably infinite with respect to the sort of elements. Therefore, by using a many-sorted version of the Nelson–Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.     

Odometers on Regular Languages

Odometers or "adding machines" are usually introduced in the context of positional numeration systems built on a strictly increasing sequence of integers. We generalize this notion to systems defined on an arbitrary infinite regular language. In this latter situation, if (A,<) is a totally ordered alphabet, then enumerating the words of a regular language L over A with respect to the induced genealogical ordering gives a one-to-one correspondence between ℕ and L. In this general setting the odometer is not defined on a set of sequences of digits but on a set of pairs of sequences where the first (resp. the second) component of the pair is an infinite word over A (resp. an infinite sequence of states of the minimal automaton of L). We study some properties of the odometer such as continuity, injectivity, surjectivity, minimality, .... We then study some particular cases: we show the equivalence of this new function with the classical odometer built upon a sequence of integers whenever the set of greedy representations of all the integers is a regular language; we also consider substitution numeration systems as well as the connection with β-numerations.     

A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions

MLSS is a decidable sublanguage of set theory involving the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton.In this paper we extend MLSS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We prove that the resulting language is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of MLSS.     

Non-structural subtype entailment in automata theory

Decidability of non-structural subtype entailment is a long-standing open problem in programming language theory. In this paper, we apply automata theoretic methods to characterize the problem equivalently by using regular expressions and word equations. This characterization induces new results on non-structural subtype entailment, constitutes a promising starting point for further investigations on decidability, and explains for the first time why the problem is so difficult. The difficulty is caused by implicit word equations that we make explicit.     

基于Verilog 的正则表达式编译器的实现

随着网络带宽的快速增长,正则表达式匹配逐渐成为网络数据处理系统的性能瓶颈。为了获得更高的匹配效率,基于FPGA的正则表达式匹配引擎成为近年来的研究热点之一,而将正则表达式高效的转换成硬件描述语言是其中的关键技术。首先分析了正则表达式转换为硬件电路的算法,然后在此算法基础上实现了一个编译器。最后在Modelsim平台上进行了仿真,仿真结果证明了编译器的正确性。     

Regular Languages of Thin Trees

An infinite tree is called thin if it contains only countably many infinite branches. Thin trees can be seen as intermediate structures between infinite words and infinite trees. In this work we investigate properties of regular languages of thin trees. Our main tool is an algebra suitable for thin trees. Using this framework we characterize various classes of regular languages: commutative, open in the standard topology, and definable in weak MSO logic among all trees. We also show that in various meanings thin trees are not as rich as all infinite trees. In particular we observe a collapse of the parity index to the level (1, 3) and a collapse of the topological complexity to co-analytic sets. Moreover, a gap property is shown: a regular language of thin trees is either weak MSO-definable among all trees or co-analytic-complete.     

Regular solutions of linear differential systems with power series coefficients

The following problem is considered: given a system of linear ordinary differential equations of arbitrary order with power series coefficients, to recognize whether it has regular solutions at point 0 and, if it does, to find them. An algorithm for solving this problem is proposed. Each power series that is a coefficient of the original system is specified by a procedure that computes the series coefficient by the index of this coefficient. The original system is assumed to have full rank; i.e., the equations of the system are independent. The algorithm is implemented in Maple.     

Test Sets for the Universal and Existential Closure of Regular Tree Languages

Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.     

正则模型类的时态可定义性

正则模型是非正规模态逻辑的模型,通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算,可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭,并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力。