From regular expressions to smaller NFAs

Several methods have been developed to construct λ-free automata that represent a regular expression. Among the most widely known are the position automaton (Glushkov), the partial derivatives automaton (Antimirov) and the follow automaton (Ilie and Yu). All these automata can be obtained with quadratic time complexity, thus, the comparison criterion is usually the size of the resulting automaton. The methods that obtain the smallest automata (although, for general expressions, they are not comparable), are the follow and the partial derivatives methods. In this paper, we propose another method to obtain a λ-free automaton from a regular expression. The number of states of the automata we obtain is bounded above by the size of both the partial derivatives automaton and of the follow automaton. Our algorithm also runs with the same time complexity of these methods.     

模糊树自动机语言的封闭性

给出了[Σ-]代数、[Σ-]树、模糊[Σ-]树自动机、模糊[Σ-]树自动机行为的定义。引入了模糊树自动机语言的并、交、连接和Kleene闭包运算,证明了在这些运算下模糊树自动机语言的封闭性。     

A note on partially ordered tree automata

A recent paper by Bouajjani, Muscholl and Touili shows that the class of languages accepted by partially ordered word automata (or equivalently accepted by Σ₂-formulae) is closed under semi-commutation and it suggested the following open question: can we extend this result to tree languages? This problem can be addressed by proving (1) that the class of tree regular languages accepted by Σ₂ formulae is strictly included in the class of languages accepted by partially ordered automata, and (2) that Bouajjani and the others results cannot be extended to tree.     

A general approach for building combinational P automata

In traditional automata theory, the closure with respect to certain operations is one of the most investigated properties, especially the methods of constructing automata for certain operations among the given sub-automata. However, up to now less effort has been addressed to this question for P automata. As an improvement on earlier results, we introduce P automata with communication and active membrane rules working in the initial mode (CAIP). We present methods for constructing automata that recognize the Union, the Concatenation, the Kleene Closure, or the ω Closure of the given languages which are represented by some P automata. We also show that for any language denoted by a regular expression, we can readily construct a CAIP automaton corresponding to it.     

From Syntactic Theories to Interpreters: Automating the Proof of Unique Decomposition

Developing syntactic theories for reasoning about programming languages usually involves proving a unique-decomposition lemma. The proof of such a lemma is tedious, error-prone, and is usually attempted many times during the design of a theory. We therefore investigate the automation of such proofs.We map the unique-decomposition lemma to the problems of checking equivalence and ambiguity of syntactic definitions. Because checking these properties of context-free grammars is undecidable, we work with regular tree grammars and use algorithms on finite tree automata to perform the checking. To make up for the insufficient expressiveness of regular tree grammars, we extend the basic framework with built-in types and constants, contexts, and polymorphic types.Our implementation extends an earlier system by Xiao et al. [16] that translates semantic specifications expressed as syntactic theories to interpreters. We have successfully used the combined system to generate interpreters and verify the unique-decomposition lemma for a number of examples.     

Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

Duration-constrained regular expressions

This paper investigates the logic-automata-connection for Duration Calculus. It has been frequently observed that Duration Calculus with linear duration terms comes close to being a logic of linear hybrid automata. We attempt to make this relation precise by constructing Kleene-connection between duration-constrained regular expressions and a subclass of linear hybrid automata called loop-reset automata in which any variable tested in a loop is reset in the same loop. The formalism of duration-constrained regular expressions is an extension of regular expressions with duration constraints, which are essentially formulas of Duration Calculus without negation, yet extended by a Kleene-star operator. In this paper, we show that this formalism is equivalent in expressive power to loop-reset automata by providing a translation procedure from expressions to automata and vice verse.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones     

Canonical forms for labelled trees and their applications in frequent subtree mining

Tree structures are used extensively in domains such as computational biology, pattern recognition, XML databases, computer networks, and so on. In this paper, we first present two canonical forms for labelled rooted unordered trees–the breadth-first canonical form (BFCF) and the depth-first canonical form (DFCF). Then the canonical forms are applied to the frequent subtree mining problem. Based on the BFCF, we develop a vertical mining algorithm, RootedTreeMiner, to discover all frequently occurring subtrees in a database of labelled rooted unordered trees. The RootedTreeMiner algorithm uses an enumeration tree to enumerate all (frequent) labelled rooted unordered subtrees. Next, we extend the definition of the DFCF to labelled free trees and present an Apriori-like algorithm, FreeTreeMiner, to discover all frequently occurring subtrees in a database of labelled free trees. Finally, we study the performance and the scalability of our algorithms through extensive experiments based on both synthetic data and datasets from real applications.     

Constants and label-equivalence: A decision procedure for reflexive regular splicing languages

A structural characterization of reflexive splicing languages has been recently given in [P. Bonizzoni, C. De Felice, R. Zizza, The structure of reflexive regular splicing languages via Schützenberger constants, Theoretical Computer Science 334 (2005) 71-98] and [P. Bonizzoni, G. Mauri, Regular splicing languages and subclasses, Theoretical Computer Science 340 (2005) 349-363] showing surprising connections between long standing notions in formal language theory, the syntactic monoid and Schützenberger constant and the splicing operation.In this paper, we provide a procedure to decide whether a regular language is a reflexive splicing language, based on the above-mentioned characterization that is given in terms of a finite set of constants for the language. The procedure relies on the notion of label-equivalence that induces a finite refinement of the syntactic monoid of a regular language L. A finite set of representatives for label-equivalent classes of constant words in L is defined and it is proved that such a finite set provides the splice sites of splicing rules generating language L.     

Syntactic recognition of ECG signals by attributed finite automata

A syntactic pattern recognition method of electrocardiograms (ECG) is described in which attributed automata are used to execute the analysis of ECG signals. An ECG signal is first encoded into a string of primitives and then attributed automata are used to analyse the string. We have found that we can perform fast and reliable analysis of ECG signals by attributed automata.     

Expressiveness of propositional projection temporal logic with star

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.     

Excessively duplicating patterns represent non-regular languages

A constrained term pattern s:φ$s:\phi$ represents the language of all instances of the term s satisfying the constraint φ. For each variable in s, this constraint specifies the language of its allowed substitutions. Regularity of languages represented by sets of patterns has been studied for a long time. This problem is known to be co-NP-complete when the constraints allow each variable to be replaced by any term over a fixed signature, and EXPTIME-complete when the constraints restrict each variable to a regular set. In both cases, duplication of variables in the terms of the patterns is a necessary condition for non-regularity. This is because duplications force the recognizer to test equality between subterms. Hence, for the specific classes of constraints mentioned above, if all patterns are linear, then the represented language is necessarily regular. In this paper we focus on the opposite case, that is when there are patterns with “excessively duplicating” variables. We prove that when each pattern of a non-empty set has a duplicated variable constrained to an infinite language, then the language represented by the set is necessarily non-regular. We prove this result independently of the kind of constraints used, just assuming that they are mappings from variables to arbitrary languages. Our result provides an efficient procedure for detecting, in some cases, non-regularity of images of regular languages under tree homomorphisms.     

Parameterized complexity of basic decision problems for tree automata

There are many decision problems in automata theory (including membership, emptiness, inclusion and universality problems) that are NP-hard for some classes of tree automata (TA). The study of their parameterized complexity allows us to find new bounds of their nonpolynomial time algorithmic behaviours. We present results of such a study for classical TA, rigid tree automata, TA with global equality and disequality and t-DAG automata. As parameters we consider the number of states, the cardinality of the signature, the size of the term or the t-dag and the size of the automaton.     

格值交替树自动机

交替（树）自动机因其本身关于取补运算的简洁性及其与非确定型（树）自动机的等价性,成为自动机与模型检测领域研究的一个新方向.在格值交替自动机与经典交替树自动机概念的基础上,引入格值交替树自动机的概念,并研究了格值交替树自动机的代数封闭性和表达能力.首先,证明了对格值交替树自动机的转移函数取对偶运算,终止权重取补之后所得自动机与原自动机接受语言互补这一结论.其次,证明了格值交替树自动机关于交、并运算的封闭性.最后,讨论了格值交替树自动机和格值树自动机、格值非确定型自动机的表达能力;证明了格值交替树自动机与格值树自动机的等价性,并给出了二者相互转化的算法及其复杂度分析;同时,提供了用格值非确定型自动机来模拟格值交替树自动机的方法.     

正规文法与有限自动机的等价构造

在功能上,正规文法与有限自动机描述和识别语言是等价的,它们之间也存在等价构造算法,但这些构造算法有些复杂.对其算法进行了简化且给以了证明,并提出了一个从有限自动机构造等价左线性正规文法的算法,同时也进行了证明,最后给出了该算法的一个实例.     

Tree pattern mining with tree automata constraints

Most work on pattern mining focuses on simple data structures such as itemsets and sequences of itemsets. However, a lot of recent applications dealing with complex data like chemical compounds, protein structures, XML and Web log databases and social networks, require much more sophisticated data structures such as trees and graphs. In these contexts, interesting patterns involve not only frequent object values (labels) appearing in the graphs (or trees) but also frequent specific topologies found in these structures. Recently, several techniques for tree and graph mining have been proposed in the literature. In this paper, we focus on constraint-based tree pattern mining. We propose to use tree automata as a mechanism to specify user constraints over tree patterns. We present the algorithm CoBMiner which allows user constraints specified by a tree automata to be incorporated in the mining process. An extensive set of experiments executed over synthetic and real data (XML documents and Web usage logs) allows us to conclude that incorporating constraints during the mining process is far more effective than filtering the interesting patterns after the mining process.     

On stateless multihead automata: Hierarchies and the emptiness problem

We look at stateless multihead finite automata in their two-way and one-way, deterministic and nondeterministic variations. The transition of a k-head automaton depends solely on the symbols currently scanned by its k heads, and every such transition moves each head one cell left or right, or instructs it to stay. We show that stateless (k+4)-head two-way automata are more powerful than stateless k-head two-way automata. In the one-way case, we prove a tighter result: stateless (k+1)-head one-way automata are more powerful than stateless k-head one-way automata. Finally, we show that the emptiness problem for stateless 2-head two-way automata is undecidable.     

采用树自动机推理技术的信息抽取方法

提出了一种利用改进的k-contextual树自动机推理算法的信息抽取技术。其核心思想是将结构化（半结构化）文档转换成树,然后利用一种改进的k-contextual树（KLH树）来构造出能够接受样本的无秩树自动机,依据该自动机接收和拒绝状态来确定是否抽取网页信息。该方法充分利用了网页文档的树状结构,依托树自动机将传统的以单一结构途径的信息抽取方法与文法推理原则相结合,得到信息抽取规则。实验证明,该方法与同类抽取方法相比,样本学习时间以及抽取所需时间上均有所缩短。     

Abstract regular (tree) model checking

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification of simple systems with various sources of infinity such as unbounded counters, queues, stacks, and parameters. We then show how abstract regular tree model checking can be used for verification of programs manipulating tree-like dynamic data structures. Even more complex data structures can be handled using a suitable tree-like encoding.     

Regular Tree Languages as an Abstract Domain in Program Specialisation

On-line partial evaluation algorithms include a generalisation step, which is needed to ensure termination. In partial evaluation of logic and functional programs, the usual generalisation operation is the most specific generalisation (msg) of expressions. This can cause loss of information, which is especially serious in programs whose computations first build some internal data structure that is then used to control a subsequent phase of execution—a common pattern of computation. If the size of the intermediate data is unbounded at partial evaluation time then the msg will lose almost all information about its structure. Hence subsequent phases of computation cannot be effectively specialised.In this paper the problem is tackled by introducing regular tree languages into a partial evaluation algorithm. A regular tree language is a set of terms defined by tree automata or tree grammars. In the algorithm, regular tree approximations of sets of terms encountered during partial evaluation are constructed. The critical point is that when generalisation is performed, the upper bound on regular tree languages can be combined with the msg, thus preserving recursive information about term structure. This approach also allows the specialisation of programs with respect to goals whose arguments range over regular tree languages.The algorithm is presented as an instance of Leuschel's framework for abstract specialisation of logic programs. This provides a generic algorithm parameterised by an abstract domain—regular trees in this case. The correctness requirements from his framework are established. The extension of the algorithm to propagate regular approximations of answers as well as calls is also presented, increasing the amount of specialisation that can be obtained. Finally a technique for increasing precision based on wrapper functions is introduced.