scholarly journals A Transformation-Based Approach to Implication of GSTE Assertion Graphs

2013 ◽  
Vol 2013 ◽  
pp. 1-7
Author(s):  
Guowu Yang ◽  
William N. N. Hung ◽  
Xiaoyu Song ◽  
Wensheng Guo
Keyword(s):  
Model Checking ◽  
Directed Graphs ◽  
Classical Model ◽  
Regular Languages ◽  
Finite State Automaton ◽  
Finite State Automata ◽  
Symbolic Trajectory Evaluation ◽  
Finite State ◽  
Symbolic Trajectory ◽  
Language Containment

Generalized symbolic trajectory evaluation (GSTE) is a model checking approach and has successfully demonstrated its powerful capacity in formal verification of VLSI systems. GSTE is an extension of symbolic trajectory evaluation (STE) to the model checking ofω-regular properties. It is an alternative to classical model checking algorithms where properties are specified as finite-state automata. In GSTE, properties are specified as assertion graphs, which are labeled directed graphs where each edge is labeled with two labeling functions: antecedent and consequent. In this paper, we show the complement relation between GSTE assertion graphs and finite-state automata with the expressiveness of regular languages andω-regular languages. We present an algorithm that transforms a GSTE assertion graph to a finite-state automaton and vice versa. By applying this algorithm, we transform the problem of GSTE assertion graphs implication to the problem of automata language containment. We demonstrate our approach with its application to verification of an FIFO circuit.

Synthesis with Mandatory Stop Actions

2021 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Antonio Di Stasio ◽  
Giuseppe Perelli ◽  
Shufang Zhu
Keyword(s):  
Model Checking ◽  
Finite State Automata ◽  
Deep Impact ◽  
Synthesis Technique ◽  
Büchi Automata ◽  
Finite State ◽  
Ltl Synthesis ◽  
Buchi Automata ◽  
The Impact

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

Finite-State Technology

2018 ◽  
Author(s):  
Mans Hulden
Keyword(s):  
Natural Language Processing ◽  
Natural Language ◽  
Computational Linguistics ◽  
Language Processing ◽  
Finite State Machines ◽  
Regular Languages ◽  
Finite State Automata ◽  
State Machines ◽  
Computational Phonology ◽  
Finite State

Finite-state machines—automata and transducers—are ubiquitous in natural-language processing and computational linguistics. This chapter introduces the fundamentals of finite-state automata and transducers, both probabilistic and non-probabilistic, illustrating the technology with example applications and common usage. It also covers the construction of transducers, which correspond to regular relations, and automata, which correspond to regular languages. The technologies introduced are widely employed in natural language processing, computational phonology and morphology in particular, and this is illustrated through common practical use cases.

scholarly journals Model Checking Temporal Logic Formulas Using Sticker Automata

2017 ◽  
Vol 2017 ◽  
pp. 1-33 ◽  
Author(s):  
Weijun Zhu ◽  
Changwei Feng ◽  
Huanmei Wu
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Complex Problem ◽  
Finite State Automaton ◽  
Dna Molecules ◽  
Single Stranded Dna ◽  
Finite State ◽  
Input Strings ◽  
Logic Model Checking ◽  
The Given

As an important complex problem, the temporal logic model checking problem is still far from being fully resolved under the circumstance of DNA computing, especially Computation Tree Logic (CTL), Interval Temporal Logic (ITL), and Projection Temporal Logic (PTL), because there is still a lack of approaches for DNA model checking. To address this challenge, a model checking method is proposed for checking the basic formulas in the above three temporal logic types with DNA molecules. First, one-type single-stranded DNA molecules are employed to encode the Finite State Automaton (FSA) model of the given basic formula so that a sticker automaton is obtained. On the other hand, other single-stranded DNA molecules are employed to encode the given system model so that the input strings of the sticker automaton are obtained. Next, a series of biochemical reactions are conducted between the above two types of single-stranded DNA molecules. It can then be decided whether the system satisfies the formula or not. As a result, we have developed a DNA-based approach for checking all the basic formulas of CTL, ITL, and PTL. The simulated results demonstrate the effectiveness of the new method.

Tricolor automata

2015 ◽  
Author(s):  
C. M. Sperberg-McQueen
Keyword(s):  
Regular Languages ◽  
The Other ◽  
Finite State Automata ◽  
Simple Application ◽  
Finite State

Tricolor automata are extensions of finite state automata, intended for the comparison of two regular languages; states and arcs in the automaton are colored to indicate whether they are peculiar to one language or the other, or common to both. Their design represents a simple application to practical purposes of ideas derived from the work of Glushkov and Brzozowski. Examples are given to show how tricolor automata can be used to visualize the intersection, union, and set difference of two languages, and algorithms for constructing them are given.

scholarly journals KNUTH–BENDIX FOR GROUPS WITH INFINITELY MANY RULES

2000 ◽  
Vol 10 (05) ◽  
pp. 539-589 ◽  
Author(s):  
D. B. A. EPSTEIN ◽  
P. J. SANDERS
Keyword(s):  
Computer Program ◽  
Regular Language ◽  
The Body ◽  
Finite State Automaton ◽  
Finite State Automata ◽  
Central Feature ◽  
Rapid Reduction ◽  
Automatic Structures ◽  
Small Constant ◽  
Finite State

We introduce a new class of groups with solvable word problem, namely groups specified by a confluent set of short-lex-reducing Knuth–Bendix rules which form a regular language. This simultaneously generalizes short-lex-automatic groups and groups with a finite confluent set of short-lex-reducing rules. We describe a computer program which looks for such a set of rules in an arbitrary finitely presented group. Our main theorem is that our computer program finds the set of rules, if it exists, given enough time and space. (This is an optimistic description of our result — for the more pessimistic details, see the body of the paper.) The set of rules is embodied in a finite state automaton in two variables. A central feature of our program is an operation, which we call welding, used to combine existing rules with new rules as they are found. Welding can be defined on arbitrary finite state automata, and we investigate this operation in abstract, proving that it can be considered as a process which takes as input one regular language and outputs another regular language. In our programs we need to convert several nondeterministic finite state automata to deterministic versions accepting the same language. We show how to improve somewhat on the standard subset construction, due to special features in our case. We axiomatize these special features, in the hope that these improvements can be used in other applications. The Knuth–Bendix process normally spends most of its time in reduction, so its efficiency depends on doing reduction quickly. Standard data structures for doing this can become very large, ultimately limiting the set of presentations of groups which can be so analyzed. We are able to give a method for rapid reduction using our much smaller two variable automaton, encoding the (usually infinite) regular language of rules found so far. Time taken for reduction in a given group is a small constant times the time taken for reduction in the best schemes known (see [5]), which is not too bad since we are reducing with respect to an infinite set of rules, whereas known schemes use a finite set of rules. We hope that the method described here might lead to the computation of automatic structures in groups for which this is currently infeasible. Some proofs have been omitted from this paper in the interests of brevity. Full details are provided in [4].

scholarly journals Non Homogeneous Rough Finite State Automaton

2021 ◽  
Vol 11 (2) ◽  
pp. 629-641
Author(s):  
B. Praba ◽  
R. Saranya
Keyword(s):  
Artificial Intelligence ◽  
Machine Learning ◽  
Dynamical Behaviour ◽  
Finite State Automaton ◽  
Finite State Automata ◽  
Lower Approximation ◽  
Upper Approximation ◽  
Finite State ◽  
Transition Map

Objective: The study of finite state automaton is an essential tool in machine learning and artificial intelligence. The class of rough finite state automaton captures the uncertainty using the rough transition map. The need to generalize this concept arises to adhere the dynamical behaviour of the system. Hence this paper focuses on defining non-homogeneous rough finite state automaton. Methodology: With the aid of Rough finite state automata we define the concept of non-homogeneous rough finite state automata. Findings: Non homogeneous Rough Finite State Automata (NRFSA) Mt is defined by a tuple (Q,Σ,δt,q0 (t),F(t)) The dynamical behaviour of any system can be expressed in terms of an information system at time t. This leads us to define non-homogeneous rough finite state automaton. For each time ‘t’ we generate lower approximation rough finite state automaton Mt_ and the upper approximation rough finite state automaton Mt- and the defined concepts are elaborated with suitable examples. The ordered pair , Mt=(M(t)-,M(t)-) is called as the non-homogeneous rough finite state automaton. Conclusion: Over all our study reveals the characterization of the system which changes its behaviour dynamically over a time ‘t’. Novelty: The novelty of the proposed article is that it clearly immense the system behaviour over a time ‘t’. Using this concept the possible and the definite transitions in the system can be calculated in any given time ‘t’.

scholarly journals Applications of the finite state automata for counting restricted permutations and variations

2012 ◽  
Vol 22 (2) ◽  
pp. 183-198
Author(s):  
Vladimir Baltic
Keyword(s):  
The Other ◽  
Finite State Automaton ◽  
Finite State Automata ◽  
Combinatorial Structures ◽  
Restricted Permutations ◽  
Finite State

In this paper, we use the finite state automata to count the number of restricted permutations and the number of restricted variations. For each type of restricted permutations, we construct a finite state automaton able to recognize and enumerate them. We, also, discuss how it encompasses the other known methods for enumerating permutations with restricted position, and in one case, we establish connections with some other combinatorial structures, such as subsets and compositions.

INFIX-FREE REGULAR EXPRESSIONS AND LANGUAGES

2006 ◽  
Vol 17 (02) ◽  
pp. 379-393 ◽  
Author(s):  
YO-SUB HAN ◽  
YAJUN WANG ◽  
DERICK WOOD
Keyword(s):  
Polynomial Time ◽  
Regular Language ◽  
Polynomial Time Algorithm ◽  
Time Algorithm ◽  
Regular Languages ◽  
Finite State Automaton ◽  
Primality Test ◽  
Finite State ◽  
State Pair ◽  
Free Decomposition

We study infix-free regular languages. We observe the structural properties of finite-state automata for infix-free languages and develop a polynomial-time algorithm to determine infix-freeness of a regular language using state-pair graphs. We consider two cases: 1) A language is specified by a nondeterministic finite-state automaton and 2) a language is specified by a regular expression. Furthermore, we examine the prime infix-free decomposition of infix-free regular languages and design an algorithm for the infix-free primality test of an infix-free regular language. Moreover, we show that we can compute the prime infix-free decomposition in polynomial time. We also demonstrate that the prime infix-free decomposition is not unique.

Sign in / Sign up

Export Citation Format

Share Document