Method of reducing finite controlling automata and corresponding computer-readable medium
AssigneeSiemens Aktiengesellschaft
InventorsRobi Malik, Martin Witte
Life of this patent
Estimating the term…
Abstract
When the automatic controls of a number of small automata are synthesized to form large automata, the latter are often difficult to manipulate and for the most part cannot be represented graphically. In order to maintain the applicability of incremental verification techniques, the larger automata are reduced, in accordance with the invention. This is done by modeling the automata in a discrete event system DES and by eliminating from the DES all redundant state transitions, disallowed states, and unimportant selfloops. The novel method is most prominently applicable in control programs and distributed control system controllers.
Claims16
A computer-implemented method of manipulating a machine control process by reducing a finite control automaton, comprising:
- modeling each of a plurality of primary automata in a primary discrete event system containing system components selected from a group including an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and self loops;
- calculating a synchronous product of the primary automata to obtain a combined discrete event system;
- defining, in the combined discrete event system, states with relevance in deciding whether a given event is allowed or forbidden and defining states without relevance;
- removing the states without relevance and forming a partition of the state space containing the states with relevance;
- and
- eliminating all redundant state transitions and forming a reduced discrete event system controlling the machine control process.
A computer-implemented method of reducing a finite control automaton, comprising:
- modeling each of a plurality of primary automata in a primary discrete event system containing system components selected from a group including an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and selfloops;
- determining a first set of states in which a given event is allowed and a second set of states in which the given event is prohibited;
- calculating a third set of prohibited pairs from the first and second sets by an iterative back-tracking procedure;
- if the third set does not contain all possible pairs of states, selecting an arbitrary pair not contained in the third set and defining further pairs by forward-tracking edges between the states;
- forming a covering of the state space of the discrete event system;
- replacing all multiple edges between states in the state space;
- redefining the first and second sets;
- repeating said calculating using the first and second sets as redefined;
- and
- forming a reduced discrete event system to control a manufacturing control process producing a product.
A computer-readable medium having computer-executable instructions for machine process control performing a method of reducing a finite control automaton, comprising:
- modeling each of a plurality of primary automata in a primary discrete event system containing system components selected from a group including an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and self loops;
- calculating a synchronous product of the primary automata to obtain a combined discrete event system;
- defining, in the combined discrete event system, states with relevance in deciding whether a given event is allowed or forbidden and defining states without relevance;
- removing the states without relevance and forming a partition of the state space containing the states with relevance;
- and
- eliminating all redundant state transitions and forming a reduced discrete event system enabling the primary automata to control the machine process in producing a desired product.
A computer-readable medium having computer-executable instructions embodied in a manufacturing process control computer system for performing a method comprising:
- modeling each of a plurality of primary automata in a primary discrete event system containing system components selected from a group including an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and selfloops controlling the manufacturing process control computer system;
- determining a first set of states in which a given event is allowed and a second set of states in which the given event is prohibited;
- calculating a third set of prohibited pairs from the first and second sets by an iterative back-tracking procedure;
- if the third set does not contain all possible pairs of states, selecting an arbitrary pair not contained in the third set and defining further pairs by forward-tracking edges between the states;
- forming a covering of the state space of the discrete event system;
- replacing all multiple edges between states in the state space;
- redefining the first and second sets;
- repeating said calculating using the first and second sets as redefined;
- and
- forming a reduced discrete event system.
A computer-readable medium embodying a set of application programs and application program interfaces for execution on a manufacturing process control computer system in conjunction with an application program for combining and simplifying finite control automata, comprising:
- a first interface for inputting data representing a plurality of primary automata in a system of related automata for controlling the manufacturing process control computer system;
- a processing stage for modeling each primary automaton as a primary discrete event system containing system components selected from the group consisting of an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and selfloops;
- a processing stage for calculating a synchronous product of the primary automata to obtain a combined discrete event system and for imposing limitations on the combined discrete event system to obtain a limited discrete event system;
- a processing stage programmed to eliminate all forbidden states from the state space of the limited discrete event system, to eliminate all redundant state transitions from the limited discrete event system, and to form a reduced discrete event system;
- and
- a second interface for outputting a representation of the reduced discrete event system.
A computer system for forming a reduced discrete event system, comprising:
- at least one input unit to input models of a plurality of primary automata in a primary discrete event system containing system components selected from a group including an event alphabet with a plurality of events, a state space with a plurality of states, an initial state, state transitions, and self loops;
- and
- a processor to calculate a synchronous product of the primary automata to obtain a combined discrete event system, to define, in the combined discrete event system, states with relevance in deciding whether a given event is allowed or forbidden and states without relevance, to remove the states without relevance, to form a partition of the state space containing the states with relevance, and to eliminate all redundant state transitions in forming the reduced discrete event system.
Dependencies are inferred from the claim text.