# Sistema de Transição

Na teoria da ciência da computação, um sistema de transição é um conceito utilizado no estudo da computação. É usado para descrever o comportamento potencial de sistemas discretos. Consiste de estados e transições entre estados, que podem ser rotuladas com etiquetas escolhidas a partir de um conjunto; o mesmo rótulo pode aparecer em mais de uma transição. Se o conjunto de rótulos é um conjunto unitário, o sistema é essencialmente sem rótulo, e uma definição mais simples que omite os rótulos é possível.
Sistemas de transição coincidem matematicamente com sistemas de reescrita abstratos (como explicado mais adiante neste artigo) e grafos direcionados. Eles diferem de autômatos finitos em várias maneiras:
* O conjunto de estados não é necessariamente finito, ou mesmo contável.
* O conjunto de transições não é necessariamente finito, ou mesmo contável.
* Nenhum estado "inicio" ou estado "final" são dadas.
Sistemas de transição podem ser representados como grafos direcionados.

## Definição Formal

Formalmente, um sistema de transição é um par (S, →), onde S é um conjunto de estados e → é um conjunto de transições entre estados (i.e. um subconjunto de S × S). O fato de que há uma transição do estado p para o estado q, i.e. (p, q) ∈ →, é escrito como p → q.
Um sistema de transição rotulado é uma tupla (S, Λ, →), onde S é um conjunto de estados, Λ é um conjunto de rótulos e → é um conjunto de transições rotuladas (i.é., um subconjunto de S × Λ × S). O fato de que (p,α,q) ∈ → é escrito como
    $p{\overset {\alpha }{\rightarrow }}q.\,$
Isto representa o fato de que existe uma transição do estado p para o estado q com rótulo α. Rótulos podem representar coisas diferentes dependendo da linguagem de interesse. Usos típicos dos rótulos incluem a representação de entrada esperada, as condições que devem ser verdadeiras para disparar a transição, ou ações realizadas durante a transição. Sistemas de transição rotulada foram originalmente introduzidos como sistemas de transição nomeadas.
Se, para qualquer p e α, existe apenas uma única tupla (p,α,q) em →, então, diz-se que α é determinística (para p). Se, para qualquer p e α, existe pelo menos uma tupla (p,α,q) em →, então, diz-se que α é executável (p).

## Relação entre sistemas de transição não rotulados e rotulados

Existem muitas relações entre esses conceitos. Algumas são simples, tais como a observação que um sistema de transição rotulado onde o conjunto de rótulos consiste de apenas um elemento é equivalente a um sistema de transição não rotulado. No entanto, nem todas estas relações são igualmente triviais.

## Comparação com sistemas de reescrita abstratos

Como um objecto matemático, um sistema de transição não rotulado é idêntico a um sistema de reescrita abstrato (não indexado). Se considerarmos a relação de reescrita como um conjunto indexado de relações, como alguns autores fazem, então, um sistema de transição rotulado é equivalente a um sistema de reescrita abstrato com os índices sendo os rótulos. O foco do estudo e a terminologia são diferentes. Entretanto, em um sistema de transição estamos interessados em interpretar os rótulos como ações, enquanto que em um sistema de reescrita abstrato o foco é em como os objetos podem ser transformados (reescritos) em outros.

## Extensões

Em verificação de modelos , um sistema de transição é, às vezes, definido para incluir uma função de rotulagem adicional para os estados, assim, resultando em uma noção que envolve a estrutura de Kripke.
Linguagens de ação são um caso especial de sistemas de transação, adicionando um conjunto de fluentes F, um conjunto de valores V, e uma função que mapeia F × S para V.

## Veja também

* Simulação de preorder
* Bisimulation
* Operacional semântica
* Estrutura de Kripke
* Máquina De Estado

## References

* ↑ Robert M. Keller (July 1976) "Formal Verification of Parallel Programs", Communications of the ACM, vol 19, nr 7, p. 371-384.
* ↑ Marc Bezem, J. W. Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003, ISBN 0-521-39115-6. p. 7-8
* ↑ Christel Baier; Joost-Pieter Katoen. Principles of model checking. [S.l.]: The MIT Press. p. 20. ISBN 978-0-262-02649-9
* ↑ Micheal Gelfond, Vladimir Lifschitz (1998) "Action Languages", Linköping Electronic Articles in Computer and Information Science, vol 3, nr 16.