PAMPAS: Parallel Algorithms for Model-checking and Parameter Synthesis

Funded by: EP NUFFIC - Van Gogh programme
Duration: February 2018 until February 2019
Contact: prof.dr. J.C. van de Pol

Summary of the project

The scientific goal of PAMPAS is to invent new parallel algorithms for synthesising the parameters of quantitative models for realistic applications. These parameters control the time intervals in which events can happen, as well as the probability of their occurrence. Technically, we study extensions of Markov Chains and Timed Automata.

Applications: Quantitative analysis of ICT systems plays a crucial role in assessing their reliability, security, energy usage, and proper timing behaviour. We follow a model-based approach, in which the distributed ICT system (with its physical or socio-technical context) is modelled and analysed before it is being implemented. Recently, we extended this approach to also cover maintenance strategies. Finally, we are collaborating with biologists, since timed and probabilistic models appeared to be very fruitful in studying biological models of signalling networks as well.

Parallel Algorithms: The models that we are dealing with are hard to analyse. This is caused by the “state space explosion” due to inherent concurrency in the systems, and also due to the combinatorial parameter space. To scale our approach to realistic systems, we have designed parallel algorithms to analyse plain models. In PAMPAS, we intend to extend these algorithms to the synthesis of model parameters, in order to deduce the time and probability intervals under which the modelled systems are functioning correctly, e.g., avoiding bad situations (safety) or guaranteeing required behaviour (liveness).

The Challenge: Designing parallel algorithms in a correct and efficiently scalable manner is very intricate. In order to come up with good solutions for the parameter synthesis problem, we propose to combine forces of the labs in Twente and Paris. Both groups bring complementary skills in multicore algorithms (Twente) and parameter synthesis (Paris). Also, both groups bring in their own models from the reliability engineering domain and from systems biology.

	Home > Research > Projects
<< EEMCS (EWI) Home News and Events People Research » Projects » Publications » Tools Education Vacancies Intranet Contact	PAMPAS: Parallel Algorithms for Model-checking and Parameter Synthesis Funded by: EP NUFFIC - Van Gogh programme Duration: February 2018 until February 2019 Contact: prof.dr. J.C. van de Pol Summary of the project The scientific goal of PAMPAS is to invent new parallel algorithms for synthesising the parameters of quantitative models for realistic applications. These parameters control the time intervals in which events can happen, as well as the probability of their occurrence. Technically, we study extensions of Markov Chains and Timed Automata. Applications: Quantitative analysis of ICT systems plays a crucial role in assessing their reliability, security, energy usage, and proper timing behaviour. We follow a model-based approach, in which the distributed ICT system (with its physical or socio-technical context) is modelled and analysed before it is being implemented. Recently, we extended this approach to also cover maintenance strategies. Finally, we are collaborating with biologists, since timed and probabilistic models appeared to be very fruitful in studying biological models of signalling networks as well. Parallel Algorithms: The models that we are dealing with are hard to analyse. This is caused by the “state space explosion” due to inherent concurrency in the systems, and also due to the combinatorial parameter space. To scale our approach to realistic systems, we have designed parallel algorithms to analyse plain models. In PAMPAS, we intend to extend these algorithms to the synthesis of model parameters, in order to deduce the time and probability intervals under which the modelled systems are functioning correctly, e.g., avoiding bad situations (safety) or guaranteeing required behaviour (liveness). The Challenge: Designing parallel algorithms in a correct and efficiently scalable manner is very intricate. In order to come up with good solutions for the parameter synthesis problem, we propose to combine forces of the labs in Twente and Paris. Both groups bring complementary skills in multicore algorithms (Twente) and parameter synthesis (Paris). Also, both groups bring in their own models from the reliability engineering domain and from systems biology.