Concept

Machine de Turing alternante

En informatique théorique, et notamment en théorie de la complexité, les machines de Turing alternantes sont une généralisation des machines de Turing non déterministes. Leur mode d'acceptation généralise les conditions d'acceptation utilisées dans les classes de complexité NP et co-NP. Le concept de machine de Turing alternante a été formulé par Ashok K. Chandra et Larry Stockmeyer et indépendamment par Dexter Kozen en 1976, avec un article publié en commun en 1981. Chandra et Stockmeyer les utilisent pour démontrer des bornes inférieures en temps exponentiel pour des jeux à deux joueurs. Les machines alternantes donnent une autre interprétation de la hiérarchie polynomiale. La définition de la classe NP utilise un mode « existentiel » pour les calculs : un calcul est acceptant s'il existe un choix qui amène en un état d'acceptation. La définition de co-NP en revanche utilise un mode « universel » de calcul : c'est seulement quand tous les choix possibles amènent à un état d'acceptation qu'un calcul est acceptant. Dans une machine de Turing alternante, le mode de calcul alterne entre ces deux modes. La notion de machine de Turing alternante étend celle de machine de Turing non déterministe. Les états sont de deux types : les états existentiels (notés pour "ou") et les états universels (notés pour "et"). Ainsi, une configuration (c'est-à-dire un état, un mot sur le ruban et une position de la tête) existentielle est acceptante s'il existe une configuration successeur acceptante ; une configuration universelle est acceptante si toutes les configurations successeurs sont acceptantes. Une machine accepte une entrée si la configuration initiale sur cette entrée est acceptante. Une machine de Turing alternante (à une bande) est une structure , où : est un ensemble fini d'états ; est lalphabet fini de la bande ; est la relation de transition ( et pour le déplacement à gauche respectivement à droite de la tête) ; est l'état initial ; spécifie le type de chaque état (existentiel ou universel).

Source officielle

https://fr.wikipedia.org/wiki/Machine_de_Turing_alternante

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Cours associés (2)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

COM-501: Advanced cryptography

This course reviews some failure cases in public-key cryptography. It introduces some cryptanalysis techniques. It also presents fundamentals in cryptography such as interactive proofs. Finally, it presents some techniques to validate the security of crypt ...

Séances de cours associées (1)

Étapes d'élimination des quantificateurs pour Presburger Arithmetic

Explore les étapes d'élimination des quantificateurs pour Presbourger Arithmetic, en mettant l'accent sur les techniques permettant de simplifier et d'éliminer efficacement les quantificateurs.

Publications associées (4)

On Induction for SMT Solvers

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas of interest in such cases. We present a set of techniques that introduce inductive reasoning into SMT solving algorithms that is sound with respect to the interpretation of structures in SMT-LIB standard. The techniques include inductive strengthening of c

2014

On Complete Reasoning about Axiomatic Specifications

Automated software verification tools typically accept specifications of functions in terms of pre- and postconditions. However, many properties of functional programs can be more naturally specified using a more general form of universally quantified properties. Such general specifications may relate multiple user-defined functions, and compare multiple invocations of a function on different arguments. We present new decision procedures for complete and terminating reasoning about such universally quantifi

2010

On Depth-bounded Message Passing Systems

We explore the border between decidability and undecidability of verification problems related to message passing systems that admit unbounded creation of threads and name mobility. Inspired by use cases in real-life programs we introduce the notion of depth-bounded message passing systems. A configuration of a message passing system can be represented as a graph. In a depth-bounded system the length of the longest acyclic path in each reachable configuration is bounded by a constant. While the general reac

2009

Afficher plus

Personnes associées (1)

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Source officielle

https://fr.wikipedia.org/wiki/Machine_de_Turing_alternante

À propos de ce résultat

Cours associés (2)

CS-550: Formal verification

COM-501: Advanced cryptography

Séances de cours associées (1)

Étapes d'élimination des quantificateurs pour Presburger Arithmetic

Explore les étapes d'élimination des quantificateurs pour Presbourger Arithmetic, en mettant l'accent sur les techniques permettant de simplifier et d'éliminer efficacement les quantificateurs.

Publications associées (4)

On Induction for SMT Solvers

2014

On Complete Reasoning about Axiomatic Specifications

2010

On Depth-bounded Message Passing Systems

2009

Afficher plus

Personnes associées (1)

Viktor Kuncak

Concepts associés (2)

Hiérarchie polynomiale

En théorie de la complexité, la hiérarchie polynomiale est une hiérarchie de classes de complexité qui étend la notion de classes P, NP, co-NP. La classe PH est l'union de toutes les classes de la hiérarchie polynomiale. Il existe plusieurs définitions équivalentes des classes de la hiérarchie polynomiale. On peut définir la hiérarchie à l'aide des quantificateurs universel () et existentiel ().

Problème SAT

vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité.

Notebooks associés (2)

Designing FIR Filters Using the Parks-McClellan Algorithm

The Parks-McClellan Filter Design Method[1]¶

                                      [2]Paolo Prandoni, [3]LCAV, EPFL

The Parks-McClellan (PM) algorithm is a clever application of advanced polynomial fitting techniques to the problem of FIR filter design. In this notebook we will explore the key ideas behind the method by considering the design of a simple Type-I lowpass filter. NOTE: This notebook uses interactive widgets. If the interactive controls do not work or show up, please fo

Exploring Quantization and Oversampling through One-Bit Music

One-Bit Music[1]¶ In this notebook we will talk about quantization and oversampling and we will do so by taking a trip down memory lane to revisit the early from monophonic square waves, introduce polyphony by way of pulse-width modulation and finish with the basics of sigma-delta quantization. pacman In [1]: import matplotlib import matplotlib.pyplot as plt import numpy as np import scipy.signal as sp from scipy.io import wavfile import IPython In [2]: import sys ! wget -q -O mus