Prochain Exposé
June 2nd, 10AM (Paris/France). Webinar
Xiong Xu (Institute of Software, Chinese Academy of Sciences, China)
Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP
Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction however poses significant challenges. To address these issues, Hoare and He’s Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-Order UTP (HUTP) is a conservative extension to Hoare and He’s theory which supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for HCSP (Hybrid Communicating Sequential Processes) and Simulink using HUTP.
Exposés des semaines suivantes
June 9th, 3PM (Paris/France). Webinar
Damien Busatto-Gaston (Université Libre de Bruxelles)
On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows.
In this talk I will present recent work on Markov decision processes. Given an MDP and a formula phi, the strategy synthesis problem asks if there exists a strategy for the MDP such that the resulting Markov chain satisfies phi. This challenging problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced globally. Moreover, we allow for linear expressions in the probabilistic inequalities. We show that this class of formulae is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis becomes decidable when strategies are either deterministic or memoryless, while the general problem remains undecidable. We compare with results on the entire PCTL logic and consider applications to the PCTL satisfiability problem.
June 30th, 3PM (Paris/France). Salle Petri-Turing
Helge Spieker (Simula Research Laboratory in Oslo, Norway)
TBA.
TBA.
Vos propositions sont les bienvenues !
