RWTH Aachen University, also known as Rhine-Westphalia Technical University of Aachen, Technical University of Aachen, University of Aachen, or Rheinisch-Westfälische Technische Hochschule Aachen, is a German public research university located in Aachen, North Rhine-Westphalia, Germany. With more than 47,000 students enrolled in 144 study programs, it is the largest technical university in Germany.
In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.
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 theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.
The Library of Efficient Data types and Algorithms (LEDA) is a proprietarily-licensed software library providing C++ implementations of a broad variety of algorithms for graph theory and computational geometry. It was originally developed by the Max Planck Institute for Informatics Saarbrücken. Since 2001, LEDA is further developed and distributed by the Algorithmic Solutions Software GmbH.
The Faculty of Georesources and Materials Engineering is one of nine faculties at the RWTH Aachen University. It comprises three sections for Raw Materials and Waste Disposal Technology, Metallurgy and Materials Technology and Geoscience and Geology. The faculty was found in 1880 and produced several notable individuals, including Friedrich Robert Helmert. Approximately 3,000 students are enrolled in the faculty.
In theoretical computer science, a stutter bisimulation is defined in a coinductive manner, as is bisimulation.
Let TS=(S,Act,→,I,AP,L) be a transition system. A stutter bisimulation for TS is
a binary relation R on S such that for all (s1,s2) which is in R:
- L(s1) = L(s2).
- If s1' is in Post(s1) with (s1',s2) is not in R,
Reinhard Wilhelm is a German computer scientist.
Jan van Leeuwen is a Dutch computer scientist and Emeritus professor of computer science at the Department of Information and Computing Sciences at Utrecht University.
Leif Kobbelt is a German university professor for Computer Science with a specialization in Computer Graphics. Since 2001 he is the head of the Institute for Computer Graphics and Multimedia at RWTH Aachen university.
Bernhard Steffen is a German computer scientist and professor at the TU Dortmund University, Germany. His research focuses on various facets of formal methods ranging from program analysis and verification, to workflow synthesis, to test-based modeling, and machine learning.
Rainer Waser is a German professor of Electrical Engineering at RWTH Aachen University. He is also director of the section Electronic Materials at the Peter Grünberg Institute which is located on the campus of Jülich Research Center. His research and teaching is on solid-state chemistry and defect chemistry to electronic properties and modelling, the technology of new materials and the physical properties of construction components.
Gerhard J. Woeginger was an Austrian mathematician and computer scientist who worked in Germany as a professor at RWTH Aachen University, where he chaired the algorithms and complexity group in the department of computer science.
Barbara M. Terhal is a theoretical physicist working in quantum information and quantum computing. She is a researcher at the Forschungszentrum Jülich, a professor in the EEMCS Department at TU Delft, as well as the Research Lead for the Terhal Group at QUTech. Her research concerns many areas in quantum information theory, including entanglement detection, quantum error correction, fault-tolerant quantum computing and quantum memories.
Tiziana Margaria is a computer scientist and software engineer whose research topics include formal methods and model-driven engineering. Educated in Italy, she has worked in Italy, Germany, Sweden, and Ireland, and currently works in Ireland as Chair of Software Systems in the University of Limerick's Department of Computer Science and Information Systems.
The International Conference on Concurrency Theory (CONCUR) is an academic conference in the field of computer science, with focus on the theory of concurrency and its applications. It is the flagship conference for concurrency theory according to the International Federation for Information Processing Working Group on Concurrency Theory. The conference is organised annually since 1988. Since 2015, papers presented at CONCUR are published in the LIPIcs–Leibniz International Proceedings in Informatics, a "series of high-quality conference proceedings across all fields in informatics established in cooperation with Schloss Dagstuhl –Leibniz Center for Informatics". Before, CONCUR papers were published in the series Lecture Notes in Computer Science.
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".
Christel Baier is a German theoretical computer scientist known for her work in model checking, temporal logic, and automata theory. She is a professor at TU Dresden, where she holds the chair for Algebraic and Logic Foundations of Computer Science in the Faculty of Computer Science. Baier is the editor-in-chief of Acta Informatica.
Regina Palkovits is a German chemist who is a Professor of Chemistry at the RWTH Aachen University. Her research considers heterogenous catalysis. She was elected a Fellow of the North Rhine-Westphalian Academy of Sciences, Humanities and the Arts in 2020.
Principles of Model Checking is a textbook on model checking, an area of computer science that automates the problem of determining if a machine meets specification requirements. It was written by Christel Baier and Joost-Pieter Katoen, and published in 2008 by MIT Press.
