The polynomial time decidability of simulation relations for finite state processes: A HORNSAT based approach

1997 ◽  
pp. 603-641 ◽  
Author(s):  
Sandeep Shukla ◽  
Daniel Rosenkrantz ◽  
Harry Hunt ◽  
Richard Stearns
Keyword(s):  
Polynomial Time ◽  
Finite State ◽  
Simulation Relations

scholarly journals Copyful Streaming String Transducers

2021 ◽  
Vol 178 (1-2) ◽  
pp. 59-76
Author(s):  
Emmanuel Filiot ◽  
Pierre-Alain Reynier
Keyword(s):  
Polynomial Time ◽  
Equivalence Problem ◽  
Expressive Power ◽  
The Other ◽  
Finite State Automata ◽  
Finite State ◽  
Variable Content ◽  
Deterministic Automata ◽  
Intermediate Output ◽  
Linear Manner

Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Černý in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decidable equivalence problem (in PSpace). On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of deterministic copyful SST. Our contributions are as follows: (i)HDT0L systems and total deterministic copyful SST have the same expressive power, (ii)the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in quadratic time. As a consequence, equivalence of deterministic SST is decidable, (iii)the functionality of non-deterministic copyful SST is decidable, (iv)determining whether a non-deterministic copyful SST can be transformed into an equivalent non-deterministic copyless SST is decidable in polynomial time.

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.

scholarly journals Computing the Expected Edit Distance from a String to a Probabilistic Finite-State Automaton

2017 ◽  
Vol 28 (05) ◽  
pp. 603-621 ◽  
Author(s):  
Jorge Calvo-Zaragoza ◽  
Jose Oncina ◽  
Colin de la Higuera
Keyword(s):  
Polynomial Time ◽  
Edit Distance ◽  
Input String ◽  
Finite State Automaton ◽  
Global View ◽  
Finite State ◽  
Median String

In a number of fields, it is necessary to compare a witness string with a distribution. One possibility is to compute the probability of the string for that distribution. Another, giving a more global view, is to compute the expected edit distance from a string randomly drawn to the witness string. This number is often used to measure the performance of a prediction, the goal then being to return the median string, or the string with smallest expected distance. To be able to measure this, computing the distance between a hypothesis and that distribution is necessary. This paper proposes two solutions for computing this value, when the distribution is defined with a probabilistic finite state automaton. The first is exact but has a cost which can be exponential in the length of the input string, whereas the second is a fully polynomial-time randomized schema.

scholarly journals LATTICED SIMULATION RELATIONS AND GAMES

2010 ◽  
Vol 21 (02) ◽  
pp. 167-189 ◽  
Author(s):  
ORNA KUPFERMAN ◽  
YOAD LUSTIG
Keyword(s):  
Formal Methods ◽  
Polynomial Time ◽  
Partially Ordered ◽  
Multiple View ◽  
A Value ◽  
Lattice Element ◽  
Kripke Structures ◽  
Simulation Relations ◽  
Truth Value ◽  
Definition Of

Multi-valued Kripke structures are Kripke structures in which the atomic propositions and the transitions are not Boolean and can take values from some set. In particular, latticed Kripke structures, in which the elements in the set are partially ordered, are useful in abstraction, query checking, and reasoning about multiple view-points. The challenges that formal methods involve in the Boolean setting are carried over, and in fact increase, in the presence of multi-valued systems and logics. We lift to the latticed setting two basic notions that have been proven useful in the Boolean setting. We first define latticed simulation between latticed Kripke structures. The relation maps two structures M1 and M2 to a lattice element that essentially denotes the truth value of the statement "every behavior of M1 is also a behavior of M2". We show that latticed-simulation is logically characterized by the universal fragment of latticed µ-calculus, and can be calculated in polynomial time. We then proceed to defining latticed two-player games. Such games are played along graphs in which each transition have a value in the lattice. The value of the game essentially denotes the truth value of the statement "the ∨-player can force the game to computations that satisfy the winning condition". An earlier definition of such games involved a zig-zagged traversal of paths generated during the game. Our definition involves a forward traversal of the paths, and it leads to better understanding of multi-valued games. In particular, we prove a min-max property for such games, and relate latticed simulation with latticed games.

scholarly journals On the Complexity of Deciding Behavioural Equivalences and Preorders. A Survey

1996 ◽  
Vol 3 (39) ◽  
Author(s):  
Hans Hüttel ◽  
Sandeep Shukla
Keyword(s):  
Computational Complexity ◽  
Polynomial Time ◽  
Branching Time ◽  
Complexity Results ◽  
Special Cases ◽  
Finite State ◽  
Bisimulation Equivalence ◽  
Infinite State ◽  
Context Free

This paper gives an overview of the computational complexity of all the equivalences in the linear/branching time hierarchy [vG90a] and the preorders<br />in the corresponding hierarchy of preorders. We consider finite state or regular processes as well as infinite-state BPA [BK84b] processes. <br />A distinction, which turns out to be important in the finite-state processes, is that of simulation-like equivalences/preorders vs. trace-like equivalences<br />and preorders. Here we survey various known complexity results for these relations. For regular processes, all simulation-like equivalences and preorders are decidable in polynomial time whereas all trace-like equivalences and preorders are PSPACE-Complete. We also consider interesting special<br />classes of regular processes such as deterministic, determinate, unary, locally unary, and tree-like processes and survey the known complexity results in<br />these special cases. For infinite-state processes the results are quite different. For the class of context-free processes or BPA processes any preorder or equivalence beyond bisimulation is undecidable but bisimulation equivalence is polynomial time<br />decidable for normed BPA processes and is known to be elementarily decidable in the general case. For the class of BPP processes, all preorders and equivalences apart from bisimilarity are undecidable. However, bisimilarity<br />is decidable in this case and is known to be decidable in polynomial time for normed BPP processes.

scholarly journals Model checking usage policies

2014 ◽  
Vol 25 (3) ◽  
pp. 710-763 ◽  
Author(s):  
MASSIMO BARTOLETTI ◽  
PIERPAOLO DEGANO ◽  
GIAN LUIGI FERRARI ◽  
ROBERTO ZUNINO
Keyword(s):  
Model Checking ◽  
Polynomial Time ◽  
Real World ◽  
Formal Model ◽  
Expressive Power ◽  
Finite State Automata ◽  
Time Model ◽  
Real World Applications ◽  
Finite State ◽  
Resource Creation

We study usage automata, a formal model for specifying policies on the usage of resources. Usage automata extend finite state automata with some additional features, parameters and guards, that improve their expressivity. We show that usage automata are expressive enough to model policies of real-world applications. We discuss their expressive power, and we prove that the problem of telling whether a computation complies with a usage policy is decidable. The main contribution of this paper is a model checking technique for usage automata. The model is that of usages, i.e. basic processes that describe the possible patterns of resource access and creation. In spite of the model having infinite states, because of recursion and resource creation, we devise a polynomial-time model checking technique for deciding when a usage complies with a usage policy.

Sign in / Sign up

Export Citation Format

Share Document