Stutter bisimulation

Last updated

In theoretical computer science, a stutter bisimulation is a relationship between two transition systems, abstract machines that model computation. It is defined coinductively and generalizes the idea of bisimulations. A bisimulation matches up the states of a machine such that transitions correspond; a stutter bisimulation allows transitions to be matched to finite path fragments. [1]

Contents

Definition

In Principles of Model Checking , Baier and Katoen define a stutter bisimulation for a single transition system and later adapt it to a relation on two transition systems. A stutter bisimulation for is a binary relation R on S such that for all (s1,s2) in R:

  1. have the same labels
  2. If is a valid transition and then there exists a finite path fragment () such that each pair is in R and is in R
  3. If is a valid transition and is not then there exists a finite path fragment () such that each pair is in R and is in R

Generalizations

A generalization, the divergent stutter bisimulation, can be used to simplify the state space of a system with the tradeoff that statements using the linear temporal logic operator "next" may change truth value. [2] A robust stutter bisimulation allows uncertainty over transitions in the system. [3]

Related Research Articles

In the mathematical field of algebraic topology, the fundamental group of a topological space is the group of the equivalence classes under homotopy of the loops contained in the space. It records information about the basic shape, or holes, of the topological space. The fundamental group is the first and simplest homotopy group. The fundamental group is a homotopy invariant—topological spaces that are homotopy equivalent have isomorphic fundamental groups. The fundamental group of a topological space is denoted by .

In mathematics, the infimum of a subset of a partially ordered set is the greatest element in that is less than or equal to each element of if such an element exists. If the infimum of exists, it is unique, and if b is a lower bound of , then b is less than or equal to the infimum of . Consequently, the term greatest lower bound is also commonly used. The supremum of a subset of a partially ordered set is the least element in that is greater than or equal to each element of if such an element exists. If the supremum of exists, it is unique, and if b is an upper bound of , then the supremum of is less than or equal to b. Consequently, the supremum is also referred to as the least upper bound.

In computer science, an LL parser is a top-down parser for a restricted context-free language. It parses the input from Left to right, performing Leftmost derivation of the sentence.

In mathematical analysis, the Minkowski inequality establishes that the Lp spaces are normed vector spaces. Let be a measure space, let and let and be elements of Then is in and we have the triangle inequality

<span class="mw-page-title-main">Petri net</span> Model to describe 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, homotopy groups are used in algebraic topology to classify topological spaces. The first and simplest homotopy group is the fundamental group, denoted which records information about loops in a space. Intuitively, homotopy groups record information about the basic shape, or holes, of a topological space.

<span class="mw-page-title-main">Maximal and minimal elements</span> Element that is not ≤ (or ≥) any other element

In mathematics, especially in order theory, a maximal element of a subset of some preordered set is an element of that is not smaller than any other element in . A minimal element of a subset of some preordered set is defined dually as an element of that is not greater than any other element in .

The notion of a fibration generalizes the notion of a fiber bundle and plays an important role in algebraic topology, a branch of mathematics.

In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.

In mathematics, a divergent series is an infinite series that is not convergent, meaning that the infinite sequence of the partial sums of the series does not have a finite limit.

Model predictive control (MPC) is an advanced method of process control that is used to control a process while satisfying a set of constraints. It has been in use in the process industries in chemical plants and oil refineries since the 1980s. In recent years it has also been used in power system balancing models and in power electronics. Model predictive controllers rely on dynamic models of the process, most often linear empirical models obtained by system identification. The main advantage of MPC is the fact that it allows the current timeslot to be optimized, while keeping future timeslots in account. This is achieved by optimizing a finite time-horizon, but only implementing the current timeslot and then optimizing again, repeatedly, thus differing from a linear–quadratic regulator (LQR). Also MPC has the ability to anticipate future events and can take control actions accordingly. PID controllers do not have this predictive ability. MPC is nearly universally implemented as a digital control, although there is research into achieving faster response times with specially designed analog circuitry.

A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke, used in model checking to represent the behavior of a system. It consists of a graph whose nodes represent the reachable states of the system and whose edges represent state transitions, together with a labelling function which maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.

In mathematical analysis, the alternating series test is the method used to show that an alternating series is convergent when its terms (1) decrease in absolute value, and (2) approach zero in the limit. The test was used by Gottfried Leibniz and is sometimes known as Leibniz's test, Leibniz's rule, or the Leibniz criterion. The test is only sufficient, not necessary, so some convergent alternating series may fail the first part of the test.

A fully polynomial-time approximation scheme (FPTAS) is an algorithm for finding approximate solutions to function problems, especially optimization problems. An FPTAS takes as input an instance of the problem and a parameter ε > 0. It returns as output a value which is at least times the correct value, and at most times the correct value.

Euclid's theorem is a fundamental statement in number theory that asserts that there are infinitely many prime numbers. It was first proven by Euclid in his work Elements. There are several proofs of the theorem.

Ramanujan summation is a technique invented by the mathematician Srinivasa Ramanujan for assigning a value to divergent infinite series. Although the Ramanujan summation of a divergent series is not a sum in the traditional sense, it has properties that make it mathematically useful in the study of divergent infinite series, for which conventional summation is undefined.

In mathematics, the Veblen functions are a hierarchy of normal functions, introduced by Oswald Veblen in Veblen (1908). If φ0 is any normal function, then for any non-zero ordinal α, φα is the function enumerating the common fixed points of φβ for β<α. These functions are all normal.

<span class="mw-page-title-main">Velocity</span> Speed and direction of a motion

Velocity is the speed in combination with the direction of motion of an object. Velocity is a fundamental concept in kinematics, the branch of classical mechanics that describes the motion of bodies.

<span class="mw-page-title-main">Stuttering equivalence</span>

In theoretical computer science, stuttering equivalence, a relation written as

In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system. Example properties include "the vending machine does not dispense a drink until money has been entered" or "the computer program eventually terminates". Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often".

References

  1. Principles of Model Checking (pages 536–580), by Christel Baier and Joost-Pieter Katoen, The MIT Press, Cambridge, Massachusetts.
  2. "Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications". Automatica. 130. 2021. doi:10.1016/j.automatica.2021.109723.
  3. "Robust stutter bisimulation for abstraction and controller synthesis with disturbance". Automatica. 160. 2024. doi:10.1016/j.automatica.2023.111394.