DBLOK2 Seminar on Formal Methods for Complex Systems

Faculty of Informatics
Spring 2012
Extent and Intensity
0/2/0. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Luca Bortolussi, Ph.D. (lecturer), doc. RNDr. David Šafránek, Ph.D. (deputy)
doc. RNDr. David Šafránek, Ph.D. (lecturer)
Guaranteed by
prof. Ing. Václav Přenosil, CSc.
Department of Machine Learning and Data Processing – Faculty of Informatics
Supplier department: Department of Machine Learning and Data Processing – Faculty of Informatics
Timetable
Mon 21. 5. 14:00–17:00 B410, Tue 22. 5. 10:00–13:00 B410, Wed 23. 5. 10:00–13:00 B410, Thu 24. 5. 10:00–13:00 B410, Fri 25. 5. 10:00–13:00 B410
Prerequisites (in Czech)
Elementary knowledge of formal methods, stochastic processes and process algebras is welcome.
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 20 student(s).
Current registration and enrolment status: enrolled: 0/20, only registered: 0/20, only registered with preference (fields directly associated with the programme): 0/20
fields of study / plans the course is directly associated with
Course objectives (in Czech)
The course starts by focusing on formal languages suitable for description of complex systems, belonging to the class of process algebras (PA). Presented will be in particular two of them, BioPEPA and sCCP. Then, the attention will be turned to the mathematical framework. Since of the main interest are the dynamical properties of systems, the two main approaches explained will be differential equations (ODE), relying on a continuous and deterministic view of the world, and stochastic processes (CTMC), mainly relying on a discrete and stochastic view of the world.
Since the world is not totally discrete nor totally continuous, these attributes are better qualified as properties of our description of the world than of the world itself. Hence, a more suitable approach has to integrate discrete, continuous, stochastic, and deterministic ingredients. To this end, there will be defined a semantics for our modelling languages in terms of stochastic hybrid systems, flexible with respect of the amount of continuity and stochasticity introduced.
Once the theoretical framework is set up, analysis techniques to extract information from these models will be presented. Special emphasis will be given to the relationships between the different semantics (CTMC, ODE, hybrid) that can be attached to a PA program. In the latter direction, we will look at approximability results, providing conditions under which a discrete and stochastic model in terms of Continuous-Time Markov Chains (CTMC) converges to an ODE or an hybrid system, in the limit of large number of interacting entities.
From the point of view of analysis techniques, there will be discussed both general approaches like simulation and statistical model checking, and approaches more specific to the stochastic world, like moment closure techniques, also in the view of approximability theorems.
Syllabus (in Czech)
  • 1) Complex systems and their specification in process algebraic framework.
  • 2) BioPEPA and Stochastic Concurrent Constraint Programming languages and their semantics.
  • 3) Fundamental mathematical description: differential equations, stochastic processes. Hybrid semantics: integrating deterministic, stochastic and discrete views. Stochastic hybrid systems.
  • 4) Relationships between deterministic, stochastic and discrete semantics.
  • 5) Approximability results, hybrid limits of stochastic systems, relevant analysis techniques.
  • 6) Computational analysis: statistical model checking and moment closure techniques.
Literature
  • L. Bortolussi. Computational Systems Biology With Constraints. Stochastic modeling of biological systems with concurrent constraint programming. ISBN: 978-3-639-08875-5. VDM Verlag Dr. Mueller e.K., Germany, 2008.
  • L. Bortolussi and A. Policriti. Hybrid Systems and Biology. Continuous and Discrete Modeling for Systems Biology. In: M. Bernardo et al. eds, Formal Methods For Computational System Biology. (vol. 5016 of LNCS, Springer, pp. 424-448
Teaching methods (in Czech)
seminar lectures, exercises;
lectures will be realized in a block of 5 lectures which will run in the period May 21 - May 25 (the precise schedule will be announced by April at the latest)
Assessment methods
final homework
Language of instruction
English
Further comments (probably available only in Czech)
Study Materials
Teacher's information
http://www.dmi.units.it/~bortolu/
The course is also listed under the following terms Spring 2013.
  • Enrolment Statistics (Spring 2012, recent)
  • Permalink: https://is.muni.cz/course/fi/spring2012/DBLOK2