About Myself

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

I have a M.S. in Mathematics from Masaryk University (1976) and 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 with the aim of integrating and intensifying reserach 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.

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 behavior 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 modeling and computer analysis. Since the complexity of biological networks is enormous due to 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 exact description of the networks, and in consequence, to infer interesting predictions of systems dynamics evolved in arbitrary environment. In order 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

Parameter synthesis for biochemical models

Systems biology models often have numerous parameters, such as kinetic constants, decay rates and drift/diffusion terms, which are unknown or only weakly constrained by existing experimental knowledge. A crucial problem for systems biology is that these parameters are often very difficult to measure directly. Furthermore, they may vary greatly according to their in vivo context. As a result, methods for the estimation of these parameters are of great interest. The goal of our research is to develop effective, fast, and scalable methods, techniques and tools for automated parameter estimation or synthesis for computational analysis of biological systems.

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

Digital Bifurcation Analysis of TCP Dynamics.

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

Digital bifurcation analysis is a new algorithmic method for exploring how the behaviour of a parameter-dependent computer system varies with a change in its parameters and, in particular, for identification of bifurcation points where such variation becomes dramatic. We have developed the method in an analogy with the traditional bifurcation theory and have it successfully applied to models taken from systems biology. In this case study paper, we demonstrate the appropriateness and usefulness of the digital bifurcation analysis as a push-button alternative to the classical approaches as traditionally used for analysing the stability of TCP/IP protocols. We consider two typical examples (congestion control and buffer sizes throughput influence) and show that the method provides the same results as obtained with classical non-automatic analytical and numerical methods.

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems.

N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek
CAV 2017
Conference Paper

We present a novel tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic. The tool is based on the algorithm of parallel semi-symbolic coloured model checking that extends standard model checking methods to cope with parametrised Kripke structures. The tool implements state-of-the-art techniques developed in previous research and is primarily intended to be used for the analysis of dynamical systems with uncertain parameters that frequently arise in computational systems biology. However, it can be employed for any dynamical system where the non-linear equations can be sufficiently well approximated by piecewise multi-affine equations.

Precise parameter synthesis for stochastic biochemical systems.

M. Češka, F. Dannenberg, N. Paoletti, M. Kwiatkowska, L. Brim
Acta Informatica
Journal Paper

We consider the problem of synthesising rate parameters for stochastic biochemical networks so that a given time-bounded CSL property is guaranteed to hold, or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised. Our method is based on extending CSL model checking and standard uniformisation to parametric models, in order to compute safe bounds on the satisfaction probability of the property. We develop synthesis algorithms that yield answers that are precise to within an arbitrarily small tolerance value. The algorithms combine the computation of probability bounds with the refinement and sampling of the parameter space. Our methods are precise and efficient, and improve on existing approximate techniques that employ discretisation and refinement. We evaluate the usefulness of the methods by synthesising rates for three biologically motivated case studies: infection control for a SIR epidemic model; reliability analysis of molecular computation by a DNA walker; and bistability in the gene regulation of the mammalian cell cycle.

Detecting Attractors in Biological Models with Uncertain Parameters.

J. Barnat, N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva, D. Safranek
CMSB 2017
Conference Paper

Complex behaviour arising in biological systems is typically characterised by various kinds of attractors. An important problem in this area is to determine these attractors. Biological systems are usually described by highly parametrised dynamical models that can be represented as parametrised graphs typically constructed as discrete abstractions of continuous-time models. In such models, attractors are observed in the form of terminal strongly connected components (tSCCs). In this paper, we introduce a novel method for detecting tSCCs in parametrised graphs. The method is supplied with a parallel algorithm and evaluated on discrete abstractions of several non-linear biological models.

A Model Checking Approach to Discrete Bifurcation Analysis.

N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek
Formal Methods 2016
Conference Paper

Bifurcation analysis is a central task of the analysis of para- meterised 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. In this paper we propose a novel 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. To describe such behaviour patterns, called phase portraits, we use a hybrid version of a CTL logic augmented with direction formulae. We demonstrate the method on a case study taken from systems biology.

PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems.

M. Ceska, P. Pilar, N. Paoletti, L. Brim, and M. Kwiatkowska
TACAS 2016
Conference Paper

In this paper we present PRISM-PSY, a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains and time-bounded temporal logic specifications. We redesign, in terms of matrix-vector operations, the recently formulated algorithms for precise parameter synthesis in order to enable effective data-parallel processing, which results in significant acceleration on many-core architectures. High hardware utilisation, essential for performance and scalability, is achieved by state space and parameter space parallelisation: the former leverages a compact sparse-matrix representation, and the latter is based on an iterative decomposition of the parameter space. Our experiments on several biological and engineering case studies demonstrate an overall speedup of up to 31-fold on a single GPU compared to the sequential implementation.

Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems.

N. Benes, L. Brim, M. Demko, S. Pastva, D. Safranek
ATVA 2016
Conference Paper

We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.

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

+420 549 493 367

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