Related Research Articles
Queueing theory is the mathematical study of waiting lines, or queues. A queueing model is constructed so that queue lengths and waiting time can be predicted. Queueing theory is generally considered a branch of operations research because the results are often used when making business decisions about the resources needed to provide a service.
A Markov chain or Markov process is a stochastic model describing a sequence of possible events in which the probability of each event depends only on the state attained in the previous event. Informally, this may be thought of as, "What happens next depends only on the state of affairs now." A countably infinite sequence, in which the chain moves state at discrete time steps, gives a discrete-time Markov chain (DTMC). A continuous-time process is called a continuous-time Markov chain (CTMC). It is named after the Russian mathematician Andrey Markov.
In statistics, Markov chain Monte Carlo (MCMC) is a class of algorithms used to draw samples from a probability distribution. Given a probability distribution, one can construct a Markov chain whose elements' distribution approximates it – that is, the Markov chain's equilibrium distribution matches the target distribution. The more steps that are included, the more closely the distribution of the sample matches the actual desired distribution.
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.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
Network calculus is "a set of mathematical results which give insights into man-made systems such as concurrent programs, digital circuits and communication networks." Network calculus gives a theoretical framework for analysing performance guarantees in computer networks. As traffic flows through a network it is subject to constraints imposed by the system components, for example:
The Advanced Learning and Research Institute (ALaRI), a faculty of informatics, was established in 1999 at the University of Lugano to promote research and education in embedded systems. The Faculty of Informatics within very few years has become one of the Switzerland major destinations for teaching and research, ranking third after the two Federal Institutes of Technology, Zurich and Lausanne.
CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
TAPAs is a tool for specifying and analyzing concurrent systems. Its aim is to support teaching of process algebras. Systems are described as process algebra terms that are then mapped to labeled transition systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions or by model checking temporal formulas over the obtained LTS. A key feature of TAPAs that makes it particularly suited for teaching is that it maintains a consistent graphical and textual representation of each system. After a change in the graphic notation, the textual representation is updated immediately; but after textual modifications, the update of the graphical representation has to be manually triggered.
Marta Zofia Kwiatkowska is a Polish theoretical computer scientist based in the United Kingdom.
The UK Large-Scale Complex IT Systems (LSCITS) Initiative is a research and graduate education programme focusing on the problems of developing large-scale, complex IT systems. The initiative is funded by the EPSRC, with more than ten million pounds of funding awarded between 2006 and 2013.
In queueing theory, a discipline within the mathematical theory of probability, a fluid queue is a mathematical model used to describe the fluid level in a reservoir subject to randomly determined periods of filling and emptying. The term dam theory was used in earlier literature for these models. The model has been used to approximate discrete models, model the spread of wildfires, in ruin theory and to model high speed data networks. The model applies the leaky bucket algorithm to a stochastic source.
Stochastic Petri nets are a form of Petri net where the transitions fire after a probabilistic delay determined by a random variable.
Stochastic cellular automata or probabilistic cellular automata (PCA) or random cellular automata or locally interacting Markov chains are an important extension of cellular automaton. Cellular automata are a discrete-time dynamical system of interacting entities, whose state is discrete.
The following outline is provided as an overview of and topical guide to machine learning:
AltaRica is an object-oriented modeling language dedicated to probabilistic risk and safety analyses. It is a representative of the so-called model-based approach in reliability engineering. Since its version 3.0, it is developed by the non-profit AltaRica Association, which develops jointly the associated modeling environment AltaRica Wizard.
Lenore D. Zuck is an Israeli-American computer scientist whose research involves formal methods in software engineering, as well as information privacy. She is a research professor of computer science at the University of Illinois Chicago.
Kim Guldstrand Larsen R is a Danish scientist and professor of computer science at Aalborg University, Denmark. His field of research includes modeling, validation and verification, performance analysis, and synthesing of real-time, embedded, and cyber-physical systems utilizing and contributing to concurrency theory and model checking. Within this domain, he has been instrumental in the invention and continuous development of one of the most widely used verification tools, and has received several awards and honors for his work.
References
- ↑ Kwiatkowska, M.; Norman, G.; Parker, D. (2011). "PRISM 4.0: Verification of Probabilistic Real-time Systems". In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of Lecture Notes in Computer Science, pages 585-591, Springer.
- ↑ "PRISM case studies repository" . Retrieved 2024-04-19.
- ↑ [[Kwiatkowska, M.; Norman, G; Parker, D.; Santos, G. (2020). "PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time". In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of Lecture Notes in Computer Science, pages 475-487, Springer.
