In the second half of the previous century it was realized that behavior can very naturally be described by labeled transition systems. The primary motivation came from the desire to describe the communication of a computer system with its environment, for instance a user, or with other computer systems.

But the framework is also very suitable to describe for instance human to human communication, interaction of physical objects, and recently much attention goes into modeling complex chemical processes in living cells in this way.

With such models of behavior, it is possible to ask and answer all kinds of questions about the behavior. Will a computer always respond to an incoming request? Is the behavior of a computer deadlock free? Is the behavior of the new computer behaviorally equivalent to the one it is replacing? Investigating which properties a given behavior has is called analysis.

There are many formalisms and tools to model and analyze behavior these days. The chair Formal System Analysis (FSA) concentrates on the development and use of the mCRL2 language and its associated toolset. The mCRL2 toolset distinguishes itself on the one hand from other tools, as it tries to be as close to common mathematical and logical concepts as possible, to have maximal expressivity.

On the other hand the chair goes to great lengths to guarantee that the tools are among the best if it comes to the analysis of concrete industrial systems.

Current research focuses on proving that properties formulated in the modal mu-calculus with data are valid for given process models. The technique used for this is to translate the formula and the model to a parameterised boolean equation system (PBES) which the chair subsequently solves. Solving large PBESs is not easy and often very time consuming. The chair is looking to find substantial faster ways to do this.

Furthermore, the chair is looking into scaling up real time verification to industrial scale. Currently, it is possible to verify smaller timed systems. Unlike untimed systems, of which the analysis techniques are quite capable to deal with industrial systems, this is not the case if explicit time bounds or time outs are used.

FSA also has a strong interest in modeling of stochastic behavior. Currently, this is not possible in mCRL2. It is very well possible to answer questions like "Will this message always be delivered", but the researchers of FSA cannot straightforwardly deal with questions like "Will this message on average be delivered in more than 90% of the cases". They can only answer such questions by encoding probabilities using data parameters in processes, and although this does work, they want a more elegant framework.

So, the focus of the chair FSA is on modelling and verifying behavior of systems and programs. Behavior must be understood as all possible actions that a system can consecutively perform during its lifetime. Computer-based systems are so complex, that it is impossible to program them without understanding how the different software components communicate, and what the responsibilities of these parts are. By modeling the behavior, these responsibilities are made explicit. Due to the complexity of the matter at hand, it is also non-trivial to get these behavioral models correct.

For this purpose we use analysis techniques. Primarily, these are used to find flaws in the model, and ultimately these are employed to show that the modeled behavior satisfies all the requirements. For instance, a data communication protocol must not lose messages, and a firewall should under no circumstance let an intruder pass.

With current modeling techniques it is no problem to model the communication patterns of even the most complex systems. Using modal formulas most requirements can be formulated in a formal, precise way. Using one of the many existing process equivalences, it is very well possible to state the behavioral equivalence between implementations and specifications.

So, in general, it is not really problematic (but sometimes hard) to formulate the properties that a system ought to have. The current technological bottleneck is our capability to prove that a requirement holds for a given model (the model checking problem) or that two processes are actually equivalent (the equivalence checking problem).

The major research activity of this group is to increase the strength of the analysis tools. The core problem of the analysis of behavior is the state space explosion problem. There are so many states in which a system can end up, that it is generally impossible to explore these all individually.

For this purpose, we must use so-called symbolic techniques to enable the verification. These techniques come from the realm of automatic reasoning, term rewriting and computer assisted theorem checking. Also, state space reduction techniques (abstract interpretation, confluence checking) are relevant to reduce the problem size.

The chair FSA offers many interesting Master's thesis projects in this area.