Journée “Parametric Analyses of Concurrent Systems” le 26 mai 2016

Journée commune AFSEC/PACS (ANR PACS : Parametric Analyses of Concurrent Systems)

Pour définir la taille de la salle et prévoir les autorisations d'accès au bâtiment , une inscription (gratuite) au plus tard le 10 mai 2016 est nécessaire en envoyant un email à olivier-h.roux@irccyn.ec-nantes.fr ; objet : "Inscription AFSEC 26 mai" (cliquer sur le lien) - préciser : Nom et Affiliation.

Quand: Le 26 mai 2016
Lieu: Université Paris Diderot / IRIF

Programme (en cours d'élaboration) :

• 10h-11h Polynomial Interrupt Timed Automata (Serge Haddad, LSV - ENS Cachan)
• Résumé: Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA.
  Joint work with B. Bérard (LIP6), C. Picaronny (LSV) , M. Safey El Din (LIP6) and M. Sassolas (LACL).
• 11h-12h Symbolic Robustness Analysis of Timed Automata. (Ocan Sankur, IRISA - Rennes)
• Résumé:
  We study the robust safety problem for timed automata under guard imprecisions which consists in computing a bound on the perturbations on delays under which a safety specification holds. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its performance in comparison with a recently published one, and with a binary search on enlargement values.
• 14h-15h Reachability in Networks of Register Protocols under a Fair Stochastic Scheduler (Arnaud Sangnier, LIAFA - Paris 7)
• Résumé: We study the almost-sure reachability problem in a distributed system
  obtained as the asyn- chronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
  This is a joint work with Patricia Bouyer, Nicolas Markey, Mickael Randour and Daniel Stan.
• 15h-16h Controlling Actions and Time in Parametric Timed Automata (Laure Petrucci, LIPN - Paris 13)
• Résumé:
  Cyber-physical systems involve both discrete actions and real-time that elapses depending on timing constants.
  In this paper, we introduce a formalism for such systems containing both real-time parameters in linear timing constraints and switchable (Boolean) actions.
  We define a new approach for synthesizing combinations of parameter valuations and allowed actions, under which the system correctness is ensured when expressed in the form of a safety property.
  We apply our approach to a railway crossing system example with a malicious intruder potentially threatening the system safety.