DBLOK2 Seminar on Formal Methods for Complex Systems

Fakulta informatiky
jaro 2012
Rozsah
0/2/0. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Luca Bortolussi, Ph.D. (přednášející), doc. RNDr. David Šafránek, Ph.D. (zástupce)
doc. RNDr. David Šafránek, Ph.D. (přednášející)
Garance
prof. Ing. Václav Přenosil, CSc.
Katedra strojového učení a zpracování dat – Fakulta informatiky
Dodavatelské pracoviště: Katedra strojového učení a zpracování dat – Fakulta informatiky
Rozvrh
Po 21. 5. 14:00–17:00 B410, Út 22. 5. 10:00–13:00 B410, St 23. 5. 10:00–13:00 B410, Čt 24. 5. 10:00–13:00 B410, Pá 25. 5. 10:00–13:00 B410
Předpoklady
Elementary knowledge of formal methods, stochastic processes and process algebras is welcome.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20
Mateřské obory/plány
Cíle předmětu
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.
Osnova
  • 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.
Literatura
  • 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
Výukové metody
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)
Metody hodnocení
final homework
Vyučovací jazyk
Angličtina
Informace učitele
http://www.dmi.units.it/~bortolu/
Organization notes: 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).

Abstract: Complex systems, i.e. systems made of many components interacting in intricated patterns, are ubiquitous in the world, from the biochemical machinery of a cell to the socio-technical networks that are becoming more and more central in everyday life. Understanding them is not possible without the aid of proper mathematical and computational instruments. In particular, the exceptional complexity of these systems is a challenge for the current state of the art in mathematical and computational modelling. Overcoming these limits requires surely new ideas, but also a careful integration of the approaches currently available. There are three main pillars upon which basing a formal treatment of complex systems: the language used to describe them, the mathematical theory to (automatically) construct models, and the analytical and computational tools available to analyze such models. Integrating different approaches is not only central in constructing software for model building and model analysis, but it is also relevant from a theoretical point of view, as connecting different approaches may provide insights to increase our ability to tackle the complexity of such systems.
Další komentáře
Studijní materiály
Předmět je zařazen také v obdobích jaro 2013.