State space enumeration

Last updated

In computer science, state space enumeration are methods that consider each reachable program state to determine whether a program satisfies a given property. [1] As programs increase in size and complexity, the state space grows exponentially. The state space used by these methods can be reduced by maintaining only the parts of the state space that are relevant to the analysis. However, the use of state and memory reduction techniques makes runtime a major limiting factor. [2]

Computer science study of the theoretical foundations of information and computation

Computer science is the study of mathematical algorithms and processes that interact with data and that can be represented as data in the form of programs. It enables the use of algorithms to manipulate, store, and communicate digital information. A computer scientist studies the theory of computation and the practice of designing software systems.

In mathematical logic, satisfiability and validity are elementary concepts of semantics. A formula is satisfiable if it is possible to find an interpretation (model) that makes the formula true. A formula is valid if all interpretations make the formula true. The opposites of these concepts are unsatisfiability and invalidity, that is, a formula is unsatisfiable if none of the interpretations make the formula true, and invalid if some such interpretation makes the formula false. These four concepts are related to each other in a manner exactly analogous to Aristotle's square of opposition.

State space term in the theory of discrete dynamical systems; set of values which a process can take; set of states a system; (in a discrete system) countable and often finite

In the theory of discrete dynamical systems, a state space is the set of all possible configurations of a system. For example, a system in queueing theory defining the number of customers in a line would have state space {0, 1, 2, 3, ...}. State spaces can be either infinite or finite. An example of a finite state space is that of the toy problem Vacuum World, in which there are a limited set of configurations that the vacuum and dirt can be in.

See also

Related Research Articles

Discrete mathematics study of discrete mathematical structures

Discrete mathematics is the study of mathematical structures that are fundamentally discrete rather than continuous. In contrast to real numbers that have the property of varying "smoothly", the objects studied in discrete mathematics – such as integers, graphs, and statements in logic – do not vary smoothly in this way, but have distinct, separated values. Discrete mathematics therefore excludes topics in "continuous mathematics" such as calculus or Euclidean geometry. Discrete objects can often be enumerated by integers. More formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics." Indeed, discrete mathematics is described less by what is included than by what is excluded: continuously varying quantities and related notions.

Information retrieval (IR) is the activity of obtaining information system resources relevant to an information need from a collection. Searches can be based on full-text or other content-based indexing. Information retrieval is the science of searching for information in a document, searching for documents themselves, and also searching for metadata that describe data, and for databases of texts, images or sounds.

Z notation

The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.

Tony Hoare British computer scientist

Sir Charles Antony Richard Hoare, is a British computer scientist. He developed the sorting algorithm quicksort in 1959/1960. He also developed Hoare logic for verifying program correctness, and the formal language communicating sequential processes (CSP) to specify the interactions of concurrent processes and the inspiration for the occam programming language.

Ole-Johan Dahl was a Norwegian computer scientist. Dahl was a professor of computer science at the University of Oslo and is considered to be one of the fathers of Simula and object-oriented programming along with Kristen Nygaard.

In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based technique for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Petri net

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, in which the nodes represent transitions and places. The directed arcs describe which places are pre- and/or postconditions for which transitions. 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 the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

In computer science, model checking or property checking refers to the following problem: Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.

Theoretical computer science subfield of computer science and of mathematics

Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on more mathematical topics of computing and includes the theory of computation.

Concurrency (computer science)

In computer science, concurrency refers to the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the final outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability property of a program, algorithm, or problem into order-independent or partially-ordered components or units.

Neil Immerman American theoretical computer scientist (b.1953)

Neil Immerman is an American theoretical computer scientist, a professor of computer science at the University of Massachusetts Amherst. He is one of the key developers of descriptive complexity, an approach he is currently applying to research in model checking, database theory, and computational complexity theory.

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Process architecture is the structural design of general process systems. It applies to fields such as computers, business processes, and any other process system of varying degrees of complexity.

Wil van der Aalst Dutch computer scientist and professor

Willibrordus Martinus Pancratius van der Aalst is a Dutch computer scientist and full professor at RWTH Aachen University, leading the Process and Data Science (PADS) group. His research and teaching interests include information systems, workflow management, Petri nets, process mining, specification languages, and simulation. He is also known for his work on workflow patterns.

Martin Henson Dean of International Development and Professor of Computer Science at the University of Essex, UK

Professor Martin C. Henson FBCS FRSA is an English computer scientist based at the University of Essex. He is Dean for International Affairs and is affiliated to the School of Computer Science & Electronic Engineering. Henson was Head of the Department of Computer Science from 2000–2006.

Grzegorz Rozenberg Polish mathematician and computer scientist

Grzegorz Rozenberg is a Polish Dutch computer scientist.

Rüdiger Valk is a German mathematician. From 1976 to 2010 he was Professor for Theoretical Computer Science (Informatics) at the Institut für Informatik of the University of Hamburg, Germany.

References

  1. "A Compact Petri Net Representation for Concurrent Programs", Matthew B. Dwyer, Lori A. Clarke, Kari A. Niesy, Department of Computer Science, University of Massachusetts, Amherst Amherst, MA 01003
  2. "Proceedings of the conference on Application and theory of petri nets: formal methods in software engineering and defence systems - Volume 12", ACM International Conference Proceeding Series, Vol. 145, by Marko Mäkelä, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland