X-machine
Encyclopedia
The X-machine is a theoretical model of computation
introduced by Samuel Eilenberg
in 1974.
Automata, Languages and Machines, Vol. A.
Academic Press, London.
The X in "X-machine" represents the fundamental data type on which the machine operates; for example, a machine that operates on databases (objects of type database) would be a database-machine. The X-machine model is structurally the same as the finite state machine
, except that the symbols used to label the machine's transitions denote relations
of type X→X. Crossing a transition is equivalent to applying the relation that labels it (computing a set of changes to the data type X), and traversing a path in the machine corresponds to applying all the associated relations, one after the other.
, for example), which admitted deterministic, non-deterministic and non-terminating computations. His seminal work published many variants of the basic X-machine model, each of which generalized the finite state machine
in a slightly different way.
In the most general model, an X-machine is essentially a "machine for manipulating objects of type X". Suppose that X is some datatype, called the fundamental datatype, and that Φ is a set of (partial) relations φ: X → X. An X-machine is a finite state machine
whose arrows are labelled by relations in Φ. In any given state, one or more transitions may be enabled if the domain
of the associated relation φi accepts (a subset of) the current values stored in X. In each cycle, all enabled transitions are assumed to be taken. Each recognised path through the machine generates a list φ1 ... φn of relations. We call the composition φ1 o ... o φn of these relations the path relation corresponding to that path. The behaviour of the X-machine is defined to be the union of all the behaviours computed by its path relations. In general, this is non-deterministic, since applying any relation computes a set of outcomes on X. In the formal model, all possible outcomes are considered together, in parallel.
For practical purposes, an X-machine should describe some finite computation. An encoding function α: Y → X converts from some input data type Y into the initial state of X, and a decoding function β: X → Z, converts back from the final state(s) of X into some output data type Z. Once the initial state of X is populated, the X-machine runs to completion, and the outputs are then observed. In general, a machine may deadlock (be blocked), or livelock (never halt), or perform one or more complete computations. For this reason, more recent research has focused on deterministic X-machines, whose behaviour can be controlled and observed more precisely.
FindIncrements →DoIncrement FindIncrements
FindIncrements →SkipIncrement FindSubExprs
FindSubExprs →DoSubExpr FindSubExprs
FindSubExprs →SkipSubExpr Completed
The relation DoIncrement maps a parsed subtree corresponding to "x := x + 1" into the optimized subtree "++x". The relation DoSubExpr maps a parse tree containing multiple occurrences of the same expression "x + y ... x + y" into an optimized version with a local variable to store the repeated computation "z := x + y; ... z ... z". These relations are only enabled if X contains the domain values (subtrees) on which they operate. The remaining relations SkipIncrement and SkipSubExpr are nullops (identity relations) enabled in the complementary cases.
So, the Optimizer-machine will run to completion, first converting trivial additions into in-place increments (while in the FindIncrements state), then it will move on to the FindSubExprs state and perform a series of common sub-expression removals, after which it will move to the final state Completed. The decoding function β will then map from the memory-type X (the optimized parse-tree) into the output-type Z (optimized machine code).
'X-machines as a basis for dynamic system specification',
Software Engineering Journal 3(2), pp. 69-76. who noticed that the model was ideal for software formal specification
purposes, because it cleanly separates control flow from processing. Provided one works at a sufficiently abstract level, the control flows in a computation can usually be represented as a finite state machine, so to complete the X-machine specification all that remains is to specify the processing associated with each of the machine's transitions. The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,
'Formal methods in the specification of the human-machine interface',
International J. Command and Control, Communications and Info. Systems. 2, pp. 24-34.
his modelling of processes in cell biochemistry,
'Mathematical models of cell biochemistry'.
Technical Report CS-86-4, Dept of Computer Science, Sheffield University.
and Stannett's modelling of decision-making in military command systems.
'An organisational approach to decision-making in command systems.'
International J. Command and Control, Communications and Info. Systems. 1, pp. 23-34.
was found to serve as the basis for specifying large software systems that are completely testable.
Correct Systems - Building a Business Process Solution.
Springer, Applied Computing Series. Another variant,
the Communicating Stream X-Machine
offers a useful testable model for biological processes
and future swarm-based satellite systems.
M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005)
'Requirements of an Integrated Formal Method for Intelligent Swarms',
in Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal.
Association for Computing Machinery, pp. 125-133.
by Andras Kornai
, who models word meaning by `pointed' machines that have one member of the base set X distinguished.
. NASA
has recently discussed using a combination of Communicating Stream X-Machines
and the process calculus WSCSS in the design and testing of swarm satellite systems.
'X-machines and the Halting Problem: Building a super-Turing machine'.
Formal Aspects of Computing 2, pp. 331-41.
it is consequently related to work in hypercomputation
theory.
'Hypercomputation'.
Minds and Machines 12, pp. 461-502.
(SXM) model,
which forms the basis for Mike Holcombe and Florentin Ipate's theory of complete software testing, which guarantees known correctness properties, once testing is over. The Stream X-Machine differs from Eilenberg's original model, in that the fundamental data type X = Out* × Mem × In*, where In* is an input sequence, Out* is an output sequence, and Mem is the (rest of the) memory.
The advantage of this model is that it allows a system to be driven, one step at a time, through its states and transitions, while observing the outputs at each step. These are witness values, that guarantee that particular functions were executed on each step. As a result, complex software systems may be decomposed into a hierarchy of Stream X-Machines, designed in a top-down way and tested in a bottom-up way. This divide-and-conquer approach to design and testing is backed by Florentin Ipate's proof of correct integration, which proves how testing the layered machines independently is equivalent to testing the composed system.
COMX: A methodology for the formal design of computer systems using Communicating X-machines.
PhD Thesis, Staffordshire University.
in which machines are connected via named communication channels (known as ports); this model exists in both discrete- and real-timed variants.
'On Making a Crossing Safe',
Technical Report SOCTR/97/01, School of Computing, Staffordshire University.
(Citeseer)
Earlier versions of this work were not fully formal and did not show full input/output relations.
A similar Communicating X-Machine approach using buffered
channels was developed by Petros Kefalas. The focus of this work was on expressiveness in the composition of components. The ability to reassign channels meant that some of the testing theorems from Stream X-Machines did not carry over.
These variants are discussed in more detail
on a separate page.
'Modelling logic programming using a network of communicating machines', in
Proc. 2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26–28 January 1994, pp. 156-161.
Abstract In Vertan's model, the machines communicate indirectly, via a shared communication matrix (essentially an array of pigeonholes), rather than directly via shared channels.
Bălănescu, Cowling, Georgescu, Vertan and others have studied the formal properties of this CSXM model in some detail. Full input/output relations can be shown. The communication matrix establishes a protocol for synchronous communication. The advantage of this is that it decouples each machine's processing from their communication, allowing the separate testing of each behaviour. This compositional model was proven equivalent to a standard Stream X-Machine
, so leveraging the earlier testing theory developed by Holcombe and Ipate.
This X-machine variant is discussed in more detail
on a separate page.
approach, in that the monolithic data type X is distributed over, and encapsulated by, several objects, which are serially composed; and systems are driven by method invocations and returns, rather than by inputs and outputs.
Further work in this area concerned adapting the formal testing theory in the context of inheritance, which partitions the state-space of the superclass in extended subclass objects.
A "CCS-augmented X-machine" (CCSXM) model was later developed by Simons and Stannett in 2002 to support complete behavioural testing of object-oriented systems, in the presence of asynchronous communication
'CCS-Augmented X-Machines',
Technical Report CS-2002-04, Department of Computer Science, Sheffield University, UK. This is expected to bear some similarity with NASA
's recent proposal; but no definitive comparison of the two models has as yet been conducted.
Computation
Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...
introduced by Samuel Eilenberg
Samuel Eilenberg
Samuel Eilenberg was a Polish and American mathematician of Jewish descent. He was born in Warsaw, Russian Empire and died in New York City, USA, where he had spent much of his career as a professor at Columbia University.He earned his Ph.D. from University of Warsaw in 1936. His thesis advisor...
in 1974.
Automata, Languages and Machines, Vol. A.
Academic Press, London.
The X in "X-machine" represents the fundamental data type on which the machine operates; for example, a machine that operates on databases (objects of type database) would be a database-machine. The X-machine model is structurally the same as the finite state machine
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
, except that the symbols used to label the machine's transitions denote relations
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
of type X→X. Crossing a transition is equivalent to applying the relation that labels it (computing a set of changes to the data type X), and traversing a path in the machine corresponds to applying all the associated relations, one after the other.
Original theory
Eilenberg's original X-machine was a completely general theoretical model of computation (subsuming the Turing machineTuring machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
, for example), which admitted deterministic, non-deterministic and non-terminating computations. His seminal work published many variants of the basic X-machine model, each of which generalized the finite state machine
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
in a slightly different way.
In the most general model, an X-machine is essentially a "machine for manipulating objects of type X". Suppose that X is some datatype, called the fundamental datatype, and that Φ is a set of (partial) relations φ: X → X. An X-machine is a finite state machine
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
whose arrows are labelled by relations in Φ. In any given state, one or more transitions may be enabled if the domain
Domain (mathematics)
In mathematics, the domain of definition or simply the domain of a function is the set of "input" or argument values for which the function is defined...
of the associated relation φi accepts (a subset of) the current values stored in X. In each cycle, all enabled transitions are assumed to be taken. Each recognised path through the machine generates a list φ1 ... φn of relations. We call the composition φ1 o ... o φn of these relations the path relation corresponding to that path. The behaviour of the X-machine is defined to be the union of all the behaviours computed by its path relations. In general, this is non-deterministic, since applying any relation computes a set of outcomes on X. In the formal model, all possible outcomes are considered together, in parallel.
For practical purposes, an X-machine should describe some finite computation. An encoding function α: Y → X converts from some input data type Y into the initial state of X, and a decoding function β: X → Z, converts back from the final state(s) of X into some output data type Z. Once the initial state of X is populated, the X-machine runs to completion, and the outputs are then observed. In general, a machine may deadlock (be blocked), or livelock (never halt), or perform one or more complete computations. For this reason, more recent research has focused on deterministic X-machines, whose behaviour can be controlled and observed more precisely.
Example
A compiler with a peep-hole optimizer can be thought of as a machine for optimizing program structure. In this Optimizer-machine, the encoding function α takes source code from the input-type Y (the program source) and loads it into the memory-type X (a parse tree). Suppose that the machine has several states, called FindIncrements, FindSubExprs and Completed. The machine starts in the initial state FindIncrements, which is linked to other states via the transitions:FindIncrements →DoIncrement FindIncrements
FindIncrements →SkipIncrement FindSubExprs
FindSubExprs →DoSubExpr FindSubExprs
FindSubExprs →SkipSubExpr Completed
The relation DoIncrement maps a parsed subtree corresponding to "x := x + 1" into the optimized subtree "++x". The relation DoSubExpr maps a parse tree containing multiple occurrences of the same expression "x + y ... x + y" into an optimized version with a local variable to store the repeated computation "z := x + y; ... z ... z". These relations are only enabled if X contains the domain values (subtrees) on which they operate. The remaining relations SkipIncrement and SkipSubExpr are nullops (identity relations) enabled in the complementary cases.
So, the Optimizer-machine will run to completion, first converting trivial additions into in-place increments (while in the FindIncrements state), then it will move on to the FindSubExprs state and perform a series of common sub-expression removals, after which it will move to the final state Completed. The decoding function β will then map from the memory-type X (the optimized parse-tree) into the output-type Z (optimized machine code).
Convention
When referring to Eilenberg's original model, "X-machine" is typically written with a lower-case "m", because the sense is "any machine for processing X". When referring to later specific models, the convention is to use a capital "M" as part of the proper name of that variant.1980s
Interest in the X-machine was revived in the late 1980s by Mike Holcombe,'X-machines as a basis for dynamic system specification',
Software Engineering Journal 3(2), pp. 69-76. who noticed that the model was ideal for software formal specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
purposes, because it cleanly separates control flow from processing. Provided one works at a sufficiently abstract level, the control flows in a computation can usually be represented as a finite state machine, so to complete the X-machine specification all that remains is to specify the processing associated with each of the machine's transitions. The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,
'Formal methods in the specification of the human-machine interface',
International J. Command and Control, Communications and Info. Systems. 2, pp. 24-34.
his modelling of processes in cell biochemistry,
'Mathematical models of cell biochemistry'.
Technical Report CS-86-4, Dept of Computer Science, Sheffield University.
and Stannett's modelling of decision-making in military command systems.
'An organisational approach to decision-making in command systems.'
International J. Command and Control, Communications and Info. Systems. 1, pp. 23-34.
1990s
X-machines have received renewed attention since the mid-1990s, when Gilbert Laycock's deterministic Stream X-MachineStream X-Machine
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.Gilbert Laycock...
was found to serve as the basis for specifying large software systems that are completely testable.
Correct Systems - Building a Business Process Solution.
Springer, Applied Computing Series. Another variant,
the Communicating Stream X-Machine
Communicating X-Machine
The Communicating X-Machine is a model of computation introduced by various researchers in the 1990s to model systems composed of communicating agents. The model exists in several variants, which are either based directly on Samuel Eilenberg's X-machine or on Gilbert Laycock's later Stream...
offers a useful testable model for biological processes
and future swarm-based satellite systems.
M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005)
'Requirements of an Integrated Formal Method for Intelligent Swarms',
in Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal.
Association for Computing Machinery, pp. 125-133.
2000s
X-machines have been applied to lexical semanticsLexical semantics
Lexical semantics is a subfield of linguistic semantics. It is the study of how and what the words of a language denote . Words may either be taken to denote things in the world, or concepts, depending on the particular approach to lexical semantics.The units of meaning in lexical semantics are...
by Andras Kornai
Andras Kornai
András Kornai is a well-known mathematical linguist. He earned his mathematics PhD in 1983 from Eötvös Loránd University, Budapest where his advisor was Miklós Ajtai...
, who models word meaning by `pointed' machines that have one member of the base set X distinguished.
Major variants
The X-machine is rarely encountered in its original form, but underpins several subsequent models of computation. The most influential model on theories of software testing has been the Stream X-MachineStream X-Machine
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.Gilbert Laycock...
. NASA
NASA
The National Aeronautics and Space Administration is the agency of the United States government that is responsible for the nation's civilian space program and for aeronautics and aerospace research...
has recently discussed using a combination of Communicating Stream X-Machines
Communicating X-Machine
The Communicating X-Machine is a model of computation introduced by various researchers in the 1990s to model systems composed of communicating agents. The model exists in several variants, which are either based directly on Samuel Eilenberg's X-machine or on Gilbert Laycock's later Stream...
and the process calculus WSCSS in the design and testing of swarm satellite systems.
Analog X Machine (AXM)
The earliest variant, the continuous-time Analog X-Machine (AXM), was introduced by Mike Stannett in 1990 as a potentially "super-Turing" model of computation;'X-machines and the Halting Problem: Building a super-Turing machine'.
Formal Aspects of Computing 2, pp. 331-41.
it is consequently related to work in hypercomputation
Hypercomputation
Hypercomputation or super-Turing computation refers to models of computation that are more powerful than, or are incomparable with, Turing computability. This includes various hypothetical methods for the computation of non-Turing-computable functions, following super-recursive algorithms...
theory.
'Hypercomputation'.
Minds and Machines 12, pp. 461-502.
Stream X-Machine (SXM)
The most commonly encountered X-machine variant is Gilbert Laycock's 1993 Stream X-MachineStream X-Machine
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.Gilbert Laycock...
(SXM) model,
which forms the basis for Mike Holcombe and Florentin Ipate's theory of complete software testing, which guarantees known correctness properties, once testing is over. The Stream X-Machine differs from Eilenberg's original model, in that the fundamental data type X = Out* × Mem × In*, where In* is an input sequence, Out* is an output sequence, and Mem is the (rest of the) memory.
The advantage of this model is that it allows a system to be driven, one step at a time, through its states and transitions, while observing the outputs at each step. These are witness values, that guarantee that particular functions were executed on each step. As a result, complex software systems may be decomposed into a hierarchy of Stream X-Machines, designed in a top-down way and tested in a bottom-up way. This divide-and-conquer approach to design and testing is backed by Florentin Ipate's proof of correct integration, which proves how testing the layered machines independently is equivalent to testing the composed system.
Communicating X-Machine (CXM)
The earliest proposal for connecting several X-machines in parallel is Judith Barnard's 1995 Communicating X-machine (CXM or COMX) model,COMX: A methodology for the formal design of computer systems using Communicating X-machines.
PhD Thesis, Staffordshire University.
in which machines are connected via named communication channels (known as ports); this model exists in both discrete- and real-timed variants.
'On Making a Crossing Safe',
Technical Report SOCTR/97/01, School of Computing, Staffordshire University.
(Citeseer)
Earlier versions of this work were not fully formal and did not show full input/output relations.
A similar Communicating X-Machine approach using buffered
channels was developed by Petros Kefalas. The focus of this work was on expressiveness in the composition of components. The ability to reassign channels meant that some of the testing theorems from Stream X-Machines did not carry over.
These variants are discussed in more detail
Communicating X-Machine
The Communicating X-Machine is a model of computation introduced by various researchers in the 1990s to model systems composed of communicating agents. The model exists in several variants, which are either based directly on Samuel Eilenberg's X-machine or on Gilbert Laycock's later Stream...
on a separate page.
Communicating Stream X-Machine (CSXM)
The first fully formal model of concurrent X-machine composition was proposed in 1999 by Cristina Vertan and Horia Georgescu, based on earlier work on communicating automatata by Philip Bird and Anthony Cowling.'Modelling logic programming using a network of communicating machines', in
Proc. 2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26–28 January 1994, pp. 156-161.
Abstract In Vertan's model, the machines communicate indirectly, via a shared communication matrix (essentially an array of pigeonholes), rather than directly via shared channels.
Bălănescu, Cowling, Georgescu, Vertan and others have studied the formal properties of this CSXM model in some detail. Full input/output relations can be shown. The communication matrix establishes a protocol for synchronous communication. The advantage of this is that it decouples each machine's processing from their communication, allowing the separate testing of each behaviour. This compositional model was proven equivalent to a standard Stream X-Machine
Stream X-Machine
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.Gilbert Laycock...
, so leveraging the earlier testing theory developed by Holcombe and Ipate.
This X-machine variant is discussed in more detail
Communicating X-Machine
The Communicating X-Machine is a model of computation introduced by various researchers in the 1990s to model systems composed of communicating agents. The model exists in several variants, which are either based directly on Samuel Eilenberg's X-machine or on Gilbert Laycock's later Stream...
on a separate page.
Object X-Machine (OXM)
Kirill Bogdanov and Anthony Simons developed several variants of the X-machine to model the behaviour of objects in object-oriented systems. This model differs from the Stream X-MachineStream X-Machine
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.Gilbert Laycock...
approach, in that the monolithic data type X is distributed over, and encapsulated by, several objects, which are serially composed; and systems are driven by method invocations and returns, rather than by inputs and outputs.
Further work in this area concerned adapting the formal testing theory in the context of inheritance, which partitions the state-space of the superclass in extended subclass objects.
A "CCS-augmented X-machine" (CCSXM) model was later developed by Simons and Stannett in 2002 to support complete behavioural testing of object-oriented systems, in the presence of asynchronous communication
'CCS-Augmented X-Machines',
Technical Report CS-2002-04, Department of Computer Science, Sheffield University, UK. This is expected to bear some similarity with NASA
NASA
The National Aeronautics and Space Administration is the agency of the United States government that is responsible for the nation's civilian space program and for aeronautics and aerospace research...
's recent proposal; but no definitive comparison of the two models has as yet been conducted.
Downloadable technical reports
- M. Stannett and A. J. H. Simons (2002) Complete Behavioural Testing of Object-Oriented Systems using CCS-Augmented X-Machines. Tech Report CS-02-06, Dept of Computer Science, University of Sheffield. Download
- J. Aguado and A. J. Cowling (2002) Foundations of the X-machine Theory for Testing. Tech Report CS-02-06, Dept of Computer Science, University of Sheffield. Download
- J. Aguado and A. J. Cowling (2002) Systems of Communicating X-machines for Specifying Distributed Systems. Tech Report CS-02-07, Dept of Computer Science, University of Sheffield. Download
- M. Stannett (2005) The Theory of X-Machines - Part 1. Tech Report CS-05-09, Dept of Computer Science, University of Sheffield. Download
External links
- http://www.dcs.shef.ac.uk/~ajc/csxms/index.html - Tony Cowling's Communicating SXM Systems pages
- http://x-machines.com - Mike Stannett's Theory of X-Machines site