Automata theory

Summary

Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science. The word automata comes from the Greek word αὐτόματος, which means "self-acting, self-willed, self-moving". An automaton (automata in plural) is an abstract self-propelled computing device which follows a predetermined sequence of operations automatically. An automaton with a finite number of states is called a Finite Automaton (FA) or Finite-State Machine (FSM). The figure on the right illustrates a finite-state machine, which is a well-known type of automaton. This automaton consists of states (represented in the figure by circles) and transitions (represented by arrows). As the automaton sees a symbol of input, it makes a transition (or jump) to another state, according to its transition function, which takes the previous state and current input symbol as its arguments. Automata theory is closely rel

Official source

https://en.wikipedia.org/wiki/Automata_theory

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (12)

Related publications

Related people (2)

Related people

Related units (3)

Related units

Related concepts (46)

Related concepts

Related courses (7)

Related courses

Related lectures (9)

Related lectures

Let T-1, ... , T-d be homogeneous trees with degrees q(1) + 1, ... , q(d) + 1 >= 3; respectively. For each tree, let h : Tj -> Z be the Busemann function with respect to a fixed boundary point ( end). Its level sets are the horocycles. The horocyclic product of T-1 , ... , T-d is the graph DL(q1, ... , q(d)) consisting of all d-tuples x(1) ... x(d) is an element of T-1 x ... x T-d with h(x(1)) + ... + h(x(d)) = 0, equipped with a natural neighbourhood relation. In the present paper, we explore the geometric, algebraic, analytic and probabilistic properties of these graphs and their isometry groups. If d =2 and q(1) = q(2) = q then we obtain a Cayley graph of the lamplighter group ( wreath product) 3q (sic) Z. If d = 3 and q(1) = q(2) = q(3) = q then DL is a Cayley graph of a finitely presented group into which the lamplighter group embeds naturally. In general, when d - 4 and q(1) = ... = q(d) = q is such that each prime power in the decomposition of q is larger than d 1, we show that DL is a Cayley graph of a finitely presented group. This group is of type Fd - 1, but not Fd. It is not automatic, but it is an automata group in most cases. On the other hand, when the q(j) do not all coincide, DL(q(1) , ... , q(d))is a vertex-transitive graph, but is not a Cayley graph of a finitely generated group. Indeed, it does not even admit a group action with finitely many orbits and finite point stabilizers. The l(2)-spectrum of the "simple random walk" operator on DL is always pure point. When d = 2, it is known explicitly from previous work, while for d = 3 we compute it explicitly. Finally, we determine the Poisson boundary of a large class of group-invariant random walks on DL. It coincides with a part of the geometric boundary of DL.

2008

, ,

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: implementations of linearizable objects can be composed into more complex linearizable objects. However, devising complete linearizable objects is very difficult requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation, namely optimizing algorithms to handle common scenarios more efficiently. Unfortunately, the outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative linarizability. This property is as general as linearizability, yet it allows intra-object composability, namely proving multiple protocol phases separately. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in its trace-based as well as its mechanically checked automaton-based versions in an Isabelle I/O automata framework. This framework enables for the first time scalable specifications and mechanical proofs of speculative implementations of linearizable objects.

2011

, ,

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: a system composed of linearizable objects is itself linearizable. However, devising linearizable objects is very difficult, requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation: optimizing algorithms to handle common scenarios more efficiently. The outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative linearizability. This property is as general as linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in a trace-based as well as an automaton-based model. To obtain a further degree of confidence, we also formalize and mechanically check the theorem in the automaton-based model, using the I/O automata framework within the Isabelle interactive proof assistant. We expect our framework to enable, for the first time, scalable specifications and mechanical proofs of speculative implementations of linearizable objects.

Assoc Computing Machinery2012

, ,

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: a system composed of linearizable objects is itself linearizable. However, devising linearizable objects is very difficult, requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation: optimizing algorithms to handle common scenarios more efficiently. The outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative linearizability. This property is as general as linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in a trace-based as well as an automaton-based model. To obtain a further degree of confidence, we also formalize and mechanically check the theorem in the automaton-based model, using the I/O automata framework within the Isabelle interactive proof assistant. We expect our framework to enable, for the first time, scalable specifications and mechanical proofs of speculative implementations of linearizable objects.

Assoc Computing Machinery2012

, ,

2011