Search results for "AUTOMATA"

The double-incompleteness theorem

1976

Let T be a strong enough theory, and M - its metatheory, both are consistent. Then there is a closed arithmetical formula H that is undecidable in T, but one cannot prove in M neither that H is T-unprovable, nor that H is T-unrefutable. For English translation and proof, see K. Podnieks What is mathematics: Godel's theorem and around.

Matrix-based complexity functions and recognizable picture languages

2008

Some Algebraic Properties of Machine Poset of Infinite Words

2008

The complexity of infinite words is considered from the point of view of a transformation with a Mealy machine that is the simplest model of a finite automaton transducer. We are mostly interested in algebraic properties of the underlying partially ordered set. Results considered with the existence of supremum, infimum, antichains, chains and density aspects are investigated.

Deciding properties of integral relational automata

1994

This paper investigates automated model checking possibilities for CTL* formulae over infinite transition systems represented by relational automata (RA). The general model checking problem for CTL* formulae over RA is shown undecidable, the undecidability being observed already on the class of Restricted CTL formulae. The decidability result, however, is obtained for another substantial subset of the logic, called A-CTL*+, which includes all ”linear time” formulae.

Verification of Well-Formed Communicating Recursive State Machines

2008

AbstractIn this paper we introduce a new (non-Turing equivalent) formal model of recursive concurrent programs called well-formed communicating recursive state machines (CRSM). CRSM extend recursive state machines (RSM) by allowing a restricted form of concurrency: a state of a module can be refined into a finite collection of modules (working in parallel) in a potentially recursive manner. Communication is only possible between the activations of modules invoked on the same fork. We study the model-checking problem of CRSM with respect to specifications expressed in a temporal logic that extends CaRet with a parallel operator (ConCaRet). We propose a decision algorithm that runs in time ex…

Minimal Büchi Automata for Certain Classes of LTL Formulas

2009

In this paper we calculate the minimal number of states of Buchi automata which encode some classes of linear temporal logic (LTL) formulas that are frequently used in model checking. Our results may be used for verification of the quality of algorithms which automatically translate LTL formulas into Buchi automata and for improving the quality and speed of such translators. In the last section of this paper we compare our lower-bound estimations to Buchi automata generated by two currently used translators: LTL2BA and SPOT.

Verification of scope-dependent hierarchical state machines

2008

AbstractA hierarchical state machine (Hsm) is a finite state machine where a vertex can either expand to another hierarchical state machine (box) or be a basic vertex (node). Each node is labeled with atomic propositions. We study an extension of such model which allows atomic propositions to label also boxes (Shsm). We show that Shsms can be exponentially more succinct than Shsms and verification is in general harder by an exponential factor. We carefully establish the computational complexity of reachability, cycle detection, and model checking against general Ltl and Ctl specifications. We also discuss some natural and interesting restrictions of the considered problems for which we can …

Quantum Finite One-Counter Automata

1999

In this paper the notion of quantum finite one-counter automata (QF1CA) is introduced. Introduction of the notion is similar to that of the 2-way quantum finite state automata in [1]. The well-formedness conditions for the automata are specified ensuring unitarity of evolution. A special kind of QF1CA, called simple, that satisfies the well-formedness conditions is introduced. That allows specify rules for constructing such automata more naturally and simpler than in general case. Possible models of language recognition by QF1CA are considered. The recognition of some languages by QF1CA is shown and compared with recognition by probabilistic counterparts.

A description based on languages of the final non-deterministic automaton

2014

The study of the behaviour of non-deterministic automata has traditionally focused on the languages which can be associated to the different states. Under this interpretation, the different branches that can be taken at every step are ignored. However, we can also take into account the different decisions which can be made at every state, that is, the branches that can be taken, and these decisions might change the possible future behaviour. In this case, the behaviour of the automata can be described with the help of the concept of bisimilarity. This is the kind of description that is usually obtained when the automata are regarded as labelled transition systems or coalgebras. Contrarily t…

Complexity of operations on cofinite languages

2010

International audience; We study the worst case complexity of regular operation on cofinite languages (i.e., languages whose complement is finite) and provide algorithms to compute efficiently the resulting minimal automata.