Theory of regions

Last updated

The Theory of regions is an approach for synthesizing a Petri net from a transition system. As such, it aims at recovering concurrent, independent behavior from transitions between global states. Theory of regions handles elementary net systems as well as P/T nets and other kinds of nets. An important point is that the approach is aimed at the synthesis of unlabeled Petri nets only.

Contents


Definition


A region of a transition system is a mapping assigning to each state a number (natural number for P/T nets, binary for ENS) and to each transition label a number such that consistency conditions holds whenever . [1]

Intuitive explanation

Each region represents a potential place of a Petri net.

Mukund: event/state separation property, state separation property. [2]

Related Research Articles

<span class="mw-page-title-main">Permutation</span> Mathematical version of an order change

In mathematics, a permutation of a set is, loosely speaking, an arrangement of its members into a sequence or linear order, or if the set is already ordered, a rearrangement of its elements. The word "permutation" also refers to the act or process of changing the linear order of an ordered set.

<span class="mw-page-title-main">Petri net</span> One of several mathematical modeling systems for the description of distributed systems

A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.

In mathematics, particularly in matrix theory, a permutation matrix is a square binary matrix that has exactly one entry of 1 in each row and each column with all other entries 0. Such a matrix P, say of size n × n, can represent a permutation of n elements. Pre-multiplying an n-row matrix M by such a permutation matrix, forming PM, results in permuting the rows of M, while post-multiplying an n-column matrix M, forming MP, permutes the columns of M.

The Nambu–Goto action is the simplest invariant action in bosonic string theory, and is also used in other theories that investigate string-like objects. It is the starting point of the analysis of zero-thickness string behavior, using the principles of Lagrangian mechanics. Just as the action for a free point particle is proportional to its proper time — i.e., the "length" of its world-line — a relativistic string's action is proportional to the area of the sheet which the string traces as it travels through spacetime.

In physics, the Polyakov action is an action of the two-dimensional conformal field theory describing the worldsheet of a string in string theory. It was introduced by Stanley Deser and Bruno Zumino and independently by L. Brink, P. Di Vecchia and P. S. Howe in 1976, and has become associated with Alexander Polyakov after he made use of it in quantizing the string in 1981. The action reads:

In abstract algebra, Hilbert's Theorem 90 (or Satz 90) is an important result on cyclic extensions of fields (or to one of its generalizations) that leads to Kummer theory. In its most basic form, it states that if L/K is an extension of fields with cyclic Galois group G = Gal(L/K) generated by an element and if is an element of L of relative norm 1, that is

<span class="mw-page-title-main">Ramanujan tau function</span>

The Ramanujan tau function, studied by Ramanujan (1916), is the function defined by the following identity:

The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus.

In linear algebra, the Laplace expansion, named after Pierre-Simon Laplace, also called cofactor expansion, is an expression of the determinant of an n × n-matrix B as a weighted sum of minors, which are the determinants of some (n − 1) × (n − 1)-submatrices of B. Specifically, for every i, the Laplace expansion along the ith row is the equality

<span class="mw-page-title-main">Parabolic cylindrical coordinates</span>

In mathematics, parabolic cylindrical coordinates are a three-dimensional orthogonal coordinate system that results from projecting the two-dimensional parabolic coordinate system in the perpendicular -direction. Hence, the coordinate surfaces are confocal parabolic cylinders. Parabolic cylindrical coordinates have found many applications, e.g., the potential theory of edges.

In mathematics, the theory of optimal stopping or early stopping is concerned with the problem of choosing a time to take a particular action, in order to maximise an expected reward or minimise an expected cost. Optimal stopping problems can be found in areas of statistics, economics, and mathematical finance. A key example of an optimal stopping problem is the secretary problem. Optimal stopping problems can often be written in the form of a Bellman equation, and are therefore often solved using dynamic programming.

In game theory, a stochastic game, introduced by Lloyd Shapley in the early 1950s, is a repeated game with probabilistic transitions played by one or more players. The game is played in a sequence of stages. At the beginning of each stage the game is in some state. The players select actions and each player receives a payoff that depends on the current state and the chosen actions. The game then moves to a new random state whose distribution depends on the previous state and the actions chosen by the players. The procedure is repeated at the new state and play continues for a finite or infinite number of stages. The total payoff to a player is often taken to be the discounted sum of the stage payoffs or the limit inferior of the averages of the stage payoffs.

A queue machine, queue automaton, or pullup automaton (PUA) is a finite state machine with the ability to store and retrieve data from an infinite-memory queue. It is a model of computation equivalent to a Turing machine, and therefore it can process the same class of formal languages.

In the fields of computer vision and image analysis, the scale-invariant feature operator is an algorithm to detect local features in images. The algorithm was published by Förstner et al. in 2009.

Laser linewidth is the spectral linewidth of a laser beam.

Dynamical mean-field theory (DMFT) is a method to determine the electronic structure of strongly correlated materials. In such materials, the approximation of independent electrons, which is used in density functional theory and usual band structure calculations, breaks down. Dynamical mean-field theory, a non-perturbative treatment of local interactions between electrons, bridges the gap between the nearly free electron gas limit and the atomic limit of condensed-matter physics.

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton. Further, clocks can be reset. Timed automata are a sub-class of a type hybrid automata.

<span class="mw-page-title-main">ProbOnto</span> Knowledge base and ontology of probability distributions

ProbOnto is a knowledge base and ontology of probability distributions. ProbOnto 2.5 contains over 150 uni- and multivariate distributions and alternative parameterizations, more than 220 relationships and re-parameterization formulas, supporting also the encoding of empirical and univariate mixture distributions.

Properties of an execution of a computer program—particularly for concurrent and distributed systems—have long been formulated by giving safety properties and liveness properties.

References

  1. "Madhavan Mukund".
  2. Mukund, Madhavan (1992-12-01). "Petri nets and step transition systems". International Journal of Foundations of Computer Science. 03 (4): 443–478. doi:10.1142/S0129054192000231. ISSN   0129-0541.