Exposés de la saison 2013-2014

Jeudi 12 septembre, 14h30 en salle Markov

Srinivas Pinisetty (SUMO)

Runtime Enforcement of Timed Propreties

Runtime enforcement is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies to a property. Runtime enforcement has been extensively studied over the last decade in the context of untimed properties. In this talk, we introduce runtime enforcement of timed properties. We revisit the foundations of runtime enforcement when time between events matters. Proposed runtime enforcers are time retardant: to produce an output sequence, additional delays are introduced between the events of the input sequence to correct it. We show how runtime enforcers can be synthesized for any safety or co-safety timed property. Finally, we briefly describe about some potential applications, and possibilities of extending the enforcement mechanism for more general properties such as response.

Mardi 17 septembre, 11h00 en salle Markov

Yann Thierry-Mieg (LIP6)

A Guarded Action Language to express system semantics.

Symbolic data structures such as decision diagrams have proved successful for model-checking. However, expressing systems in a symbolic manner to take full advantage of these data structures usually requires a high level of expertise.
Based on Instantiable Transition System (ITS) that enables composition of specifications, we define the Guarded Action Language (GAL). GAL is a simple yet expressive formalism, allowing to model concurrent systems manipulating complex data types such as integers and arrays with a C-like syntax. This framework is supported by very efficient decision diagrams for model-checking.
We show how several formalisms featuring both time and data manipulation can be easily translated to GAL/ITS, and show through performance comparisons that our approach is competitive with other solvers.

Jeudi 26 septembre

Pas de séminaire cette semaine, en raison de la conférence RV'2013

Les sujets abordés durant RV'2013 sont proches des centres d'intérêt du séminaire. Le séminaire fait donc relâche cette semaine. Voir rv2013.gforge.inria.fr pour plus d'information.

Mardi 1er Octobre, 14h30 en salle Markov

Madhavan Mukund (Chennai Mathematical Institute)

Deterministically Communicating MDPs

The formal verification of large probabilistic models remains a challenge. Exploiting the concurrency that is often present is one way to address this problem. Here we study a restricted class of networks of Markov Decision Processes (MDPs) whose actions consist of synchronizations which in turn determine the local probability distribution for their next moves. The restriction we impose is that the synchronizations are deterministic in the sense that two simultaneously enabled synchronizations are required to involve disjoint sets of MDPs. As a result, one can define the global behaviour of a DMDP as a Markov chain without having to introduce schedulers. In order to cope with the exponential size of this Markov chain in the number of components, we define an interleaved semantics in terms of the local synchronization actions. The network structure induces an independence relation on these actions. Using Mazurkiewicz trace theory, we establish a strong relationship between the interleaved semantics and the global Markov chain semantics. This allows us to construct a natural probability measure with respect to the interleaved semantics. Consequently, verification of DMDPs can often be efficiently carried out using the interleaved semantics without having to construct the global Markov chain. To illustrate this we develop a statistical model checking (SMC) procedure under the interleaved semantics and use it to verify a probabilistic algorithm for leader election over an anonymous ring. This is joint work with Sumit Kumar Jha, Ratul Saha and P.S. Thiagarajan.

Jeudi 10 octobre, 14h30 en salle Markov

Andrei Paskevich

Deductive Program Verification with Why3

We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, exceptions, and ghost code. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that obviates the use of a memory model. Verification conditions are discharged by Why3 with the help of various existing automated and interactive theorem provers. A rich set of proof task transformations is implemented in Why3 to ensure sound translation of proof obligations to the language and logic of the back-end provers. A user can program directly in WhyML and get correct-by-construction OCaml programs via an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

Jeudi 17 octobre, 14h30 en salle Aurigny

Francesco Belardinelli

Verification of Auctions as Artifact Systems: Decidability via Finite Abstraction

Artifact Systems are a novel paradigm in business processes that has recently received considerable attention in service-oriented computing. Artifact Systems (AS) are best described in terms of interacting modules, or artifacts, consisting of a data model and a lifecycle, which account respectively for the relational structure of data and their evolutions over time. However, by considering data and processes as equally relevant tenets of AS, the typical questions concerning the verification of these services can no longer be solved by current methodologies, as the presence of data means that the number of states in AS is infinite in general. In this talk we show that the framework of Artifact Systems can be applied fruitfully to game-theoretic scenarios. Specifically, we provide a formalisation of English (ascending bid) auctions as an AS. Then, we present agent-based abstraction techniques to model check AS against specifications written in a temporal-epistemic logic, thus obtaining decidability results for the auction scenario in question. The research presented in this talk includes joint work with Prof A. Lomuscio and Dr F. Patrizi and it has been partially funded by the EU STREP Project ACSI.

Mardi 22 Octobre

Pierre Bourhis (CNRS - LIFL - INRIA Lille)

The Impact of Disjunction on Query Answering Under Guarded-Based Existential Rules.

We study the complexity of conjunctive query answering under (weakly-)(frontier-)guarded disjunctive existential rules, i.e., existential rules extended with disjunction, and their main subclasses, linear rules and inclusion dependencies (IDs). Our main result states that conjunctive query answering under a fixed set of disjunctive IDs is 2exptime-hard. This quite surprising result together with a 2exptime upper bound for weakly-frontier-guarded disjunctive rules, obtained by exploiting recent results on guarded negation first-order logic, gives us a complete picture of the computational complexity of our problem. We also consider a natural subclass of disjunctive IDs, namely frontier-one (only one variable is propagated), for which the combined complexity decreases to exptime. Finally, we show that frontier-guarded rules, combined with negative constraints, are strictly more expressive than DL-LITE-H-Bool, one of the most expressive languages of the DL-Lite family. We also show that query answering under DL-LITE-H-Bool is 2exptime-complete in combined complexity.

Jeudi 7 novembre, 14h30 en salle Markov

Sylvain Schmitz (LSV)

The Complexity of Vector Addition Games

Vector addition games are obtained by endowing vector addition systems with fork rules. Initially introduced in the study of propositional linear and relevance logics, they have more recently gathered attention in an emerging quantitative theory of verification and synthesis as multi-dimensional energy games. We show that finding the winner of such a game with a parity condition is 2ExpTime-complete. As an application, we show that the same complexity result applies to the problem of whether a there exists a simulation between a vector addition system and a finite-state system.
Joint work with Jean-Baptiste Courtois.

Jeudi 21 novembre, 14h30 en salle Aurigny

Yann Régis-Giana

Certifying and reasoning about the concrete complexity of programs

A cost annotating compiler is a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. In this talk, we present a so-called labelling method to answer the following two natural questions: (i) How to prove that these cost annotations are sound and precise? (ii) How to use these cost annotations to derive synthetic and parametric bounds on the concrete execution of programs?

Mardi 26 novembre, 10h30 en salle Petri/Turing

Joel Ouaknine, Oxford University

Decision Problems for Linear Recurrence Sequences

Linear recurrence sequences (such as the Fibonacci numbers) permeate a vast number of areas of mathematics and computer science (in particular: program termination and probabilistic verification), and also have many applications in other fields such as economics, theoretical biology, and statistical physics. In this talk, I will focus on three fundamental decision problems for linear recurrence sequences, namely the Skolem Problem (does the sequence have a zero?), the Positivity Problem (are all terms of the sequence positive?), and the Ultimate Positivity Problem (are all but finitely many terms of the sequence positive?). This is joint work with James Worrell.

Jeudi 28 novembre, 15h30 en salle Aurigny

Benoit Valiron

Toward a formal analysis of quantum algorithms

The field of quantum algorithms is vibrant. Nevertheless, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and is able to generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.

Jeudi 5 décembre, 14h30 en salle Markov

Jérôme Leroux (LABRI)

Acceleration for Petri Nets

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flatable, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set. In this presentation, the framework of verification of infinite-state systems based on acceleration techniques is recalled. We also explain the completeness of this method on the computation of Presburger formulas denoting the reachability sets of Petri nets.

Jeudi 12 décembre, 14h30 en salle Markov

M. Praveen (LABRI)

Reasoning about data repetitions with counter systems

We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2-EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a poten- tially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.

Jeudi 19 décembre, 14h30 en salle Markov

Christophe Chareton (ONERA)

Updatable Strategy Logic

In this talk, we present a temporal multi-agent logic called Updatable Strategy Logic (USL) which subsumes the main propositions in this area, such as ATL-ATL*, ATLsc and SL. These logics allow to express the capabilities of agents to ensure the satisfaction of temporal properties. USL mainly differs from SL in two ways. Semantically, the notion of strategy composition is extended to enable an agent to refine her strategy, that is to update it without revoking it. Syntactically, a new operator, called "unbinder", is introduced: it allows an agent to explicitly revoke a strategy, whereas revocation is implicit in SL. USL allows to express new properties of interactions between coalitions of agents and new properties of comparisons between strategies. A predicate of equality is made expressible. It also allows to introduce a notion of « sustainability » for the capabilities of agents to achieve objectives, a sustainable capability for an agent being a capability that still holds even after it has been employed. This makes USL strictly more expressive than SL.

Jeudi 16 janvier, 14h30-18h00

Mini workshop

Modal logics and rational relations

On the occasion of Bastien Maubert's PhD defense, a mini workshop with talks from members of his jury is organized.

14h30-15h15 : François Schwarzentruber : Big Brother Logic

Logical modeling and reasoning about agents equipped with surveillance cameras in the plane (work with Olivier Gasquet and Valentin Goranko)

We consider multi-agent scenarios where each agent controls a surveillance camera positioned in the plane, with fixed position and angle of view, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other's observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language. We introduce 3 different but equivalent versions of the semantics for these languages, discuss their expressiveness and provide translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for the basic logic BBL that we introduce here and for some of its extensions. Notably, we show that even for the extension with common knowledge, model checking remains in PSPACE. Finally, we discuss some further extensions: by adding obstacles, positioning the cameras in 3D or enabling them to change positions. Our work has potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multi-robot systems.

15h15 - 16h00 : Catalin Dima : Asymptotic behavior in temporal logic.

We study the approximability of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to infinity. More specifically, for formulas in the fragments PLTL+ and PLTL- of the Parametric Linear Temporal Logic of Alur et al., we provide algorithms for computing the limit entropy as all parameters tend to infinity. As a consequence, we can decide the problem whether the limit entropy of a formula in one of the two fragments coincides with that of its time- unbounded transformation, obtained by replacing each occurrence of a time-bounded operator into its time-unbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discrete-time timed automata and analysis of their strongly-connected components.

The talk is based on joint work with E. Asarin, M. Blockelet, A. Degorre and Ch. Mu, which was partly supported by the French ANR project EQINOCS.

16h15 - 17h00 : Christof Loeding : The synthesis problem for word transducers

We consider automatic and rational relations, which are defined by synchronous and asynchronous two-tape word automata, respectively. Viewing such relations as specifications, we study the question whether these specifications can be implemented by deterministic word transducers: Given an automatic (or rational) relation, decide whether there exists a deterministic word transducer that computes a function compatible with the relation. We show that the problem is undecidable for rational relations and decidable for automatic relations.

Jeudi 23 janvier, 14h30 en salle Aurigny

Ivan José Vazinczak (Centre for Artificial Intelligence Research - South Africa)

Towards a Multifarious Qualitative Analysis of Uncertainty in Reasoning

The last few decades have seen the development of a whole variety of logics, extending or modifying classical logic to deal with many different notions and problems, motivated by philosophical as well as practical needs. These involve different modes of reasoning such as reasoning with uncertainty, exceptions, similarity, vagueness, incomplete information and many others, usually referred to as qualitative uncertain reasoning (or, more commonly, nonmonotonic reasoning). Notwithstanding all the progress that has been achieved, some important facets of nonmonotonicity in logic have largely been overlooked or have only been partially treated so far. To witness, the literature on nonmonotonic reasoning has focused almost exclusively on nonmonotonicity of conditional forms; the question as to which notions of nonmonotonic entailment are most appropriate in given contexts remains open, and belief revision paradigms are largely restricted to an underlying classical (Tarskian) consequence relation. Moreover, well-established approaches are largely based on propositional languages or haunted by the undecidability of full first-order logic. Modern applications require formalisms with a good balance between expressive power and computational complexity. Even if some of the issues related to uncertainty in reasoning have been studied using probabilistic approaches and statistical methods, their qualitative computational nature remains a large avenue for exploration. Therefore, there is a need to investigate and design new general logical methods with which one can better understand, formalize and get to grips with the different aspects of nonmonotonicity in reasoning at all its different levels. In this talk we shall (i) attempt to depict a coherent picture of qualitative uncertain reasoning in all its forms; (ii) give an overview of our recent contributions towards such a unifying theory, and (iii) provide directions for further exploring the questions that still remain open.

Mardi 28 janvier, 14h30 en salle Aurigny

Didier Dubois IRIT, Université Paul Sabatier

La logique possibiliste généralisée

Nous présentons un cadre logique minimal qui permet de raisonner avec des formules booléennes qualifiées par des bornes inférieures de degrés de nécessité ou de possibilité. Il s'agit d'un langage propositionnel enchâssé dans un autre qui qualifie les propositions du premier. La version tout-ou-rien de ce cadre correspond à une logique épistémique élémentaire MEL dont la syntaxe est un fragment de la logique modale KD, et dont un fragment permet de capturer les logiques tri-valuées de Lukasiewicz et de Kleene. Sa sémantique se décline en termes de sous-ensembles d'interprétations du langage propositionnel. La version valuée de cette logique épistémique généralise la logique possibiliste et sa sémantique est en termes de familles de distributions de possibilité. Nous montrons la complétude de cette logique par rapport à cette sémantique possibiliste. Ce formalisme permet de capturer la logique d'équilibre de Pearce, et partant, les formules de l'answer-set programming. L'intérêt de cette traduction est de visualiser le sens intuitif de ces règles dans la syntaxe et de fournir une sémantique non-procédurale, mais plus proches de la sémantique des modèles, et plus intuitive, en termes d'information incomplète. Plus généralement, ce cadre logique peut servir de base à une vision unifiée des représentations de l'incertain, raisonnement par défaut, de la croyance etc...

Jeudi 6 février, 14h30 en salle Aurigny

Doron Peled (Bar-Ilan University)

Synthesis using genetic programming based on Model Checking

We show how the use of genetic programming, in combination of model checking and testing, provides a powerful way to synthesize programs. Whereas classical algorithmic synthesis provides alarming high complexity and undecidability results, the genetic approach provides a surprisingly successful heuristics. We describe several versions of a method for synthesizing sequential and concurrent systems. To cope with the constraints of model checking and of theorem proving, we combine such exhaustive verification methods with testing. We show several examples where we used our approach to synthesize, improve and correct code.

Lundi 10 février, 14h30

Anne Bouillard (ENS)

Oracle skipping for perfect sampling

La simulation parfaite est une technique de simulation qui permet de générer une variable aléatoire selon la distribution stationnaire d'une chaîne de Markov finie et ergodique. Lorsque la chaîne modélise le comportement d'un système (réseau de files d'attente par exemple), les changements d'états correspondent à des événements. Or, ces événements peuvent être passifs (ne pas changer l'état de la chaîne). On peut alors modifier l'algorithme originel de simulation parfaite pour ne générer que des événements qui changent l'état de la chaîne. Sur l'exemple des files d'attente, nous montrerons comment cela accélère l'algorithme de simulation parfaite.

Jeudi 20 février, 14h30 en salle Markov

Jonathan Protzenko

The Mezzo programming language -- a retrospective

Over the past two years, we developed a new programming language at Gallium: Mezzo. The initial goal was to provide a better type system for an ML-like language. We wanted to talk about state (is this iterator still valid or has it expired?), ownership (who owns this piece of mutable data in the heap?) and aliasing (must-alias; must-not-alias). In this talk, I will introduce the language we've come up with through various interactive examples, talk about the nice properties programs written in Mezzo enjoy (data-race freedom), and give a big-picture view of the current state of the project (the compiler, the proof of soundness).

Jeudi 27 février, 14h30

John Mullins (Ecole Polytechnique Montréal)

Opacity with Orwellian observers and Intransitive Non-interference

Opacity is a general language-theoretic scheme which may be instantiated to several security properties of a system. A behavior of a system is opaque if a passive attacker can never deduce its occurrence from the system observation. Instead of considering the case of static observability where the set of observable events is fixed off-line or dynamic observability where the set of observable events changes over time depending on the history of the trace, we consider Orwellian partial observability where unobservable events are not revealed unless some downgrading event occurs in the future of the trace. We show how to check that a regular secret is opaque for a regular language L w.r.t. an Orwellian projection while it has been proved undecidable for regular languages w.r.t. Orwellian observation functions. We finally illustrate relevancy of our results by proving the equivalence between the opacity property of regular secrets w.r.t. Orwellian projection and the intransitive non-interference property.

Jeudi 6 mars, 11h00 en salle Markov

Alain Girault (INRIA Grenoble)

Tradeoff exploration between reliability, power consumption, and execution time for embedded systems

For autonomous critical real-time embedded systems (e.g., satellite), guaranteeing a very high level of reliability is as important as keeping the power consumption as low as possible. We propose an off-line scheduling heuristic which, from a given software application graph and a given multiprocessor architecture (homogeneous and fully connected), produces a static multiprocessor schedule that optimizes three criteria: its length (crucial for real-time systems), its reliability (crucial for dependable systems), and its power consumption (crucial for autonomous systems). Our tricriteria scheduling heuristic, called TSH, uses the active replication of the operations and the data-dependencies to increase the reliability and uses dynamic voltage and frequency scaling to lower the power consumption. We demonstrate the soundness of TSH. We also provide extensive simulation results to show how TSH behaves in practice: first, we run TSH on a single instance to provide the whole Pareto front in 3D; second, we compare TSH versus the ECS heuristic (Energy-Conscious Scheduling) from the literature; and third, we compare TSH versus an optimal Mixed Linear Integer Program.

Jeudi 13 mars, 14h30, salle Aurigny

Louis-Marie Traonouez

Refinement Distances for the Modal nu-Calculus

Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. We then introduce a quantitative extension of disjunctive modal transition systems and of the modal nu-calculus, intended for the specification and compositional verification of systems with quantitative information. We show that also in this quantitative setting, there is a structural equivalence between the modal nu-calculus and disjunctive modal transition systems. This enables the transfer of methods and tools from the logical realm to the structural one, and back.

Jeudi 20 mars, 14h30 en salle Markov

Sophia Knight (LORIA)

Epistemic Logic as a Programming Language: Epistemic Modalities in Process Calculi

I will discuss the role which epistemic reasoning can play in concurrency theory. The idea of using epistemic modalities as programming constructs has been largely unexplored. Logic programming emerged under the slogan ``Logic as a programming language.'' In this talk I will explore the role of modal logic as a programming language, incorporating epistemic and closely related spatial modalities, as part of the programming language and not just as part of the meta-language for reasoning about protocols. I will present spatial and epistemic process calculi for reasoning about spatial information and knowledge distributed among the agents of a system, and I will discuss domain-theoretical structures for representing spatial and epistemic information.

Jeudi 20 mars, 16h00 en salle Markov

Aybüke Özgün (LORIA)

Topological Models for (Full) Belief and Belief Revision

We introduce a new topological semantics for belief logics in which the belief modality is interpreted as the closure of the interior operator. We show that our semantics validates the axioms of Stalnaker's combined system of knowledge and belief (presented in his paper 'On Logics of Knowledge and Belief'), in fact, that it constitutes the most general extensional semantics validating these axioms. We further prove that in this semantics the logic KD45 is sound and complete with respect to the class of extramlly disconnected spaces and compare our proposal to the topological interpretation of belief in terms of the derived set operator. We also explore topological analogues of static and dynamic belief change by providing topological semantics for conditional belief and update modalities. This is joint work with Alexandru Baltag, Nick Bezhanishvili and Sonja Smets.

Jeudi 27 mars, 14h30 en salle Markov

Amélie Stainer (Université Libre de Bruxelles)

Synthesising succint strategies in monotonic games, with applications to real-time schedulers synthesis

Finite turn-based safety games can be used to synthesize schedulers for computer systems running on multiprocessor platforms[BM-esa10]. In this context, games are implicitly defined from a set of tasks T and their size is exponential in the size of T. Nevertheless, there is a natural relation between states of areas of such games. We first formalise the properties that we expect on the relation between states, by the notion of weak bisimulation which is an intermediate between simulation and bisimulation relation. Then, we show how such weak bisimulations can be exploited to (1) improve the running time of the OTFUR algorithm [CDFLL-concur05] to compute winning strategies and (2) obtain a succint representation of a winning strategy.

Jeudi 3 avril, 14h30 en salle Markov

Loig Jezequel

Computation of Summaries Using Net Unfoldings

We study the following summarization problem: given a parallel composition A=A_1||...||A_n of labelled transition systems communicating with the environment through a distinguished component A_i, efficiently compute a summary S_i such that E||A and E||S_i are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications. (Joint work with J. Esparza and S. Schwoon)

Jeudi 10 avril, 14h30 en salle Markov

Benoit Baudry

Automatic and Efficient Synthesis of Equivalent Computationally Diverse Programs

The predictability of program execution provides attackers a rich source of knowledge who can exploit it to spy or remotely control the program. Moving target defense addresses this issue by constantly switching between many diverse variants of a program, which reduces the certainty that an attacker can have about the program execution. The effectiveness of this approach relies on the availability of a large number of software variants that exhibit dierent executions. However, current approaches rely on the natural diversity provided by off-the-shelf components, which is very limited. In this paper, we explore the automatic synthesis of large sets of program variants, called sosies. Sosies provide the same expected functionality as the original program, while exhibiting different executions. They are said to be computationally diverse. This work addresses two objectives: comparing different transformations for increasing the likelihood of sosie synthesis (densifying the search space for sosies); demonstrating computation diversity in synthesized sosies. We synthesized 30 184 sosies in total, for 9 large, real-world, open source ap- plications. For all these programs we identied one type of program analysis that systematically increases the density of sosies; we measured computation diversity for sosies of 3 programs and found diversity in method calls or data in more than 40% of sosies. This is a step towards controlled massive unpredictability of software.

Jeudi 17 avril, 14h30 en salle Markov

Valentin Goranko (Technical University of Denmark)

Secure aggregation of distributed information in multi-agent systems

We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where a group of agents have information distributed amongst them, i.e., included in their collective knowledge, while each agent has only partial knowledge of it. The agents act as a team that has to exchange and aggregate that information, either as common knowledge within the group or in the individual knowledge of at least one of them. The exchange is performed over insecure communication channels and is presumed intercepted by an adversary ``eavesdropper''. The task of the team is to achieve the aggregation of the distributed information, following a prearranged protocol, in such a way that the adversary does not learn important information. We model the SADI problem by assuming that the information that each agent has is encoded by a set of ``cards'' that she holds in her hands. The cards are drawn from a publicly known deck and every card is in the hands of exactly one agent of the team and can only be seen by that agent. The goal of the team is to exchange and spread across the whole team the information about how the cards are distributed amongst the agents. The agents can only communicate by making public announcements over insecure channels and the goal of the eavesdropper is to learn the location of at least one of the cards by intercepting and analyzing the announcements exchanged by the agents. The problem described above is a variation of the well-known ``Russian cards problem''. Here we, on the one hand, generalize it to any number of agents, but on the other hand we restrict it essentially by assuming that the eavesdropper has no cards in his hands. In this work we present a combinatorial construction of protocols that provides a direct solution of a class of SADI problems and develop a technique of iterated reduction of SADI problems to ``simpler'' ones which are eventually solvable directly. We show that our methods provide a solution to all SADI problems of sufficiently large size. (joint work with David Fernandez-Duque)

mardi 13 mai et mercredi 14 mai

Colloque en l'honneur d'Albert Benveniste

Pour célébrer les 65 ans d’Albert Benveniste, plus de 40 ans de recherches, et à l’occasion de son départ en retraite, Inria et l’Irisa organisent un colloque en son honneur. Ce colloque se tiendra le 13 mai après-midi et la matinée du 14 mai 2014. Il est destiné à ses collègues et amis, ainsi qu’à tous ceux qui s’intéressent à ses travaux. Le programme couvrira de nombreux sujets, en relation avec les travaux d’Albert Benveniste : traitement du signal, contrôle, surveillance des structures, conception, architecture et programmation des systèmes temps-réel, systèmes stochastiques, architectures de services.

Informations, programme et inscription sur : https://project.inria.fr/alberts65th/

Inscription gratuite mais obligatoire pour le colloque. Participation de 30 euros pour la soirée de gala du 13 mai.

Jeudi 15 mai, à 14h30 en salle Markov

Cinzia Di Giusto (Univ. Evry)

Disciplined Runtime Update

Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing requirements related to runtime update. This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. I will present a process calculi framework of reconfigurable processes, in which concurrent processes can be replaced, suspended, or discarded at runtime. I will propose a session type discipline for a calculus with reconfigurable processes. Our typed framework offers a simple alternative for integrating runtime update mechanisms in the modeling and analysis of structured communications. I will show that well-typed processes enjoy safety and consistency properties: while the former property ensures the absence of communication errors at runtime, the latter guarantees that active session behavior is never disrupted by update actions.

mercredi 28 mai, 14h30

Caterina Urban (ENS)

An Abstract Domain to Infer Ordinal-Valued Ranking Functions

The traditional method for proving program termination consists in inferring a ranking function. In many cases (i.e. programs with unbounded non-determinism), a single ranking function over natural numbers is not sufficient. Hence, we propose a new abstract domain to automatically infer ranking functions over ordinals. We extend an existing domain for piecewise-defined natural-valued ranking functions to polynomials in omega, where the polynomial coefficients are natural-valued functions of the program variables. The abstract domain is parametric in the choice of the maximum degree of the polynomial, and the types of functions used as polynomial coefficients. We have implemented a prototype static analyzer for a while-language by instantiating our domain using affine functions as polynomial coefficients. We successfully analyzed small but intricate examples that are out of the reach of existing methods. To our knowledge this is the first abstract domain able to reason about ordinals. Handling ordinals leads to a powerful approach for proving termination of imperative programs, which in particular subsumes existing techniques based on lexicographic ranking functions.

jeudi 5 juin, 14h30

Mahsa Shirmohammadi (LSV/ULB)

Limit Synchronization in Markov Decision Processes

Markov decision processes (MDP) are finite-state systems with both strategic and probabilistic choices. After fixing a strategy, an MDP produces a sequence of probability distributions over states. The sequence is eventually synchronizing if the probability mass accumulates in a single state, possibly in the limit. Precisely, for 0 ≤ p ≤ 1 the sequence is p-synchronizing if a probability distribution in the sequence assigns probability at least p to some state, and we distinguish three synchronization modes: (i) sure winning if there exists a strategy that produces a 1-synchronizing sequence; (ii) almost-sure winning if there exists a strategy that produces a sequence that is, for all ε > 0, a (1-ε)-synchronizing sequence; (iii) limit-sure winning if for all ε > 0, there exists a strategy that produces a (1-ε)-synchronizing sequence. We consider the problem of deciding whether an MDP is sure, almost-sure, limit-sure winning, and we establish the decidability and optimal complexity for all modes, as well as the memory requirements for winning strategies. Our main contributions are as follows: (a) for each winning modes we present characterizations that give a PSPACE complexity for the decision problems, and we establish matching PSPACE lower bounds; (b) we show that for sure winning strategies, exponential memory is sufficient and may be necessary, and that in general infinite memory is necessary for almost-sure winning, and unbounded memory is necessary for limit-sure winning; (c) along with our results, we establish new complexity results for alternating finite automata over a one-letter alphabet.

mardi 17 juin, 14h30 en salle Markov

S. Akshay (IIT Bombay)

Reachability problems for Markov chains

In this talk, we consider a basic reachability problem for Markov chains which lies at the heart of many model checking questions: given a finite Markov chain with distinguished source and target states, and a rational number r, does there exist an integer n such that the probability to reach the target from the source in n steps is r? Surprisingly, it turns out that the decidability of this problem is still open. We provide evidence of the hardness of the problem by relating it to the Skolem Problem: a number-theoretic decision problem whose decidability has been open for decades. We further investigate the dynamics of a Markov chain and show some regularity and non-regularity results. We will also explore the links between these problems and other classically hard problems such as program termination.

jeudi 26 juin, 11h en salle Crête

Étienne André

Precise Robustness Analysis of Concurrent Real-Time Systems

Real-time systems need to be perfectly reliable, both in terms of functional correctness (discrete behavior), and timed correctness (e.g., all deadlines met). Formal methods can prove that the system satisfies both a functional and a timed specification. However, when implemented in practice, the system can very slightly derive from its model, when the timings constants (deadlines, timers, clock speeds) are very close to but different from their corresponding value in the model, in which case the specification may become violated. This concept is known as the robustness. Here, we introduce a more precise notion of robustness than what is usually considered: we measure the allowed variability of each timing delay in their neighbourhood, and give their allowed variability in the term of a linear constraint on the timing constants considered as parameters. Our approach, based on the inverse method, allows the designer to identify the constants allowing the least variability; we also exhibit a condition and a construction for rendering robust a non-robust system. We use the formalism of timed automata (and extensions) throughout the talk, and we use as a motivating application the schedulability analysis of a distributed real-time system with fixed priority. We finally discuss an extension of this concept to probabilistic systems, and give a robustness condition guaranteeing the equality of min/max reachability probabilities.

jeudi 3 juillet, 14h30, salle Minquiers

Antti Kuusisto

Descriptive Complexity Theory of Distributed Computing.

The objective of descriptive complexity theory is to provide logical characterizations of computational complexity classes. For example, the pioneering result of Fagin from 1974 states that the class NP contains exactly the classes of structures that are definable in existential second-order logic (ESO). The logic ESO is said to capture NP. So far descriptive complexity theory has concentrated almost exclusively to classical computation. The recent article [Hella et al. PODC 2012] introduces descriptive complexity theory of distributed computing. The article characterizes a range of complexity classes of distributed computing in terms of related modal logics. Furthermore, the article provides a complete classification of the computational capacities of the studied complexity classes. Classification results are obtained with the help of logical methods. We also discuss a paper [Kuusisto, CSL 2013], which is a continuation paper of [Hella et al. PODC 2012]. In [Hella et al. PODC 2012], all logical characterizations are limited to complexity classes defined in terms of constant-time distributed message passing automata. The paper [Kuusisto, CSL 2013] provides logical characterizations also for non-constant-time distributed algorithms.