Exposés de la saison 2015-2016

Jeudi 17 septembre, 14h30 salle Markov

Serge Haddad (ENS Cachan, LSV)

Polynomial Interrupt Timed Automata

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éatrice Bérard (LIP6), Claudine Picaronny (LSV), Mohab Safey El Din (LIP6), and Mathieu Sassolas (LACL)

Jeudi 24 Septembre, 14h00 en salle Lipari

Tristan Charrier

Public announcements with mental programs

We propose a variant of arbitrary public announcement logic which is decidable. In this variant, knowledge accessibility relations are defined by programs. Technically, programs are written in dynamic logic with propositional assignments. We prove that both the model checking problem and the satisfiability problem are decidable and AEXP-pol-complete where AEXP-pol is the class of decision problems decided by alternating Turing machines running in exponential time where the number of alternations is polynomial. Whereas arbitrary public announcement logic is undecidable, our framework is decidable and we provide a proof-of-concept to show its expressiveness: we use our framework to reason about epistemic properties and arbitrary announcements when agents are cameras located in the plane.

Jeudi 1er octobre, 14h00 en salle Aurigny

Nicolas Markey

Optimal strategies in weighted timed games: undecidability and approximation

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, but the value problem (whether the optimal weight is less than a given value) had not been properly investigated. We prove that the value problem is undecidable as well, and introduce a large subclass of weighted timed games (to which the undecidability proof above applies) for which arbitrary-precise approximations of the optimal weight can be computed.
This is joint work with Patricia Bouyer and Samy Jaziri.

Jeudi 8 octobre, 14h00 en salle Aurigny

Sophie Pinchinat

Relating paths in transition systems: the fall of the modal mu-calculus

We revisit Janin and Walukiewicz's classic result on the expressive com- pleteness of the modal mu-calculus w.r.t. MSO , when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of MSO and the mu-calculus: MSO with path relation and the jumping mu-calculus. While "bounded-memory" binary relations bring about no extra expressivity to either of the two logics, "unbounded-memory" binary relations make the bisimulation-invariant fragment of MSO with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfect-information inhabits the gap.
This is joint work with Catalin Dima and Bastien Maubert

Jeudi 15 octobre, 14h00 en salle Minquiers

Uli Fahrenberg

Star-continuous Kleene omega-algebras for energy problems

Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on star-continuous Kleene omega-algebras, we show that some energy problems can be solved by algebraic manipulations on the transition matrix of energy automata. To this end, we prove general results about certain classes of finitely additive functions on complete lattices which should be of a more general interest.
This is joint work with Zoltán Ésik, Axel Legay and Karin Quaas which has been presented at ATVA'13, DLT'15 and FICS'15 and supported by ANR MALTHY. The talk will fall in two parts. First I will motivate and introduce star-continuous Kleene algebras and star-continuous Kleene omega-algebras, and in the second part I will apply this to energy problems.

Jeudi 12 novembre, 14h00 en salle Markov

Khalil Ghorbal

Characterizing Invariant Algebraic Sets for Polynomial Differential Equations

Given an explicit differential equation with a polynomial right hand side, we completely characterize its invariant algebraic sets. Thats is we give necessary and sufficient conditions for an algebraic set to be an invariant for the ODE at hand. Such characterization, so called, differential radical characterization, relies on a sound abstraction of the reachable set of the solutions by the smallest variety that contains it, that is the closure of the reachable set in the Zariski topology. It is furthermore computationally appealing as only the invariant candidate and its higher-order Lie derivatives are involved. It leads to a novel proof rule that is necessary and sufficient, which implies that invariance of algebraic equations over real-closed fields is decidable. Moreover, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NP-hard. The approach is applied to the formal verification of hybrid systems by allowing for precise and sound abstractions of the continuous part. of the system.

Jeudi 19 novembre, 14h00 en salle Aurigny

Yann Thierry-Meig

Symbolic model-checking using ITS-tools and model transformations

We present verification toolset ITS-tools, featuring a symbolic model-checking back-end engine based on hierarchical set decision diagrams (SDD) that supports reachability, CTL and LTL model-checking and a user-friendly eclipse based front-end. Using model transformations to a Guarded Action Language (GAL) as intermediate format, ITS-tools can analyze third party (Uppaal, Spin, Divine...) specifications. GAL specifications are tailored for symbolic analysis using decision diagrams, but can also be analyzed using other technologies such as SMT solvers.

Jeudi 26 novembre, 14h00 en salle Aurigny

Benedikt Bollig

Towards Formal Verification of Distributed Algorithms

Model checking is an automatic verification technique, which provides an answer to the question whether a program, given as a state-transition system, satisfies its specification, given in terms of a temporal-logic formula. Model checking is very well studied as far as boolean finite-state programs are concerned.
To take into account several sources of infinity such as an unknown number of processes or infinite data structures, the classical setting has been extended in several orthogonal directions. In the context of concurrent programs, one may ask whether a specification is satisfied independently of the number of participating processes. This question is referred to as parameterized verification. Second, a system may have to cope with variables ranging over an infinite domain such as the natural numbers or finite strings. Depending on the operations that are allowed on this domain, system executions can then be described as words over an infinite alphabet that is possibly equipped with one or several binary relations such as equality or a total order. Those words are usually referred to as data words. Many models and results from both areas, parameterized verification and data words, smoothly extend the classical finite-state approach and, in particular, provide decidable instances of the model-checking problem.
Our concern in this talk will be distributed algorithms, where an unknown number of (identical) processes cooperate to achieve a common goal. However, assuming perfectly identical processes, even simple tasks such as electing a leader cannot always be accomplished. One may, therefore, assume that every process is equipped with a unique process identifier from an unbounded domain, and that identifiers can be compared with one another wrt. a total order. Thus, when modeling distributed algorithms, one has to cope with both sources of infinity mentioned above: the number of processes and infinite data. This may be one reason why there have been only a few approaches to the formal verification of distributed algorithms.
In this talk, I survey recent developments in the areas of parameterized verification and data words, and we demonstrate how they can be exploited towards a framework for the formal verification of distributed algorithms.

Jeudi 3 décembre, Salle Petri/Turing

séminaire à l'occasion de l'HDR de B. Combemale

A journey from requirements, to development, to runtime management

https://intranet.irisa.fr/fr/actus/seminaire/journey-requirements-development-runtime-management

Jeudi 10 décembre, salle Minquiers

Benoît Caillaud

Structural Analysis of Multi-Mode DAE Systems

Multi-mode DAE systems are the underlying mathematical model supporting physical modeling languages such as Modelica. They consist of equations of the the form “when g do e”, where “g” are predicates and “e” differential algebraic equations. Reusing ideas borrowed from the constructive semantics of synchronous languages, we propose an abstract semantics of multi-mode DAE systems. This semantics is used to determine the structural differentiation index of a system and then compute a static scheduling of its equations, for all possible modes of the system.

Lundi 14 décembre, 14h, salle Sicile

Edon Kelmendi

Limit-sure reachability in a class of stochastic semiperfect-information games

We study two-player stochastic games with reachability conditions where the maximizer has no information whereas the minimizer has perfect-information. The question of limit-sure reachability is the following: is it true that for all epsilon>0 and finite-memory strategies tau (for the minimizer) there exists a finite word w (for the maximizer) such that the probability of reaching the final states is larger than 1-epsilon when the game unravels according to w and tau. This question is undecidable in general, the reason being that if the minimizer has no choice at all such a game is equivalent to a probabilistic finite automaton where the value 1 problem is undecidable. Building up on previous work on probabilistic finite automata we identify a robust class of games where the limit-sure reachability is decidable. We also show that there are games where the optimal strategies of the minimizer need infinite-memory which is slightly surprising since the minimizer has perfect-information.

Jeudi 7 janvier, 14h00 en Salle Minquiers

Pablo Rauzy

A formal approach to cryptosystems implementation security

Cryptosystems implementations are vulnerable to physical attacks, i.e., attacks that exploit side channels that are not modeled in classical cryptanalysis. Physical attacks can be classified into two categories. On one side, passive attacks, in which the attacker can read physical quantities (such as computation times, power consumption, or electromagnetic emanation) and then exploits the gathered information. On the other side, active attacks, in which the attacker can modify intermediate values of the computation (by injecting a fault with a laser, an electromagnetic pulse, or an intentional power glitch) and then use the faulted output value. In both cases, the attack may either significantly reduce the key space, or directly reveal the secret key. We are going to show how the formal approach can help to build robust systems in both settings. First, we will see an overview of my work on the automation and proof of a balancing countermeasure against power analysis on a block cipher. Then, we will see how formal methods enabled to prove and optimize countermeasures against the BellCoRe fault injection attack on CRT-RSA, and how, thanks to formal methods, we can build on these countermeasure to build better ones, and even leverage them to protect other asymmetric cryptography algorithms.

Jeudi 14 janvier, Salle Aurigny

Gregor Goessler

Blaming in component-based real-time systems

In component-based safety-critical real-time systems it is crucial to determine which component(s) caused the violation of a required system-level safety property, be it to issue a precise alert, or to determine liability of component providers. In this talk I will present an approach for blaming in real-time systems whose component specifications are given as timed automata. The analysis is based on a single execution trace violating a safety property P. We formalize blaming using counterfactual reasoning (“what would have been the outcome if component C had behaved correctly?”) to distinguish component failures that actually contributed to the outcome from failures that had no impact on the violation of P. I then show how to effectively implement blaming by reducing it to a model-checking problem for timed automata. If time permits I'll outline some recent work on fault ascription in concurrent systems.

Mardi 26 janvier, 15h en salle Minquiers

Jonathan Protzenko

The global sequence protocol: a memory model for distributed systems.

In the context of distributed memory models, one has to choose between consistency and performance. Sequentially consistent systems offer a compelling abstraction for the programmer, but require complex and costly synchronization between clients in order to guarantee consistency. If one is willing to give up strong consistency, then /eventual consistent/ models provide an alternative. Eventual consistency means the system /eventually/ reaches a state where all clients agree on the same sequence of operations; before that, though, each client may have local state that disagrees with other clients. Eventual consistency may model a processor with local caches and a central memory; it may also model a distributed cloud storage system with a central server and a variety of clients. Starting from a functional setting, I will introduce a very abstract model where clients send functions that fold over an initial state; then, I will move on to a more concrete, implementable model called GSP and show how to use it in a concrete application.

Jeudi 28 janvier

Gustavo Petri

Data-Driven Shape Inference

I will present an automated procedure for discovering expressive shape specifications for inductive data structures. In this approach we extract potential shape predicates based on the definition of constructors of arbitrary user-defined inductive data types, and combine these predicates within an expressive first-order specification language using a lightweight data-driven learning procedure. Notably, this technique requires no programmer annotations, and is equipped with a type-based decision procedure to verify the correctness of discovered specifications.

Jeudi 11 février, 14h00 en salle Markov

Ocan Sankur

Assume-Admissible Synthesis

we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. This rule is based on the notion of admissible strategies, well-known in game theory. Intuitively, admissible strategies are those that are maximal for a dominance relation defined between strategies. We illustrate how admissible strategies can be used to define ``reasonable'' behaviors of different components. We compare our synthesis rule with previous rules defined in the literature, and show that contrary to the previous proposals, it defines sets of solutions which are rectangular; this property leads to solutions which are robust and resilient, and allows one to synthesize strategies separately for each agent. We provide algorithms with optimal complexity and also an abstraction framework compatible with the new rule.
Joint work with Romain Brenguier and Jean-Francois Raskin.

Jeudi 18 février, 14h00 en salle Aurigny

Mickael Rabie

Time and Homonyms Considerations over Community Protocols

Guerraoui and Ruppert introduced the model of Community Protocols. This Distributed System works with agents having a finite memory and unique identifiers (the set of identifiers being ordered). Each agent can store a finite number of identifiers they heard about. The interactions are asynchronous and pairwise, following a fair scheduler. The computation power of this model is fully characterized: it corresponds exactly to what non deterministic Turing Machines can compute on a space O(n\log n). In this talk, I will focus on two restrictions of the model: The first is what happens when agents may share identifiers, the population admitting homonyms. I will introduce a hierarchy, with characterizations depending on the rate of unique identifiers present in the population. The main result is that with log n identifiers, a Turing Machine with a polylogarithmic space can be simulated. The second consider the following time restriction: what can be computed in a polylogarithmic number of parallel interactions. This version is not yet characterized, but I will provide some impossibility results, some computable protocols, and I will give the tighter bound we found.

Jeudi 25 février en salle Minquiers

Hans van Ditmarsch (LORIA)

Epistemic Gossip Protocols

A well-studied phenomenon in network theory since the 1970s are optimal schedules to distribute information by one-to-one communication between nodes. One can take these communicative actions to be telephone calls, and protocols to spread information this way are known as gossip protocols or epidemic protocols. Statistical approaches to gossip have taken a large flight since then, witness for example the survey "Epidemic Information Dissemination in Distributed Systems" by Eugster et al. (IEEE Computer, 2004). It is typical to assume a global scheduler who executes a possibly non-deterministic or randomized protocol. A departure from this methodology is to investigate epistemic gossip protocols, where an agent (node) will call another agent not because it is so instructed by a scheduler, but based on its knowledge or ignorance of the distribution of secrets over the network and of other agents' knowledge or ignorance of that. Such protocols are distributed and do not need a central scheduler. This comes at a cost: they may take longer to terminate than non-epistemic, globally scheduled, protocols. A number of works have appeared over the past years (Apt et al., Attamah et al., van Ditmarsch et al., van Eijck & Gatting, Herzig & Maffre) of which we present a survey, including open problems yet to be solved by the community.

Pere Pardo (LORIA)

Dynamic Gossip: protocols characterization

In this talk we will present Dynamic Gossip, a dynamic extension of the classical Gossip Problem and some results on protocols definable in this dynamic extension. In classical Gossip problems, each agent in a group has a secret, and the goal of these agents is that everyone learns all the secrets, using only phone calls. Each call involves two agents, who will exchange all the secrets learnt so far. In Dynamic Gossip, the agents also exchange the phone numbers they know, thereby enabling new phone calls after a call.
A Dynamic Gossip protocol is then a procedure for spreading the secrets and numbers in a graph or network of agents; for example, agents can only make calls to an agent in their contact list whose secret is not yet known to them. We will survey this and other examples of Dynamic Gossip protocols, and talk about their characterization results, that is, the class of graphs where these protocols necessarily (or possibly) succeed.

Mardi 1er mars, 14h00 en salle Petri

Loig Jezequel

Lazy Reachability Analysis in Distributed Systems

We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in an early prototype and provide some very encouraging experimental results.

Jeudi 10 mars, 14h en salle Markov

Nathanaël Fijalkow (Oxford University)

Online Space Complexity

The notion of online space complexity, introduced by Karp in 1967, quantifies the amount of space required to solve a given problem using an online algorithm. Our original motivation was to study a claim of Rabin about the online space complexity of probabilistic automata. I will start by this motivating example.
Our main contribution is to devise a generic lower bound technique relying on boundedly generated lattices of languages, and two methods to apply it, one involving combinatorics on words and the other linear algebra. We give two applications of this technique. The first is to prove that the polynomial hierarchy of alternating automata is infinite. The second is to prove that the language of prime numbers written in binary does not have sublinear alternating online space complexity. This strengthens a result of Hartmanis and Shank from 1968, which implied a logarithmic lower bound for the same model. We obtain as a corollary that the primality of a number written in binary cannot be determined by a streaming alternating Turing machine using sublogarithmic space.

Jeudi 17 mars, 14h en salle Aurigny

Philippe Schnoebelen (LSV)

Well-Structured Systems: Algorithms and Complexity

Well-structured systems, aka WSTS, are a family of infinite-state computational models that support generic decidability results based on well-quasi-ordering theory. They have many applications in logics of programs and verification. In this talk we present a modern version of the basic WSTS algorithms and describe new techniques for the complexity analysis of WSTS models.

mercredi 23 mars, 11h en salle Aurigny

Sophie Pinchinat

Unifying Hyper and Epistemic Temporal Logics

In the literature, two powerful temporal logic formalisms have been proposed for expressing information-flow security requirements, that in general, go beyond regular properties. One is classic, based on the knowledge modalities of epistemic logic. The other one, the so-called hyper logic, is more recent and subsumes many proposals from the literature. In an attempt to better understand how these logics compare with each other, we consider the logic KCTL* (the extension of CTL* with knowledge modalities and synchronous perfect recall semantics) and HyperCTL*. We first establish that KCTL* and HyperCTL* are expressively incomparable. Then, we introduce a natural linear past extension of HyperCTL*, called HyperCTL* full past, that unifies the two former logics. It turns out that the model-checking problem for HyperCTL* full past is decidable, for an exact computational complexity in terms of a quantifiers' alternation. Do to lack of time, we will not adress this last point.

Jeudi 31 mars, 14h en salle Aurigny

Simon Lunel

A Sequent Calculus for a Modal Logic on Finite Data Trees

We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e. over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem. Joint work with David Baelde and Sylvain Schmitz

Jeudi 7 avril, 14h, salle Aurigny

Mickael Randour (ULB)

Reachability in Networks of Register Protocols under Stochastic Schedulers

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous 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 any 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.

mercredi 20 avril, 14h

Vlad Rusu

Incremental Language-Independent Program Verification

Reachability Logic (RL) is a recently introduced formalism for defining the operational semantics of programming languages and for specifying program properties. As a program logic RL can be seen as a language-independent generalisation of Hoare Logics. Thus, using RL one can specify programs independently on the languages in which the programs are written and one can design program-verification techniques that are also language-independent. Several such techniques have already been proposed, all of which have a circular nature: they take as input a set of RL formulas (specifying a given program that one wants to verify, as well as some of its subprograms), and allow formulas in the set to be circularly used in proofs of other formulas, or even in their own proof. Such circular reasoning is essential for dealing with repetitive behaviour (e.g., loops or recursive calls). The reasoning is sound, but only in a monolithic way, in the sense that if a proof succeeds on a given set of formulas then all the formulas in the set are semantically valid; but if the proof fails, then nothing can be inferred about any formula’s validity or invalidity. In practice, this means that one is left with no information after unsuccessful proof attempts. In this work we deal with this issue by proposing an incremental method for proving RL formulas. The proposed method takes as input a given formula specifying a given program fragment, together with a (possibly empty) set of helper formulas that specify some if its subprograms and that are were already proved valid (e.g., using our method or any other sound method). Then, certain conditions equivalent to RL formula validity are automatically checked. In case of success, the newly proved formula can be incrementally used as a helper in the proofs of other formulas, thereby proving increasingly larger program fragments. But in case of failure, unlike the case of monolithic methods, one is not left without information - one still knows the validity of the already proved helper formulas, and can build on this knowledge to make progress in the program's proof. We illustrate the approach by successfully verifying the nontrivial Knuth-Morris-Pratt string-matching algorithm, whose verification had previously been tried without success using a monolithic method. (common work with Andrei Arusoaie)

Jeudi 28 avril, 14h00 en salle Aurigny

Yannick Chevalier

Vers la synthèse de composants sécurisés

Lors d'Usenix Enigma 2016, le directeur de l'équipe d'"accès sur mesure" de la NSA a fait une liste des failles privilégiées permettant d'entrer dans un système. En dehors de l'ingénierie sociale, le point d'entrée privilégié dans les systèmes informatique est dans l'écart qui existe entre les composants (protocoles, logiciels,...) que les administrateurs systèmes ont voulu déployer et les logiciels réellement existants. Cette différence vient de la perpétuation de composants obsolètes, de la non-application de patches, mais aussi de composants n'implémentant pas fidèlement leur spécification. Cet exposé portera sur ce dernier point, et sur les travaux ouvrant la voie vers la synthèse sécurisé de composants communiquants, parmi lesquels des protocoles cryptographiques ou des services et applications Web. Cet exposé portera dans un premier temps sur la définition d'une sémantique opérationnelle à partir d'une déclaration d'échanges de messages (travail commun avec Michaël Rusinowitch), et dans un second temps de techniques de synthèse de service lorsqu'il est fait abstraction des messages. Les travaux futurs consisteront à combiner ces deux approches pour générer automatiquement des implémentations de protocoles et de services à partir de composants sécurisés déjà prouvés.

Vendredi 29 avril, 14h00 en salle Aurigny

Antonio Carzaniga

Descriptors, Locators, Identifiers: Multi-Modal Addressing in the TagNet Information-Centric Networking Architecture

A truly information centric network is one where addresses are given by applications (users), not by the network. Application-defined addresses make applications easier to write and to deploy, but on the other hand such addresses might not aggregate very well, which then limits the scalability of routing and forwarding. This is a crucial dilemma: how to architect a network so that applications can benefit from expressive and flexible addressing, and at the same time the network can scale. In this talk I will present the approach we took to solve this dilemma within the TagNet architecture. TagNet supports two distinct types of addresses at the network level: descriptors and locators. Descriptors are expressive and are fully application-defined, while locators are opaque network-level addresses. TagNet also distinguishes the role of identifiers, which play a fundamental role in caching and transport protocols, but not in routing and forwarding. With these three concepts, TagNet supports both push and pull communication, and, I will argue, it can do that with scalable routing and forwarding.

Jeudi 12 mai, 14h00 en salle Aurigny

Charlotte Truchet

AbSolute, a constraint solver without constraints

The goal in Constraint Programming (CP) is to solve combinatorial problems (usually NP-hard), described by first-order logic predicates, the constraints. Each variable of the problem belongs to a given, often finite, set of values: its domain. In CP, the variables domains over-approximate the solution set, and they are considered independent, the relations between the variables being expressed by the constraints only. Hence, the search space is always a Cartesian product of some base set (intervals or set of integers). In this talk, we present AbSolute, a constraint solver using Abstract Interpretation techniques. Precisely, our constraint solver is based on abstract domains, as they have been defined in Abstract Interpretation (AI) in order to over-approximate the traces of a program. AI abstract domains more expressive than CP ones. In particular, they can be Cartesian or relational (octagons, polyhedra, etc.). In addition, different abstract domains can be used in a collaborative way in the same solver, in particular real and integer ones. AbSolute has been implemented on top of Apron, an abstract domain library. Experimental results show promising performance improvements on a classical benchmark.

Jeudi 26 mai, 14h00 en salle Aurigny

Laurie Ricker (Mnt Allisson University)

Incremental Verification of Co-observability in Discrete-Event Systems.

Existing strategies for verifying co-observability, one of the properties that must be satisfied for synthesizing solutions to decentralized supervisory control problems, require the construction of the complete system model. When the system is composed of many subsystems, these monolithic approaches may be impractical due to the state-space explosion problem. To address this issue, we introduce an incremental verification of co-observability approach. Selected subgroups of the system are evaluated individually, until verification of co-observability is complete. The new method is potentially much more efficient than the monolithic approaches, in particular for systems composed of many subsystems, allowing for some intractable state-space explosion problems to be manageable.

Jeudi 9 juin, 14h00 en salle Markov

Olivier Carton (IRIF)

L'aléatoire à la sauce automate

We strengthen the theorem that establishes that deterministic finite transducers can not compress normal infinite words. We prove that, indeed, non-deterministic finite transducers, even augmented with a fixed number of counters, can not compress normal infinite words. However, there are push-down non-deterministic transducers that can compress normal infinite words. We also obtain new results on the preservation of normality with automata selectors. Complementing Agafonov's theorem for prefix selectors, we show that suffix selectors also preserve normality. However, there are simple two-sided selectors that do not preserve normality.
Joint work with V. Becher and P. Heiber (University of Buenos Aires)

Jeudi 23 juin, 14h00 en salle Markov

Pierre-Evariste Dagand (LIP6)

Verifying Clock-Directed Modular Code Generation for Lustre

The correct compilation of block diagram languages like Lustre, SCADE, and the discrete subset of Simulink is important since they are used to program critical embedded control software. This talk addresses the compilation pass that transforms synchronous dataflow programs into imperative ones. The challenge is to move from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where they perform stateful computations. We specify and verify in the Coq interactive theorem prover a code generator that handles the key aspects of Lustre, namely sampling, nodes and delays. Our solution introduces a novel intermediate model that combines features of the dataflow and imperative models.
This talk describes joint work with Timothy Bourke, Marc Pouzet, and Lionel Rieg.

Jeudi 7 juillet, 14h00 en salle Sicile

Maximilien Colange (LSV)

Symbolic Optimal Reachability in Weighted Timed Automata

Weighted timed automata have been defined in the early 2000’s for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this talk, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.
Joint work with Patricia Bouyer and Nicolas Markey.