About Myself

I am a professor at the Department of Computer Science, Faculty of Informatics, Masaryk University.

I have an M.S. in Mathematics from Masaryk University (1976) and a PhD in Computer Sciences from the Czech Academy of Sciences (1986) under Professor J. Horejs. Since 2006 I am a full professor of informatics at Masaryk University.

My current research interests include automated formal verification, parallel verification and digital systems biology.

In 2009, I founded the Laboratory of Systems Biology intending to integrate and intensify research and education activities in the emerging area of Computational Systems Biology at the Faculty of Informatics, Masaryk University.

From January 1, 2016, we became part of the national research infrastructure C4Sys (Centre for System Biology), representing a Czech node of the ISBE (Infrastructure for Systems Biology – Europe), and our activities are supported from the program for large research infrastructures of the Ministry of Education, Youth and Sports.

For a more detailed CV, please follow this external link or My Academic Genealogy.

a touch of history

The Department of Applied Mathematics, a predecessor to the Department of Computer Science, was located in the historical buildings till 1981. On the photograph is the main entrance to the building.
The main courtyard. The department itself was situated on the first floor.
The photograph was taken during the visit of Prof. Ballag (1976).


The aim of our research in digital systems biology is to enhance our understanding of the molecular mechanisms underlying the behaviour of complex living systems. The goal is to gain a better explanation of how the complex dynamic behaviour of the cell emerges from the interactions of molecular species. When solving such a non-trivial goal, the data have to be necessarily integrated with mathematical modelling and computer analysis. Since the complexity of biological networks is enormous due to the appearance of complicated feedback loops, the system dynamics is often counter-intuitive and cannot be directly predicted from the network structure.

Computer science technologies together with computer tools employing suitable mathematical and computer science methods can help to obtain an exact description of the networks, and in consequence, to infer interesting predictions of systems dynamics evolved in an arbitrary environment. To cope with large-scale biological models describing interaction in the scale of several functional layers of a living cell, the central requirement imposed on analysis tools is the scalability.

sybila logo

Partially Defined Boolean Networks

Boolean network is a very simple model of a biological system: each node takes either 0 or 1 and the states of nodes change according to regulation rules given as Boolean functions. In partially defined Boolean networks, some of these Boolean functions are (partially) unknown. Viewed in another way, we only know values of the Boolean functions for some arguments. The goal of our research is to develop effective, fast, and scalable methods, techniques and tools for automated analysis of robustness and control of partially defined Boolean networks.

sybila logo

Discrete Bifurcation Analysis

Bifurcation analysis is a central task of the analysis of parameterised high-dimensional dynamical systems that undergo transitions as parameters are changed. The classical numerical and analytical methods are typically limited to a small number of system parameters. Our goal is to develop an approach to bifurcation analysis that is based on a suitable discrete abstraction of the system and employs model checking for discovering critical parameter values, referred to as bifurcation points, for which various kinds of behaviour (equilibrium, cycling) appear or disappear.



DBLP journals


DBLP Conferences


Google scholar citations


Google Scholar h-index

Computing Bottom SCCs Symbolically Using Transition Guided Reduction.

N. Benes, L. Brim, S. Pastva, D. Safranek
CAV 2021
Conference Paper

Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one. Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, called interleaved transition guided reduction (ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states.

Symbolic Coloured SCC Decomposition.

N. Benes, L. Brim, S. Pastva, D. Safranek
TACAS 2021
Conference Paper

Problems arising in many scientific disciplines are often modelled using edge-coloured directed graphs. These can be enormous in the number of both vertices and colours. Given such a graph, the original problem frequently translates to the detection of the graph’s strongly connected components, which is challenging at this scale. We propose a new, symbolic algorithm that computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs 𝑂(𝑝⋅𝑛⋅log𝑛) symbolic steps, where p is the number of colours and n the number of vertices. We evaluate the algorithm using an experimental implementation based on Binary Decision Diagrams (BDDs) and large (up to 2^48) coloured graphs produced by models appearing in systems biology.

AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks.

N. Benes, L. Brim, J. Kadlecaj, S. Pastva, D. Safranek
CAV 2020
Conference Paper

Boolean networks (BNs) provide an effective modelling tool for various phenomena from science and engineering. Any long-term behaviour of a BN eventually converges to a so-called attractor. Depending on various logical parameters, the structure and quality of attractors can undergo a significant change, known as a bifurcation. We present a tool for analysing bifurcations in asynchronous parametrised Boolean networks. To fight the state-space and parameter-space explosion problem the tool uses a parallel semi-symbolic algorithm.

BibTeX file @ DBLP


I am responsible for the field of study “Bioinformatics and Systems Biology” at the Faculty of Informatics.

This field of study targets students who would like to obtain basic knowledge in the area of computer science and at the same time learn how to apply this knowledge to the benefit of molecular biology, genetics, medicine and other recently established disciplines, such as bioinformatics, proteomics, genomics, and systems biology. The progress in these disciplines is often hindered by difficulties in communication between people with technical and biological education. However, the ever-growing biological data can not be dealt without the use of modern algorithms and detailed knowledge of computer science.

The main goal of teaching Bioinformatics and Systems Biology at the Faculty of Informatics is to introduce this attractive interdisciplinary field of study to interested students, provide them with knowledge needed to understand existing problems and equip them with skills needed to solve many of them effectively. Areas currently using bioinformatics and systems biology include biology, modern biotechnology, medicine, pharmacy, and forensic science. A number of companies, especially abroad, develop software and hardware for scientific and practical needs. The potential for future development in this area is very good.

I currently teach


Call Me

I don't have an office phone and my university number is inactive.

Email Me

surname at fi.muni.cz

Visit Me

Faculty of Informatics
Botanicka 68a
602 00 BRNO
Czech Republic

Room A411

Office Hours

Wednesday 9.00-10.00
or by appointment