Temporal Process Language

Last updated

In theoretical computer science, Temporal Process Language (TPL) is a process calculus which extends Robin Milner's CCS with the notion of multi-party synchronization, which allows multiple process to synchronize on a global 'clock'. This clock measures time, though not concretely, but rather as an abstract signal which defines when the entire process can step onward.

Contents

Informal definition

TPL is a conservative extension of CCS, with the addition of a special action called σ representing the passage of time by a process - the ticking of an abstract clock. As in CCS, TPL features action prefix and it can be described as being patient, that is to say a process will idly accept the ticking of the clock, written as

Key to the use of abstract time is the timeout operator, which presents two processes, one to behave as if the clock ticks, one to behave as if it can't, i.e.

provided process E does not prevent the clock from ticking.

provided E can perform action a to become E'.

In TPL, there are two ways to prevent the clock from ticking. First is via the presence of the ω operator, for example in process the clock is prevented from ticking. It can be said that the action a is insistent, i.e. it insists on acting before the clock can tick again.

The second way in which ticking can be prevented is via the concept of maximal-progress, which states that silent actions (i.e. τ actions) always take precedence over and thus suppress σ actions. Thus is two parallel processes are capable of synchronizing at a given instant, it is not possible for the clock to tick.

Thus a simple way of viewing multi-party synchronization is that a group of composed processes will allow time to pass provided none of them prevent it, i.e. the system agrees that it is time to move on.

Formal definition

Syntax

Let a be a non-silent action name, α be any action name (including τ, the silent action) and X be a process label used for recursion.

Related Research Articles

<span class="mw-page-title-main">Pink noise</span> Signal with equal energy per octave

Pink noise, 1f noise or fractional noise or fractal noise is a signal or process with a frequency spectrum such that the power spectral density is inversely proportional to the frequency of the signal. In pink noise, each octave interval carries an equal amount of noise energy.

<span class="mw-page-title-main">Floor and ceiling functions</span> Nearest integers from a number

In mathematics and computer science, the floor function is the function that takes as input a real number x, and gives as output the greatest integer less than or equal to x, denoted x or floor(x). Similarly, the ceiling function maps x to the smallest integer greater than or equal to x, denoted x or ceil(x).

In number theory, an additive function is an arithmetic function f(n) of the positive integer variable n such that whenever a and b are coprime, the function applied to the product ab is the sum of the values of the function applied to a and b:

In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.

<span class="mw-page-title-main">Square wave</span> Type of non-sinusoidal waveform

A square wave is a non-sinusoidal periodic waveform in which the amplitude alternates at a steady frequency between fixed minimum and maximum values, with the same duration at minimum and maximum. In an ideal square wave, the transitions between minimum and maximum are instantaneous.

In mathematics, a Sobolev space is a vector space of functions equipped with a norm that is a combination of Lp-norms of the function together with its derivatives up to a given order. The derivatives are understood in a suitable weak sense to make the space complete, i.e. a Banach space. Intuitively, a Sobolev space is a space of functions possessing sufficiently many derivatives for some application domain, such as partial differential equations, and equipped with a norm that measures both the size and regularity of a function.

In model theory, a transfer principle states that all statements of some language that are true for some structure are true for another structure. One of the first examples was the Lefschetz principle, which states that any sentence in the first-order language of fields that is true for the complex numbers is also true for any algebraically closed field of characteristic 0.

In number theory, the integer square root (isqrt) of a non-negative integer n is the non-negative integer m which is the greatest integer less than or equal to the square root of n,

<span class="mw-page-title-main">Baker's map</span> Chaotic map from the unit square into itself

In dynamical systems theory, the baker's map is a chaotic map from the unit square into itself. It is named after a kneading operation that bakers apply to dough: the dough is cut in half, and the two halves are stacked on one another, and compressed.

In number theory, the law of quadratic reciprocity, like the Pythagorean theorem, has lent itself to an unusually large number of proofs. Several hundred proofs of the law of quadratic reciprocity have been published.

In mathematics, specifically in symplectic geometry, the momentum map is a tool associated with a Hamiltonian action of a Lie group on a symplectic manifold, used to construct conserved quantities for the action. The momentum map generalizes the classical notions of linear and angular momentum. It is an essential ingredient in various constructions of symplectic manifolds, including symplectic (Marsden–Weinstein) quotients, discussed below, and symplectic cuts and sums.

In information theory, information dimension is an information measure for random vectors in Euclidean space, based on the normalized entropy of finely quantized versions of the random vectors. This concept was first introduced by Alfréd Rényi in 1959.

In mathematics, a sample-continuous process is a stochastic process whose sample paths are almost surely continuous functions.

In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge. In domains where computations are expected to be infinite, such as process calculi, a computation is said to diverge if it fails to be productive.

In stochastic analysis, a rough path is a generalization of the notion of smooth path allowing to construct a robust solution theory for controlled differential equations driven by classically irregular signals, for example a Wiener process. The theory was developed in the 1990s by Terry Lyons. Several accounts of the theory are available.

<span class="mw-page-title-main">Suffix automaton</span> Deterministic finite automaton accepting set of all suffixes of particular string

In computer science, a suffix automaton is an efficient data structure for representing the substring index of a given string which allows the storage, processing, and retrieval of compressed information about all its substrings. The suffix automaton of a string is the smallest directed acyclic graph with a dedicated initial vertex and a set of "final" vertices, such that paths from the initial vertex to final vertices represent the suffixes of the string.

Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates. The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably total if and only if it belongs to a given complexity class. Further, theories of bounded arithmetic present uniform counterparts to standard propositional proof systems such as Frege system and are, in particular, useful for constructing polynomial-size proofs in these systems. The characterization of standard complexity classes and correspondence to propositional proof systems allows to interpret theories of bounded arithmetic as formal systems capturing various levels of feasible reasoning.

In number theory, the prime omega functions and count the number of prime factors of a natural number Thereby counts each distinct prime factor, whereas the related function counts the total number of prime factors of honoring their multiplicity. That is, if we have a prime factorization of of the form for distinct primes , then the respective prime omega functions are given by and . These prime factor counting functions have many important number theoretic relations.

In analytic number theory, a Dirichlet series, or Dirichlet generating function (DGF), of a sequence is a common way of understanding and summing arithmetic functions in a meaningful way. A little known, or at least often forgotten about, way of expressing formulas for arithmetic functions and their summatory functions is to perform an integral transform that inverts the operation of forming the DGF of a sequence. This inversion is analogous to performing an inverse Z-transform to the generating function of a sequence to express formulas for the series coefficients of a given ordinary generating function.

In optimal transport, a branch of mathematics, polar factorization of vector fields is a basic result due to Brenier (1987), with antecedents of Knott-Smith (1984) and Rachev (1985), that generalizes many existing results among which are the polar decomposition of real matrices, and the rearrangement of real-valued functions.

References

Matthew Hennessy and Tim Regan : A Process Algebra for Timed Systems. Information and Computation, 1995.