Transitionssystem

Transitionssystem

Ein Transitionssystem (engl. transition system) beschreibt in der Automatentheorie die möglichen Zustände eines zustandsbasierten Systems und die möglichen Übergänge (Transitionen) zwischen diesen Zuständen.

Man unterscheidet dabei diskrete und kontinuierliche Systeme. In der Regel betrachtet man nur diskrete Systeme, da diese wesentlich leichter überprüft werden können.

Ferner unterscheidet man deterministische und nichtdeterministische Transitionssysteme. Im ersten Fall wird einem Zustand und einer Transition höchstens ein Folgezustand zugeordnet, während im nichtdeterministischen Fall derselbe Zustand zu einer Transition mehrere Nachfolgezustände besitzen kann. Deterministische Transitionssysteme sind in diesem Sinne Spezialfälle von nichtdeterministischen Transitionssystemen.

Ein Transitionssystem kann verwendet werden, um bestimmte Eigenschaften eines zustandsbasierten Systems zu zeigen, insbesondere die Terminiertheit. Aus diesem Grund wird es zur Verifikation der Korrektheit von Algorithmen eingesetzt. Auch zum Beweis der Verklemmungsfreiheit von verteilten Systemen kann dieses Konstrukt angewendet werden.

Inhaltsverzeichnis

Formale Definition

Formal wird ein diskretes Transitionssystem beschrieben durch ein Quadrupel TS = (S,S0,A,T), wobei

  • S ist eine Menge von Zuständen.
  • S_0 \subseteq S ist eine nichtleere Menge von Startzuständen.
  • A ist ein endliches Alphabet wobei S \cap A = \emptyset. Die Elemente von A heißen Markierungen (engl. label) von TS.
  • T \subseteq S \times A \times S ist die Transitionsrelation von TS, die für jeden Zustand und jedes Eingabezeichen bestimmt, welche Nachfolgezustände existieren.

Das Transitionssystem entspricht also einem endlichen Automaten, nur dass die Zustandsmenge nicht endlich sein muss und die Transitionsrelation daher beliebig komplex sein kann. Schon diese scheinbar kleinen Erweiterungen führen dazu, dass Transitionssysteme im Allgemeinen turingmächtig sind.

Ein Transitionssystem heißt deterministisch, wenn die folgenden beiden Bedingungen erfüllt sind:

  • S0 enthält genau ein Element.
  • Wenn (z_0,a,z_1) \in T, dann folgt für alle (w_0,b,w_1) \in T mit w0 = z0 und b = a auch w1 = z1.

In jedem Zustand ist also für jedes Eingabezeichen eindeutig festgelegt, was der nächste Zustand sein muss.

Eigenschaften

Ein Transitionssystem heißt endlich, falls die Menge der Zustände S endlich ist. Ein endliches Transitionssystem ist ein endlicher Automat. Solche Transitionssysteme können als Transitionsdiagramm dargestellt werden: Es bildet im Allgemeinen einen gerichteten zyklischen Graphen mit benannten Kanten.

Mit (zumeist) endlichen Graphen beschäftigt sich ein ganzer Zweig der Theoretischen Informatik, die sogenannte Modellprüfung (model checking). Ziel ist es, dass durch eine Sprache (zum Beispiel Guarded Commands, Petri-Netze) definierte Transitionssystem automatisch daraufhin zu überprüfen, ob es eine Spezifikation erfüllt, die ebenfalls in einer geeigneten Sprache (meist einer Temporalen Logik, wie LTL, CTL oder CTL*) gegeben ist.

Beispiele

Ampel

Eine Ampel lässt sich als Transitionssystem verstehen. Eine Ampel besitzt die fünf Zustände {rot,rotgelb,gruen,gelb,aus}. Im Normalbetrieb wechselt die Ampel ihre Zustände in folgender Reihenfolge: rot \ \overrightarrow { a } \ rot-gelb \ \overrightarrow { a } \ gruen \ \overrightarrow { a } \ gelb \ \overrightarrow { a } \ rot. Außerdem besitzt eine Ampel einen Nachtbetrieb:gelb \ \overrightarrow { b } \ aus \ \overrightarrow { b } \ gelb. Die Beschreibung dieser beiden Zyklen als Zustandsänderung nennt man Transitionssystem.

Deterministischer endlicher Automat

Beispiel eines deterministischen endlichen Automaten

Der oben abgebildete Graph ist ein DEA mit den drei Zuständen S0, S1 und S2. Der Zustand S1 ist ein Endzustand. Das Alphabet besteht aus den beiden Buchstaben a und b. Andere Buchstaben akzeptiert der Automat nicht. Der reguläre Ausdruck a * b(a + b | b + a) * entspricht der Sprache, die dieser DEA akzeptiert.

Literatur


Wikimedia Foundation.

Игры ⚽ Нужно сделать НИР?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Bisimulation — In der theoretischen Informatik ist eine Bisimulation eine Relation zwischen den Zuständen eines Transitionssystems, die solche Zustände miteinander in Beziehung setzt, die sich gleich verhalten. Das bedeutet, dass der eine Zustand die Übergänge… …   Deutsch Wikipedia

  • Modelchecking — Model Checking (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für …   Deutsch Wikipedia

  • Modellprüfer — Model Checking (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für …   Deutsch Wikipedia

  • Modellprüfung — Model Checking (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für …   Deutsch Wikipedia

  • Modellprüfverfahren — Model Checking (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für …   Deutsch Wikipedia

  • Ableitungsrelation — Eine Transitionsrelation ist in der Informatik eine Abbildung, die einen Zustand z auf einen Folgezustand z abbildet. Die Transitionsrelation bildet zusammen mit einer Zustandsmenge ein Transitionssystem, das das Verhalten eines Automaten… …   Deutsch Wikipedia

  • Model Checking — (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für eine gegebene… …   Deutsch Wikipedia

  • Reduktionssystem — In der Mathematischen Logik und der Theoretischen Informatik steht die Bezeichnung Reduktionssystem, oder abstraktes Reduktionssystem, abgekürzt ARS, für eine Verallgemeinerung von Termersetzungssystemen. In seiner einfachsten Form ist ein ARS… …   Deutsch Wikipedia

  • Abstrakte Maschine — Ein Automat oder eine abstrakte Maschine ist in der Informatik das Modell eines digitalen, zeitdiskreten Rechners. Ob es möglich oder sinnvoll ist, eine solche Maschine tatsächlich zu bauen, ist dabei zunächst unerheblich. Die Vereinfachung der… …   Deutsch Wikipedia

  • Abstrakter Automat — Ein Automat oder eine abstrakte Maschine ist in der Informatik das Modell eines digitalen, zeitdiskreten Rechners. Ob es möglich oder sinnvoll ist, eine solche Maschine tatsächlich zu bauen, ist dabei zunächst unerheblich. Die Vereinfachung der… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”