World Library  
Flag as Inappropriate
Email this Article

Transition system

Article Id: WHEBN0010768144
Reproduction Date:

Title: Transition system  
Author: World Heritage Encyclopedia
Language: English
Subject: Finite-state machine, Stutter bisimulation, Well-structured transition system, Computation tree logic, Frame problem
Collection: Models of Computation
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Transition system

In theoretical computer science, a transition system' is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.

Transition systems coincide mathematically with abstract rewriting systems (as explained further in this article). They differ from finite state automata in several ways:

  • The set of states is not necessarily finite, or even countable.
  • The set of transitions is not necessarily finite, or even countable.
  • No "start" state or "final" states are given.

Transition systems can be represented as directed graphs.

Contents

  • Formal definition 1
  • Relation between labelled and unlabelled transition systems. 2
  • Comparison with abstract rewriting systems 3
  • Extensions 4
  • See also 5
  • References 6

Formal definition

Formally, a transition system is a pair (S, →) where S is a set of states and → is a set of state transitions (i.e., a subset of S × S). The fact that there is a transition from state p to state q, i.e. (p, q) ∈ →, is written as pq.

A labelled transition system is a tuple (S, Λ, →) where S is a set of states, Λ is a set of labels and → is a set of of labelled transitions (i.e., a subset of S × Λ × S). The fact that (p,α,q) ∈ → is written as

p \overset{\alpha}{\rightarrow} q. \,

This represents the fact that there is a transition from state p to state q with label α. Labels can represent different things depending on the language of interest. Typical uses of labels include representing input expected, conditions that must be true to trigger the transition, or actions performed during the transition.

If, for any given p and α, there exists only a single tuple (p,α,q) in →, then one says that α is deterministic (for p). If, for any given p and α, there exists at least one tuple (p,α,q) in →, then one says that α is executable (for p).

Relation between labelled and unlabelled transition systems.

There are many relations between these concepts. Some are simple, such as observing that a labelled transition system where the set of labels consists of only one element is equivalent to an unlabelled transition system. However not all these relations are equally trivial.

Comparison with abstract rewriting systems

As a mathematical object, an unlabeled transition system is identical with an (unindexed) abstract rewriting system. If we consider the rewriting relation as an indexed set of relations, as some authors do, then a labeled transition system is equivalent to an abstract rewriting system with the indices being the labels. The focus of the study and the terminology are different however. In a transition system one is interested in interpreting the labels as actions, whereas in an abstract rewriting system the focus is on how objects may be transformed (rewritten) into others.[1]

Extensions

In model checking, a transition system is sometimes defined to include an additional labeling function for the states as well, resulting in a notion that encompasses that of Kripke structure.[2]

Action languages are a special case of transition systems, adding a set of fluents F, a set of values V, and a function that maps F × S to V.[3]

See also

References

  1. ^ Marc Bezem, J. W. Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003, ISBN 0-521-39115-6. p. 7-8
  2. ^ Christel Baier; Joost-Pieter Katoen. Principles of model checking. The MIT Press. p. 20.  
  3. ^ Micheal Gelfond, Vladimir Lifschitz (1998) "Action Languages", Linköping Electronic Articles in Computer and Information Science, vol 3, nr 16.
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.