共查询到20条相似文献,搜索用时 437 毫秒
1.
In the classical framework of formal languages, a refinement operation is modeled by a substitution and an abstraction by
an inverse substitution. These mechanisms have been widely studied, because they describe a change in the specification level,
from an abstract view to a more concrete one, or conversely. For timed systems, there is up to now no uniform notion of substitution.
In this paper, we study timed substitutions in the general framework of signal-event languages, where both signals and events
are taken into account. We prove that regular signal-event languages are closed under substitution and inverse substitution.
To obtain these results, we use in a crucial way a “well known” result: regular signal-event languages are closed under intersection.
In fact, while this result is indeed easy for languages defined by Alur and Dill’s timed automata, it turns out that the construction
is much more tricky when considering the most involved model of signal-event automata. We give here a construction working
on finite and infinite signal-event words and taking into account signal stuttering, unobservability of zero-duration τ-signals and Zeno runs. Note that if several constructions have been proposed in particular cases, it is the first time that
a general construction is provided. 相似文献
2.
In this paper, we analyze the problem of state minimization in a class of Finite State Automata called Two Start State Deterministic Finite State Automata (2-MDFAs). A 2-MDFA is similar to a deterministic finite state automaton (DFA), in that on a given input, each state has precisely one destination state; however, it differs from a DFA in that there are two start states. A string is accepted by a 2-MDFA if and only if there exists a transitional path from either start state to a finish state, on that string. Observe that 2-MDFAs provide a limited amount of non-determinism and hence investigating their properties from the perspective of state minimization is a worthwhile pursuit. In case of unbounded non-determinism, i.e., Non-deterministic finite state automata (NFAs), it is well-known that the state minimization problem is PSPACE-complete [Jiang and Ravikumar in Proceedings of the 18th International Colloquium on Automata, Languages and Programming, ICALP’91, Madrid, Spain, July 8–12, 1991] and further that such automata can be exponentially more succinct than DFAs [Meyer and Fischer in Proceedings of the 12th SWAT(Annual Symposium on switching and automata theory), pp 188-191, 1971]. Even in the case of 2-MDFAs, the minimization problem remains non-trivial; indeed, Malcher in Theor Comput Sci 327(3):375–390, 2004 shows that the corresponding decision problem is NP-complete. We focus on deriving approximability bounds for the state minimization problem in 2-MDFAs. Our main contribution in the current paper, is the design of an n-approximation algorithm for state minimization in 2-MDFAs, where n denotes the minimum number of states required to represent the input language as a 2-MDFA. We also present a proof that this bound is tight for our algorithm.The work of K. Subramani was supported in part by the Air-Force office of Scientific Research under Grant FA9550-06-1-0050 相似文献
3.
I. I. Macarie 《Theory of Computing Systems》1997,30(1):91-109
We present properties of multihead two-way probabilistic finite automata that parallel those of their deterministic and nondeterministic
counterparts. We define multihead probabilistic finite automata withlogspace constructible transition probabilities, and we describe a technique to simulate these automata by standard logspace probabilistic Turing
machines. Next, we represent logspace probabilistic complexity classes as proper hierarchies based on corresponding multihead
two-way probabilistic finite automata, and we show their (deterministic logspace) reducibility to the second levels of these
hierarchies.
We obtain a simple formula for the maximum inherent bandwidth of the configuration transition matrices associated with thek-head probabilistic finite automata processing a length-n input string. (The inherent bandwidth of the configuration transition matrices associated with an automaton processing a
length-n input string is the smallest bandwidth we can get by changing the enumeration order of the automaton’s configurations.) Partially
based on this relation, we find an apparently easier logspace complete problem forPL (the class of languages recognized by logspace unbounded-error probabilistic Turing machines), and we discuss possibilities
for a space-efficient deterministic simulation of probabilistic automata.
This research was supported by the National Science Foundation under Grant No. CDA 8822724 while the author was at the University
of Rochester. An extended abstract of this paper appeared in Proceedings, Second Latin American Symposium, LATIN ’95: Theoretical
Informatics, Valparaiso, Chile, April 1995. 相似文献
4.
I. K. Rystsov 《Cybernetics and Systems Analysis》2009,45(1):8-18
Linear and affine automata are considered in their general form. The concept of dimensions of a finite automaton is introduced
and finite automata of maximal dimensions are shown to be possible. The state reachability problem in monomial form is proved
to be undecidable for two-dimensional affine automata. An analogue of Moore's theorem and theorems on homogenous and diagnostic
words are also proved. An application of linear automata to mathematical economics is considered.
Translated from Kibernetika i Sistemnyi Analiz, No. 1, pp. 10–21, January–February 2009. 相似文献
5.
We suggest that developing automata theoretic foundations is relevant for knowledge theory, so that we study not only what is known by agents, but also the mechanisms by which such knowledge is arrived at. We define a class of epistemic automata, in which agents’ local states are annotated with abstract knowledge assertions about others. These are finite state agents
who communicate synchronously with each other and information exchange is ‘perfect’. We show that the class of recognizable languages has good closure
properties, leading to a Kleene-type theorem using what we call regular knowledge expressions. These automata model distributed causal knowledge in the following way: each agent in the system has a partial knowledge
of the temporal evolution of the system, and every time agents synchronize, they update each other’s knowledge, resulting
in a more up-to-date view of the system state. Hence we show that these automata can be used to solve the satisfiability problem
for a natural epistemic temporal logic for local properties. Finally, we characterize the class of languages recognized by
epistemic automata as the regular consistent languages studied in concurrency theory. 相似文献
6.
A minimized automaton representation of reachable states 总被引:1,自引:0,他引:1
Gerard J. Holzmann Anuj Puri 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):270-278
We consider the problem of storing a set S⊂Σkas a deterministic finite automaton (DFA). We show that inserting a new string σ∈Σk or deleting a string from the set S represented as a minimized DFA can be done in expected time O(k|Σ|), while preserving
the minimality of the DFA. The method can be applied to reduce the memory requirements of model checkers that are based on
explicit state enumeration. As an example, we discuss an implementation of the method for the model checker Spin. 相似文献
7.
T. Yokomori 《Theory of Computing Systems》1996,29(3):259-270
We investigate the learning problem of two-tape deterministic finite automata (2-tape DFAs) from queries and counterexamples.
Instead of accepting a subset of ∑*, a 2-tape DFA over an alphabet ∑ accepts a subset of ∑* × ∑*, and therefore, it can specify
a binary relation on ∑*. In [3] Angluin showed that the class of deterministic finite automata (DFAs) is learnable in polynomial
time from membership queries and equivalence queries, namely, from a minimally adequate teacher (MAT).
In this article we show that the class of 2-tape DFAs is learnable in polynomial time from MAT. More specifically, we show
an algorithm that, given any languageL accepted by an unknown 2-tape DFAM, learns from MAT a two-tape nonde-terministic finite automaton (2-tape NFA)M′ acceptingL in time polynomial inn andl, wheren is the size ofM andl is the maximum length of any counterexample provided during the learning process.
This work was supported in part by Grants-in-Aid for Scientific Research No. 04229105 from the Ministry of Education, Science,
and Culture, Japan. 相似文献
8.
Lakshmi Manasa Shankara Narayanan Krishna Chinmay Jain 《Theory of Computing Systems》2011,48(3):648-679
Weighted timed automata (WTA), introduced in Alur et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 49–62, Springer, Berlin,
2001), Behrmann et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 147–161, Springer, Berlin, 2001) are an extension of Alur and Dill (Theor. Comput. Sci. 126(2):183–235, 1994) timed automata, a widely accepted formalism for the modelling and verification of real time systems. Weighted timed automata
extend timed automata by allowing costs on the locations and edges. There has been a lot of interest Bouyer et al. (Inf. Process.
Lett. 98(5):188–194, 2006), Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008), Brihaye et al. (Proceedings of FORMATS/FTRTFT’04, LNCS, vol. 3253, pp. 277–292, Springer, Berlin, 2004), Brihaye et al. (Inf. Comput. 204(3):408–433, 2006) in studying the model checking problem of weighted timed automata. The properties of interest are written using logic weighted
CTL (WCTL), an extension of CTL with costs. It has been shown Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008) that the problem of model checking WTAs with a single clock using WCTL with no external cost variables is decidable, while 3 clocks render the problem undecidable Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006). The question of 2 clocks is open. In this paper, we introduce a subclass of weighted timed automata called weighted integer
reset timed automata (WIRTA) and study the model checking problem. We give a clock reduction technique for WIRTA. Given a
WIRTA A\mathcal{A} with n≥1 clocks, we show that a single clock WIRTA A¢\mathcal{A}' preserving the paths and costs of A\mathcal{A} can be obtained. This gives us the decidability of model checking WIRTA with n≥1 clocks and m≥1 costs using WCTL with no external cost variables. We then show that for a restricted version of WCTL with external cost variables, the model checking problem is undecidable for WIRTA with 3 stopwatch costs and 1 clock. Finally, we show that model checking
WTA with 2 clocks and 1 stopwatch cost against WCTL with no external cost variables is undecidable, thereby answering a question that has remained long open. 相似文献
9.
F. Durand 《Theory of Computing Systems》1998,31(2):169-185
If a nonperiodic sequence X is the image by a morphism of a fixed point of both a primitive substitution σ and a primitive substitution τ , then the dominant eigenvalues of the matrices of σ and τ are multiplicatively dependent. This is the way we propose to generalize Cobham's theorem.
Received April 1996, and in final form April 1997. 相似文献
10.
Xiaowei Zhang Yongming Li 《Soft Computing - A Fusion of Foundations, Methodologies and Applications》2009,13(6):611-616
Intuitionistic fuzzy recognizers and intuitionistic fuzzy finite automata are discussed. The notions of intuitionistic fuzzy
recognizer, complete accessible intuitionistic fuzzy recognizer, intuitionistic fuzzy finite automata, deterministic intuitionistic
fuzzy finite automata, and intuitionistic fuzzy language are introduced. It is shown that the languages recognized by intuitionistic
fuzzy recognizer are regular, and the intuitionistic fuzzy languages recognized by the intuitionistic fuzzy finite automaton
and the intuitionistic fuzzy languages recognized by deterministic intuitionistic fuzzy finite automaton are equivalent.
This work is supported by National Science Foundation of China (Grant No.10571112), “TRAPOYT” of China and National 973 Foundation
Research Program(Grant No.2002CB312200). 相似文献
11.
Philip A. Bernstein Todd J. Green Sergey Melnik Alan Nash 《The VLDB Journal The International Journal on Very Large Data Bases》2008,17(2):333-353
Mapping composition is a fundamental operation in metadata driven applications. Given a mapping over schemas σ1 and σ2 and a mapping over schemas σ2 and σ3, the composition problem is to compute an equivalent mapping over σ1 and σ3. We describe a new composition algorithm that targets practical applications. It incorporates view unfolding. It eliminates
as many σ2 symbols as possible, even if not all can be eliminated. It covers constraints expressed using arbitrary monotone relational
operators and, to a lesser extent, non-monotone operators. And it introduces the new technique of left composition. We describe
our implementation, explain how to extend it to support user-defined operators, and present experimental results which validate
its effectiveness.
T.J. Green and A. Nash’s work was performed during an internship at Microsoft Research.
A preliminary version of this work was published in the VLDB 2006 conference proceedings. 相似文献
12.
Axel Legay 《International Journal on Software Tools for Technology Transfer (STTT)》2012,14(2):119-143
(Omega-)Regular model checking is the name of a family of techniques in which states are represented by words, sets of states by finite automata on these
objects, and transitions by finite automata operating on pairs of state encodings, i.e., finite-state transducers. In this
context, the problem of computing the set of reachable states of a system can be reduced to the one of computing the iterative
closure of the finite-state transducer representing its transition relation. In this tutorial article, we survey an extrapolation-based
technique for computing the closure of a given transducer. The approach proceeds by comparing successive elements of a sequence
of approximations of the iteration, detecting an “increment” that is added to move from one approximation to the next, and
extrapolating the sequence by allowing arbitrary repetitions of this increment. The technique applies to finite-word and deterministic
weak Büchi automata. Finally, we discuss the implementation of these results within the T(O)RMC toolsets and present case
studies that show the advantages and the limits of the approach. 相似文献
13.
Nicolas Peltier 《Annals of Mathematics and Artificial Intelligence》2009,56(1):65-85
We propose a method to use finite model builders in order to construct infinite models of first-order formulae. The constructed
models are Herbrand interpretations, in which the interpretation of the predicate symbols is specified by tree tuple automata
(Comon et al. 1997). Our approach is based on formula transformation: a formula ϕ is transformed into a formula Δ(ϕ) s.t. ϕ has a model representable by a term tuple automaton iff Δ(ϕ) has a finite model. This paper is an extended version of Peltier (2008). 相似文献
14.
Yasubumi Sakakibara 《New Generation Computing》1990,7(4):365-380
In this paper we present a new inductive inference algorithm for a class of logic programs, calledlinear monadic logic programs. It has several unique features not found in Shapiro’s Model Inference System. It has been proved that a set of trees isrational if and only if it is computed by a linear monadic logic program, and that the rational set of trees is recognized by a tree
automaton. Based on these facts, we can reduce the problem of inductive inference of linear monadic logic programs to the
problem of inductive inference of tree automata. Further several efficient inference algorithms for finite automata have been
developed. We extend them to an inference algorithm for tree automata and use it to get an efficient inductive inference algorithm
for linear monadic logic programs. The correctness, time complexity and several comparisons of our algorithm with Model Inference
System are shown. 相似文献
15.
Oscar H. Ibarra 《Theoretical computer science》2010,411(3):581-593
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. 相似文献
16.
Abuzer Yakary?lmaz Rūsi?? Freivalds A. C. Cem Say Ruben Agadzanyan 《Natural computing》2012,11(1):81-94
In classical computation, a “write-only memory” (WOM) is little more than an oxymoron, and the addition of WOM to a (deterministic
or probabilistic) classical computer brings no advantage. We prove that quantum computers that are augmented with WOM can
solve problems that neither a classical computer with WOM nor a quantum computer without WOM can solve, when all other resource
bounds are equal. We focus on realtime quantum finite automata, and examine the increase in their power effected by the addition
of WOMs with different access modes and capacities. Some problems that are unsolvable by two-way probabilistic Turing machines
using sublogarithmic amounts of read/write memory are shown to be solvable by these enhanced automata. 相似文献
17.
Hing Leung 《Acta Informatica》1998,35(7):595-624
We develop a new algorithm for determining if a given nondeterministic finite automaton is limited in nondeterminism. From
this, we show that the number of nondeterministic moves of a finite automaton, if limited, is bounded by where is the number of states. If the finite automaton is over a one-letter alphabet, using Gohon's result the number of nondeterministic
moves, if limited, is less than . In both cases, we present families of finite automata demonstrating that the upper bounds obtained are almost tight. We
also show that the limitedness problem of the number of nondeterministic moves of finite automata is PSPACE-hard. Since the
problem is already known to be in PSPACE, it is therefore PSPACE-complete.
Received: 14 June 1994 / 3 December 1997 相似文献
18.
Juraj Hromkovi Sebastian Seibert Juhani Karhumki Hartmut Klauck Georg Schnitger 《Information and Computation》2002,172(2):202
While deterministic finite automata seem to be well understood, surprisingly many important problems concerning nondeterministic finite automata (nfa's) remain open. One such problem area is the study of different measures of nondeterminism in finite automata and the estimation of the sizes of minimal nondeterministic finite automata. In this paper the concept of communication complexity is applied in order to achieve progress in this problem area. The main results are as follows:1. Deterministic communication complexity provides lower bounds on the size of nfa's with bounded unambiguity. Applying this fact, the proofs of several results about nfa's with limited ambiguity can be simplified and presented in a uniform way.2. There is a family of languages KONk2 with an exponential size gap between nfa's with polynomial leaf number/ambiguity and nfa's with ambiguity k. This partially provides an answer to the open problem posed by B. Ravikumar and O. Ibarra (1989, SIAM J. Comput.18, 1263–1282) and H. Leung (1998, SIAM J. Comput.27, 1073–1082). 相似文献
19.
Yongxi Cheng 《计算机科学技术学报》2007,22(6):909-913
We investigate the problem of listing combinations using a special class of operations, prefix shifts. Combinations are represented as bitstrings of O's and l's, and prefix shifts are the operations of rotating some prefix of a bitstring by one position to left or right. We give a negative answer to an open problem asked by F. Ruskey and A. Williams (Generating combinations by prefix shifts, In Proc. llth Annual International Computing and Combinatorics Conference 2005, LNCS 3595, Springer, 2005, pp.570-576), that is whether we can generate combinations by only using three very basic prefix shifts on bitstrings, which are transposition of the first two bits and the rotation of the entire bitstring by one position in either direction (i.e., applying the permutations σ2, σn and σn^-1 to the indices of the bitstrings). 相似文献
20.
I. K. Rystsov 《Cybernetics and Systems Analysis》2008,44(2):170-174
The mortality problem for 2×2 matrices is treated from the automata theory viewpoint. This problem is shown to be closely
related to the reachability problem for linear and affine automata of low dimensions. The decidability of the reachability
problem is proved for some subclasses of one-dimensional affine automata.
__________
Translated from Kibernetika i Sistemnyi Analiz, No. 2, pp. 24–29, March–April 2008. 相似文献