imported>Girus: Komma

2021-09-05T09:14:35Z

Komma

Neue Seite

Ein '''Transitionssystem''' (englisch ''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 [[Diskretheit|diskrete]] und [[Kontinuität (Philosophie)|kontinuierliche]] Systeme. In der Regel betrachtet man nur diskrete Systeme, da diese wesentlich leichter überprüft werden können.

Ferner unterscheidet man [[Determinismus (Algorithmus)|deterministische]] und [[Nichtdeterminismus|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 (Informatik)|Korrektheit]] von [[Algorithmus|Algorithmen]] eingesetzt. Auch zum Beweis der [[Verklemmung]]sfreiheit von [[Verteiltes System|verteilten Systemen]] kann dieses Konstrukt angewendet werden.

== Formale Definition ==
Formal wird ein diskretes Transitionssystem beschrieben durch ein [[Tupel|Quadrupel]] <math>TS = (S,S_0,A,T)</math>, wobei

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

Das Transitionssystem entspricht also einem [[Endlicher Automat|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 [[Turing-Vollständigkeit|turingmächtig]] sind.

Ein Transitionssystem heißt [[Determinismus (Algorithmus)|deterministisch]], wenn die folgenden beiden Bedingungen erfüllt sind:

* <math>S_0</math> enthält genau ein Element.
* Wenn <math>(z_0,a,z_1) \in T</math>, dann folgt für alle <math>(w_0,b,w_1) \in T</math> mit <math>w_0 = z_0</math> und <math>b = a</math> auch <math>w_1 = z_1</math>.

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 <math>S</math> endlich ist. Ein endliches Transitionssystem ist ein endlicher Automat. Solche Transitionssysteme können als ''Transitionsdiagramm'' dargestellt werden: Es bildet im Allgemeinen einen [[Graph (Graphentheorie)#Teilgraphen, Wege und Zyklen|gerichteten zyklischen Graphen]] mit benannten Kanten.

Mit (zumeist) endlichen Graphen beschäftigt sich ein ganzer Zweig der [[Theoretische Informatik|Theoretischen Informatik]], die sogenannte [[Modellprüfung]] (''model checking''). Ziel ist es, das in einer Sprache (zum Beispiel [[Guarded Command]]s, [[Petri-Netz]]e) definierte Transitionssystem automatisch daraufhin zu überprüfen, ob es eine Spezifikation erfüllt, die ebenfalls in einer geeigneten Sprache (meist einer [[Temporale Logik|Temporalen Logik]], wie [[Linear Time Temporal Logic|LTL]], [[Computation Tree Logic|CTL]] oder [[CTL*]]) gegeben ist.

== Beispiele ==
=== Ampel ===

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

== Deterministischer endlicher Automat ==

[[Datei:Dea01.png|Beispiel eines deterministischen endlichen Automaten]]

Der oben abgebildete Graph ist ein [[Deterministischer endlicher Automat|DEA]] mit den drei Zuständen <math>S_0</math>, <math>S_1</math> und <math>S_2</math>. Der Zustand <math>S_1</math> ist ein Endzustand. Das Alphabet besteht aus den beiden Buchstaben <math>a</math> und <math>b</math>. Andere Buchstaben akzeptiert der Automat nicht. Der [[Regulärer Ausdruck|reguläre Ausdruck]] <math>a^*b(a^+b|b^+a)^*</math> entspricht der Sprache, die dieser DEA akzeptiert.

== Literatur ==

* {{BibISBN|389319181X}}
* Peter Sander, Wolffried Stucky, Rudolf Herschel: ''Automaten, Sprachen, Berechenbarkeit'', ISBN 3-519-02937-5

{{Normdaten|TYP=s|GND=4329099-1}}

[[Kategorie:Automatentheorie]]

Transitionssystem - Versionsgeschichte

imported>Girus: Komma