Compiling CSPs into Tree-Driven Automata for Interactive Solving

Constraint programming techniques are widely used to model and solve decision problems and many algorithms have been developed to solve automatically and efficiently families of CSPs; nevertheless, they do not help solve interactive decision support problems, like product configuration. In such problems, the user chooses the values of the variables, and the role of the system is not to solve the CSP, but to help the user in this task. Dynamic global consistency maintaining is one of the most useful functionalities that should be offered by such a CSP platform. Unfortunately, this task is intractable in the worst case. Since interactivity requires short response times, intractability must be circumvented some way. To this end, compilation methods have been proposed that transform the original problem into a data structure allowing a short response time. In this paper, we extend the work of Amilhastre et al. [1] and Vempaty [15] by the use of a new structure, tree-driven automata, that takes advantage of the structural characteristics of configuration problems (decomposition of the components into independent subcomponents). Tree-driven automata can be far more compact than classical automata while keeping their good properties, especially a tractable complexity for the maintenance of global consistency.     

Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties

The research examines liveness and progress properties of concurrent systems and their on-the-fly verification. An alternative formalism to Büchi automata, called testing automata, is developed. The basic idea of testing automata is to observe changes in the values of state propositions instead of the values. Therefore, the testing automata are able to accept only stuttering-insensitive languages. Testing automata can accept the same stuttering-insensitive languages as (state-labelled) Büchi automata, and they have at most the same number of states. They are also more often deterministic. Moreover, on-the-fly verification using testing automata can often (but not always) use an algorithm performing only one search in the state space, whereas on-the-fly verification with Büchi automata requires two searches. Experimental results illustrating the benefits of testing automata are presented.     

PVS Strategies for Proving Abstraction Properties of Automata

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the “natural” proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.     

Dynamical Properties of Timed Automata

Timed automata are an important model for specifying and analyzing real-time systems. The main analysis performed on timed automata is the reachability analysis. In this paper we show that the standard approach for performing reachability analysis is not correct when the clocks drift even by a very small amount. Our formulation of the reachability problem for timed automata is as follows: we define the set R ^*(T,Z ₀)=_>0 Reach(T, Z ₀ where T is obtained from timed automaton T by allowing an drift in the clocks. R ^*(T,Z ₀) is the set of states which can be reached in the timed automatonT from the initial states in Z₀ when the clocks drift by an infinitesimally small amount. We present an algorithm for computing R ^*(T,Z ₀)and provide a proof of its correctness. We show that R ^*(T,Z ₀)is robust with respect to various types of modeling errors. To prove the correctness of our algorithm, we need to understand the dynamics of timed automata—in particular, the structure of the limit cycles of timed automata.     

同步格值自动机的约简和最小化算法

引入了完备L-Fuzzy矩阵的概念,提出了取值于格半群上的输入字符和输出字符长度相同的模糊自动机的概念,即完备的同步格值自动机的概念,研究了它的主要性质;从行为矩阵出发,给出了完备的同步格值自动机状态等价和自动机等价的定义,从自动机的状态等价,研究了该自动机可约简的条件,并得到了该自动机的最小化算法。     

An Automata Based Approach for Verifying Information Flow Properties

We present an automated verification technique to verify trace based information flow properties for finite state systems. We show that the Basic Security Predicates (BSPs) defined by Mantel in [Mantel, H., Possibilistic Definitions of Security – An Assembly Kit, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop (2000), pp. 185–199], which are shown to be the building blocks of known trace based information flow properties, can be characterised in terms of regularity preserving language theoretic operations. This leads to a decision procedure for checking whether a finite state system satisfies a given BSP. Verification techniques in the literature (e.g. unwinding) are based on the structure of the transition system and are incomplete in some cases. In contrast, our technique is language based and complete for all information flow properties that can be expressed in terms of BSPs.     

基于超级自动机的语言识别及逻辑推理

该文根据自动机的定义,对超级自动机作了特定的定义,并给出了自动机对语言的识别功能的具体步骤。接着由超级自动机的定义,以一个特殊的例子给出了超级自动机的语言识别和逻辑推理功能。     

Automata for learning sequential tasks

This paper describes a system that is capable of learning both combinational and sequential tasks. The system learns from sequences of input/output examples in which each pair of input and output represents a step in a task. The system uses finite state machines as its internal models. This paper proposes a method for inferring finite state machines from examples. New algorithms are developed for modifying the finite state machines to allow the system to adapt to changes. In addition, new algorithms are developed to allow the system to handle inconsistent information that may result from noise in the training examples. The system can handle sequential tasks involving long-term dependencies for which recurrent neural networks have been shown to be inadequate. Moreover, the learned finite state machines are easy to be implemented in VLSI. The system has a wide range of applications including but not limited to (a) sequence detection, prediction, and production, (b) intelligent macro systems that can learn rather than simply record sequences of steps performed by a computer user, and (c) design automation systems for designing finite state machines or sequential circuits. C. H. Ben CHOI, Ph.D.: He got his B. S., M. S., and Ph.D. degrees all from The Ohio State University in the United States. His major areas of study include Solid State Microelectronics, Computer Engineering, and Computer Information Science. He has works on general associative memory, parallel and distributed computer architectures, and machine learning. He currently works on a project concerning theoretical aspects of learning machine. His research interests include hardware and software methods of building an intelligent machine.     

Stuttering for Abstract Probabilistic Automata

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. In a series of recent papers, we proposed Abstract Probabilistic Automata (APAs), a new abstraction framework for representing possibly infinite sets of PAs. We have developed a complete abstraction theory for APAs, and also proposed the first specification theory for them. APAs support both satisfaction and refinement operators, together with classical stepwise design operators.One of the major drawbacks of APAs is that the formalism cannot capture PAs with hidden actions – such actions are however necessary to describe behaviors that shall not be visible to a third party. In this paper, we revisit and extend the theory of APAs to such context. Our first main result takes the form of proposal for a new probabilistic satisfaction relation that captures several definitions of PAs with hidden actions. Our second main contribution is to revisit all the operations and properties defined on APAs for such notions of PAs. Finally, we also establish the first link between stochastic modal logic and APAs, hence linking an automata-based specification theory to a logical one.     

Automata for direct radix conversion

Modular logic circuits are described that directly transform on a digit by digit basis a number from one radix to another. Each device—an automaton—is of combined Moore-Mealy design of which the Moore output is a coefficient in the transformed radix, and the Mealy output is an untransformed residue passed on to the next identically designed circuit. Each logic circuit is completely independent of word length, and transformation relative to the input string is exact at each instant of time with all transformed digits simultaneously available. For fractional number conversion, any specified accuracy can be obtained merely by the addition of more modular logic circuits to the chain.     

Cache-Conscious Automata for XML Filtering

Hardware cache behavior is an important factor in the performance of memory-resident, data-intensive systems such as XML filtering engines. A key data structure in several recent XML filters is the automaton, which is used to represent the long-running XML queries in the main memory. In this paper, we study the cache performance of automaton-based XML filtering through analytical modeling and system measurement. Furthermore, we propose a cache-conscious automaton organization technique, called the hot buffer, to improve the locality of automaton state transitions. Our results show that 1) our cache performance model for XML filtering automata is highly accurate and 2) the hot buffer improves the cache performance as well as the overall performance of automaton-based XML filtering     

Discrete Semantics for Hybrid Automata

Many natural systems exhibit a hybrid behavior characterized by a set of continuous laws which are switched by discrete events. Such behaviors can be described in a very natural way by a class of automata called hybrid automata. Their evolution are represented by both dynamical systems on dense domains and discrete transitions. Once a real system is modeled in a such framework, one may want to analyze it by applying automatic techniques, such as Model Checking or Abstract Interpretation. Unfortunately, the discrete/continuous evolutions not only provide hybrid automata of great flexibility, but they are also at the root of many undecidability phenomena. This paper addresses issues regarding the decidability of the reachability problem for hybrid automata (i.e., “can the system reach a state a from a state b?”) by proposing an “inaccurate” semantics. In particular, after observing that dense sets are often abstractions of real world domains, we suggest, especially in the context of biological simulation, to avoid the ability of distinguishing between values whose distance is less than a fixed ε. On the ground of the above considerations, we propose a new semantics for first-order formulæ which guarantees the decidability of reachability. We conclude providing a paradigmatic biological example showing that the new semantics mimics the real world behavior better than the precise one.     

Hierarchical Cellular Automata for Visual Saliency

Saliency detection, finding the most important parts of an image, has become increasingly popular in computer vision. In this paper, we introduce Hierarchical Cellular Automata (HCA)—a temporally evolving model to intelligently detect salient objects. HCA consists of two main components: Single-layer Cellular Automata (SCA) and Cuboid Cellular Automata (CCA). As an unsupervised propagation mechanism, Single-layer Cellular Automata can exploit the intrinsic relevance of similar regions through interactions with neighbors. Low-level image features as well as high-level semantic information extracted from deep neural networks are incorporated into the SCA to measure the correlation between different image patches. With these hierarchical deep features, an impact factor matrix and a coherence matrix are constructed to balance the influences on each cell’s next state. The saliency values of all cells are iteratively updated according to a well-defined update rule. Furthermore, we propose CCA to integrate multiple saliency maps generated by SCA at different scales in a Bayesian framework. Therefore, single-layer propagation and multi-scale integration are jointly modeled in our unified HCA. Surprisingly, we find that the SCA can improve all existing methods that we applied it to, resulting in a similar precision level regardless of the original results. The CCA can act as an efficient pixel-wise aggregation algorithm that can integrate state-of-the-art methods, resulting in even better results. Extensive experiments on four challenging datasets demonstrate that the proposed algorithm outperforms state-of-the-art conventional methods and is competitive with deep learning based approaches.     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

三维几何约束求解的自由度归约算法

三维几何约束求解在装配设计、几何造型和动力学分析等领域有着广泛的应用．在分析基本几何元素间的约束关系对刚体自由度状态影响的基础上,提出刚体自由度的归约算法,以求得满足约束后刚体的自由度状态空间;以刚体自由度状态空间分析为基础,实现对合理约束的推理求解和约束一致性维护,该算法解决了三维几何约束求解中自由度计算问题,同时避免了一些推理求解算法中出现的“组合爆炸”问题．     

袋自动机

提出了袋自动机模型和袋语言的概念,并给出了袋自动机的状态转换图;分析了袋语言重复序列在状态转换图中的反映,并划分为不变重复序列、增重复序列、减重复序列和传递重复序列,给出了袋语言的结构特性;研究了袋语言类同Chomsky文法体系中各型语言的关系,证明了正规语言类是袋语言类的真子集,袋语言类是上下文有关语言类的真子集,而袋语言类同上下文无关语言类是两个相交但互不包含的语言类,即存在不是上下文无关语言的袋语言,也存在无法用袋自动机产生的上下文无关语言.     

Automata for XML—A survey

Automata play an important role for the theoretical foundations of XML data management, but also in tools for various XML processing tasks. This survey article aims to give an overview of fundamental properties of the different kinds of automata used in this area and to relate them to the four key aspects of XML processing: schemas, navigation, querying and transformation.