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 and check 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).

Research

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 Specified 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 specified 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.

Numbers

30

DBLP journals

97

DBLP Conferences

4000

Google scholar citations

35

Google Scholar h-index

Featured Publications

Scopus Author ID: 57217505618
Web of Science

List of publications since 2000

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.

Boolean network sketches: a unifying framework for logical model inference.

N. Benes, L. Brim, O. Huvar, S. Pastva, D. Safranek
Bioinformatics, Vol. 38, No. 4, 2023.
Journal Paper

We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network’s topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network’s transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an ‘initial’ sketch, which is extended by adding restrictions representing experimental data to a ‘data-informed’ sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data.

BibTeX file @ DBLP

Teaching

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

IV010 Communication and parallelism.

The goal is to acquire basic skills that are used for formal specification and analysis of communicating systems, including the theoretical background. By the end of the course the students should be able: to develop simple specifications and implementations of communicating systems in CCS, to check formally their equivalence and to understand various kinds of process equivalences and their limitations.
Sylabus: Introduction, overview of models for concurrent systems. Modeling communication, examples of communicating systems. Language of CCS: synchronization, actions and transitions, internal communication, semantics of CCS. CCS with value passing and its translation into pure CCS. Equational laws and their applications: classification of combinators, expansion theorem, dynamic and static laws. Bisimulation and equivalence: Strong bisimulation, weak bisimulation, weak congruence, basic properties, solving equations, other equivalences, finite state processes. Temporal properties of processes, introduction to the modal mu-calculus.
Course pages in Czech

IV022 Principles of Elegant Programming.

The goal is to get acquainted with methods, principles, and strategies for designing small, elegant, and correct sequential algorithms.
Course pages in Czech

IA040 Modal and Temporal Logics for Processes.

The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems. The students should be able to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs; to understand the differences in the logics, and their capabilities and limitations; to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Course pages in Czech

IA046 Computabilty.

The course is focused on deeper understanding of results in the computability theory with emphasis on methods and techniques used to prove such results. • At the end of the course the students will be able to understand basics of computability over real numbers; will get acquainted with additional results about classification of computational problems, in particular about arithmetical hierarchy and relativised theory of computability.
Course pages in Czech

IA073 GEB - Limits of Formal Systems.

The aim of the seminar is to deepen the understanding of limits of formal computation systems. To that end the book "Gödel, Escher, Bach: An Eternal Golden Braid" by D. Hofstadter is "read" and discussed.
Course pages in Czech

IA074 On the Origin of Autonomous Systems.

The aim of the seminar is to deepen the understanding of complex systems. To that end the book "Investigations" by Stuart Kauffman is "read" and discussed.
Course pages in Czech

PA052 Introduction to Systems Biology.

This is a bachelor-level course devoted to application of computer-scientific methods and tools in the emerging field of Systems Biology. The course is focused on functional aspects of mechanisms that drive living organisms. The main goal of this course is to show students that abstract computer-scientific and mathematical methods can be effectively employed for in silico modeling and analysis of living organisms. Moreover, to enhance practical skills, students have to apply some of the techniques and software tools to analysis of a small in silico model of some primitive organism in the range of a semestral project.
Sylabus: History and scope of systems biology. Elementary biological notions. Elementary notions of systemic paradigm - biological process studied in terms of a complex system. Model organisms. Sources of biological data - Databases of biological knowledge. Research scenario in systems biology, role of computer science. Models in systems biology, model databases. Examples of systems biology application. Design and reconstruction of biological networks - Synthetic Biology. Information in biology and about biology.
Course pages in Czech

Contact

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