Liste des événements uniques du groupe Modélisation et Verification


2013-06-27Static analysis of programs manipulating arrays
11:30-12:30
076
Static analysis is a key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs, ...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections)

Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition.

The choice of this partition is a difficult problem and each method has its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes.

We generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.
 Plus d'infos  


2013-06-20
11:30-12:30
076
 Plus d'infos  


2013-06-13
11:30-12:30
076
 Plus d'infos  


2013-06-06On the Context-freeness Problem for Vector Addition Systems
11:30-12:30
076
Petri nets, or equivalently vector addition systems (VAS),
are widely recognized as a central model for concurrent systems.
Many interesting properties are decidable for this class,
such as boundedness, reachability, regularity,
as well as context-freeness, which is the focus of this paper.
The context-freeness problem asks whether the trace language
of a given VAS is context-free.
This problem was shown to be decidable by Schwer in 1992,
but the proof is very complex and intricate.
The resulting decision procedure relies on five technical conditions over
a customized coverability graph.
These five conditions are shown to be necessary,
but the proof that they are sufficient is only sketched.
In this paper, we revisit the context-freeness problem for VAS,
and give a simpler proof of decidability.
Our approach is based on witnesses of non-context-freeness,
that are bounded regular languages satisfying a nesting condition.
As a corollary,
we obtain that the trace language of a VAS is context-free if,
and only if,
it has a context-free intersection with every bounded regular language.
 Plus d'infos  


2013-05-30Exact algorithms for stochastic games and real algebraic geometry
11:30-12:30
076
Shapley's discounted stochastic games and Everett's recursive games are classical
models of game theory describing two-player zero-sum games of potentially infinite
duration. We present an exact algorithm for solving such games based on separation
bounds from real algebraic geometry. When the number of positions of the game is
constant, the algorithm runs in polynomial time and is the first with this property.
We also present lower bounds on the algebraic degree of the values of stochastic
games induced from the irreducibility of polynomials that have coefficients that
depend on the combinatorial parameters of the games, based on a generalization
of Eisenstein criterion.
 Plus d'infos  


2013-05-16Path Analysis in OTAWA Framework
11:30-12:30
076
OTAWA (Open Tool for Adaptive WCET Analysis) is an open framework dedicated to the computation of WCET (Worst Case Execution Time). To be sound, effective and precise, this type of analysis must be performed at the machine code level that requires to decode and build back the execution paths of the program.
A challenging and interesting issue of path analysis is that the embedded real-time systems, targeted by the OTAWA, exhibit a lot of different ISA (Instruction Set Architecture) like PowerPC, Sparc, ARM, TriCore, etc. As it would be a possible but a tedious and error-prone solution to implement these back-ends by hand, OTAWA re-use a well-known technology based on ADL (Architecture Description Language). Basically, ADL were developed to allow automatic and safe generation of ISS (Instruction Set Simulator) including the ability of decoding instructions from the binary code. In OTAWA, we have adapted an existing ADL generator, called GLISS, not only to get an instruction decoder but also to provide other useful information items like target of branches, used registers, type of instructions, etc.
Decoding instructions is necessary to build back execution paths but we need also to get a simple and concise representation of the execution paths. CFG (Control Flow Graph) is good and common candidate: starting from the function entry points, they are build by following the instruction control flow to get edges and by grouping instruction in basic blocks to improve compactness of the representation. Yet, it remains some constructions that are hard to handle, i.e. indirect or computed branches, whose target can not be obtained by just looking to the instructions. This constructions are induced by the use of function pointers or by optimization of switch-like statements in high-level languages. The determination of the possible target of such branches requires to perform data flow analysis based on machine code and once again, the ADL have been used in OTAWA to easily produce semantics of machine code instruction making the data flow analysis independent of the actual ISA.
The presentation will be followed by a demonstration of the OTAWA plugin in the Eclipse environment.
 Plus d'infos  


2013-04-25Automatic security proof of cryptographic primitives: public encryption, symmetric encryption modes, MAC
11:30-12:30
076
Our aim is to develop a formal method in order to prove cryptographic primitives. We consider cryptographic primitives as small programs, usually it is just few lines of code. In the last century Tony Hoare provided mechanisms in order to prove that a program is correct, so-called Hoare logic.

Our approach consists in the three following steps:

Modeling properties that studied primitives have to ensure by proposing some invariants.

Defining the language which represent the small set of commands used to construct a primitives at the good abstract level.

Proving Logics rules, that allows us to generate and propagate invariants according to the commands executed in the program.

Once the language fixed, the invariants developed and the rules of the Hoare Logic established, we can verify a primitive. Using this approach we have developed three logics to prove security of several public encryption schemes, symmetric encryption modes and also several MAC.
 Plus d'infos  


2013-04-04The Insight binary analysis framework
11:30-12:30
076
In this talk, we will present the current status of the Insight
project which is aimed at analysing binary code.

Binary code analysis is challenging because of the inherent
difficulties of analysing code where the control flow graph is not
explicitly given, where datatypes are not available, compounded with
the technical challenge of decoding mnemonics of real processors as
complex as the Intel 32-bit architecture.

The formal model used in Insight will be presented, and an application
to CFG recovery will be detailed. Further work will be discussed.
 Plus d'infos  


2013-03-28Cost-optimal factored planning using weighted automata calculus
11:30-12:30
076
Factored planning is a relatively new domain in planning. It consists in exploiting the possible decompositions of many planning problems into exponentially smaller subproblems in order to efficiently solve them by parts. Even if, in the worst case, the complexity of factored planning is the same as the complexity of classical planning, in many cases of interest it is much more efficient. However, before this work, no factored planning method existed to compute cost-optimal solutions to planning problems. In this talk we will present an approach to factored planning allowing to find cost-optimal solutions thanks to the use of weighted automata calculus. The principle of this approach is to represent the set of solutions of each subproblem as a weighted automaton and apply a standard message passing algorithm to the network constituted by all these automata. This allows to compute new automata representing exactly those solutions of subproblems which are part of solutions of the global planning problem, and from that to give a globally optimal solution of this planning problem in a modular way.
 Plus d'infos  


2013-03-07A semi-decidable approach for determining language inclusion for timed automata
11:30-12:30
076
Language inclusion for timed automata is known to be undecidable. The
universality problem can be considered to be a special case of the
language inclusion problem. Given a universal timed automaton A and any
other timed automaton B, the language inclusion problem asks if the timed
language accepted by A is included in the timed language accepted by B.
Solving this problem implies deciding the universality problem for B which
is known to be undecidable!

In this work, we present a semi-decidable algorithm which gives three
outputs as follows: 'yes' indicates that we conclude that the language
accepted by A is a subset of the language accepted by B. 'no' indicates
that the language accepted by timed automaton B does not include the
language accepted by A. 'do not know' indicates that we do not know how
the langauges accepted by A and B are related.

The language inclusion problem for timed automata is known to be decidable
when timed automaton B is deterministic or determinizable or when timed
automaton B (strongly time) simulates timed automaton A or when B is a
single clock timed automaton. We show that our method works in many cases
where B cannot simulate A or B cannot be determinized.
 Plus d'infos  


2013-02-21Equivalence Checking of Pushdown Automata and One-Counter Automata
11:30-12:30
076
The first part of my talk will be about bisimilarity of one-counter automata (which are pushdown automata over a singleton stack symbol with a bottom-of-stack symbol). I will show that this problem is PSPACE-complete, improving the previously best-known 3-EXPSPACE upper bound by Yen (joint work with Stanislav Böhm and Petr Jancar).
The second part of the talk will be about the complexity of bisimilarity checking of pushdown automata. While decidability of this problem has been shown by Sénizergues, no complexity-theoretic upper bound of this problem is known to date. I will present a recent nonelementary lower bound for this problem, improving the previously best-known EXPTIME-hardness result of Kucera and Mayr (joint work with Michael Benedikt, Stefan Kiefer and Andrzej Murawski).
 Plus d'infos  


2013-01-31Reasoning about Data Repetitions with Counter Systems
11:30-12:30
076
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
2EXPSPACE 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 potentially 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.

This is joint work with Stephane Demri and Diego Figueira.
 Plus d'infos  


2013-01-24Underapproximation of Procedure Summaries for Recursive Integer Programs
11:30-12:30
076
We show how to underapproximate the procedure summaries of recursive programs
over the integers using off-the-shelf analyzers for non-recursive programs. The
novelty of our approach is that the non-recursive program we compute may capture
unboundedly many behaviors of the original recursive program for which stack
usage cannot be bounded. Moreover, we identify a class of recursive programs on
which our method terminates and returns the precise summary relations without
underapproximation. Doing so, we generalize a similar result for non-recursive
programs to the recursive case. Finally, we present experimental results of an
implementation of our method applied on a number of examples.

Joint work with Pierre Ganty (IMDEA) and Filip Konecny (EPFL).
 Plus d'infos  


2013-01-17Beautiful Games You Cannot Stop Playing
11:30-12:30
076
Parity games are simple two player games played on a finite arena that have all that it takes to attract the attention of researchers: it is a simple problem which is hard to analyse. A pocket version of P vs. NP.
Parity games are known to be in UP, CoUP, and some weirder classes besides, but whether or not they are in P has proven to be a rather elusive question. What is more, when you work with them, you will have the constant feeling that there is a polynomial time solution just around the corner, although it dissolves into nothingness when you look more closely. This talk is about the beauty of these games, the relevant algorithmic approaches and their complexity and development over time. But be careful: they are addictive, don't get hooked!
 Plus d'infos  


2013-01-10Time-bounded reachability for monotonic hybrid automata
11:30-12:30
076

Hybrid automata (HA) form a very popular class of model for describing hybrid systems, i.e. systems that exhibit both discrete and continuous behaviors. An HA is roughly speaking a finite automaton augmented with a finite set of real-valued variables, whose values evolve continuously with time elapsing. The rate of growth of those variables can change along time and depends on the current location of the automaton. Unfortunately, HA are notoriously hard to analyse: even the reachability problem is undecidable on the very restricted subclass of stopwatch automata (where variables can have rates 0 or 1 only).

However, most of the undecidability results on HA rely on the unboundedness of time to encode runs of undecidable models such as two-counter machines. A natural question is thus to study the time-bounded variant of the verification problems on HA, hoping that this additional requirement will allow to recover decidability. A further incentive is the recent line of research by Ouaknine, Worrell, et al., who have shown the benefits of considering time-bounded variants of classical problems in the case of (alternating) timed automata.

In this talk, we study the time-bounded reachability problem for monotonic rectangular hybrid automata (MRHA). An MRHA is a rectangular hybrid automata where the rate of each clock is either alway non-negative, or always non-positive. We show that this problem is decidable (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable), and give a precise characterisation of its complexity: it is NExpTime-c. We also show that extending this class by either allowing a clock to have positive and negative rates in the same HA, or by allowing diagonal guards, leads to undecidability, even in bounded time. Finally, we present a more practical extension of our positive result, by showing that we can effectively compute fixpoints characterising the sets of states that are reachable (resp. co-reachable) within T time units from a given state.

This is joint work with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell.
 Plus d'infos  


2012-12-20Runtime Enforcement of Timed Properties
11:30-12:30
076
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. We discuss how runtime enforcers can be synthesized for a safety or co-safety timed property. 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.
 Plus d'infos  


2012-12-06A perfect model for bounded verification
10:15-11:15
Salle Patio - Bat C4 "Haut-carré"
A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata- theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for context-free languages is undecidable, no class containing them can be perfect.In practice, verification problems for language classes that are not perfect are often under-approximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages. A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language.We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multi-head pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multi-threaded programs, recursive counter machines, and communicating finite-state machines can be encoded as multi-head pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages.
 Plus d'infos  


2012-12-06Multi-dimension Quantitative Games: Complexity and Strategy Synthesis
11:15-12:15
Salle Patio - Bat C4 "Haut-carré"
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. In this talk, I will summarize several recent results that we have obtained recently: -We prove the finite-memory determinacy of multi-energy games and show the inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. -We improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was ExpSpace, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete. -We provide an optimal symbolic and incremental algorithm to synthesis strategies in multi-energy games. -We present the first solution of multi-mean-payoff games with infinite-memory strategies. We show that multi-mean-payoff games with mean-payoff-sup objectives can be decided in NP and in coNP, whereas multi-mean-payoff games with mean-payoff-inf objectives are coNP-complete.
 Plus d'infos  


2012-11-29Safety Verification of Communicating One-Counter Machines
11:30-12:30
076
In order to verify protocols that tag messages with integer
values, we investigate the decidability of the reachability
problem for systems of communicating one-counter machines. These
systems consist of local one-counter machines that asynchronously
communicate by exchanging the value of their counters via, a
priori unbounded, FIFO channels. This model extends communicating
finite-state machines (CFSM) by infinite-state local processes
and an infinite message alphabet. The main result of the paper
is a complete characterization of the communication topologies
that have a solvable reachability question. As already CFSM
exclude the possibility of automatic verification in presence of
mutual communication, we also consider an under-approximative
approach to the reachability problem, based on rendezvous
synchronization.

Joint work with Alexander Heußner and Tristan Le Gall.
 Plus d'infos  


2012-11-08Coarse abstractions make Zeno behaviors difficult to detect
11:30-12:30
076
An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NP-completeness for the LU-extrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LU-extrapolation that satisfies these conditions.
 Plus d'infos  


2012-10-04Reachability of Communicating Timed Processes
11:30-12:45
076
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises au- tomata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topology-preserving reductions between timed automata and (untimed) counter automata.
 Plus d'infos  


2012-09-27Strategy Synthesis (From Specification to Implementation)
11:30-12:30
076
This is a short jeurney from the pitfalls and beauty of Church's problem from an automata theoretic angle. We will admire the simplicity of the problems and some funny effects, from forcing the branching mode of the automata involved to the cost incurred. After looking at how we can keep our life simple for a price too hight to pay, we return more and more to the real problem and see with (maybe) some surprise that the it is even simpler. Probably. But we will prove that it is unlikely that we will ever discover the truth.
 Plus d'infos  


2012-06-07Parameterized Complexity of some Petri Net Problems
11:30-12:30
Parameterized complexity is the branch of complexity theory that seeks to identify in the computational complexity of some problems the dependence on different parameters of the input. The coverability and boundedness problems for Petri nets are known to be EXPSPACE-complete. Previous work [Ex: L.E. Rosier and H.-C. Yen. A multiparameter analysis of the boundedness problem for vector addition systems. JCSS 32, 1986] has already been done to analyse the dependency of this complexity on different parameters, such as the number of places, maximum arc weight etc. We continue this work and study the dependency of the complexity on two parameters called benefit depth and vertex cover. If k denotes a parameter and n denotes the size of the input for a problem, then the problem is said to be in the parameterized complexity class PARAPSpace if there is an algorithm to solve the problem that uses memory space O(f(k)poly(n)), where f(k) is any computable function of the parameter and poly(n) is some polynomial of the input size. We show PARAPspace results for the coverability and boundedness problems using the parameters mentioned above. We also show PARAPspace results for model checking a logic that can express some extensions of coverability and boundedness. This is joint work with Kamal Lodaya.
 Plus d'infos  


2012-05-24Querying Schemas With Access Restrictions
11:00-12:00
076
We study verification of systems whose transitions consist of
accesses to a Web-based data-source. An access is a lookup
on a relation within a relational database, fixing values for
a set of positions in the relation. For example, a transition
can represent access to a Web form, where the user is restricted
to filling in values for a particular set of fields. We
look at verifying properties of a schema describing the possible
accesses of such a system. We present a language where
one can describe the properties of an access path, and also
specify additional restrictions on accesses that are enforced
by the schema. Our main property language, AccLTL, is
based on a first-order extension of linear-time temporal logic,
interpreting access paths as sequences of relational structures.
We also present a lower-level automaton model, Aautomata,
which AccLTL specifications can compile into.
We show that AccLTL and A-automata can express static
analysis problems related to “querying with limited access
patterns” that have been studied in the database literature
in the past, such as whether an access is relevant to answering
a query, and whether two queries are equivalent in
the accessible data they can return. We prove decidability
and complexity results for several restrictions and variants
of AccLTL, and explain which properties of paths can be
expressed in each restriction.
 Plus d'infos  


2012-05-10Tagging Make Local Testing of Message-Passing Systems Feasible
11:30-12:30
076
The only practical way to test distributed message-passing systems is
to use local testing. In this approach, used in formalisms such as
concurrent TTCN-3, some components are replaced by test
processes. Local testing consists of monitoring the interactions
between these test processes and the rest of the system and comparing
these observations with the specification, typically described in
terms of message sequence charts. The main difficulty with this
approach is that local observations can combine in unexpected ways to
define implied scenarios not present in the original
specification. Checking for implied scenarios is known to be
undecidable for regular specifications, even if observations are made
for all but one process at a time. We propose an approach where we
append tags to the messages generated by the system under test. Our
tags are generated in a uniform manner, without referring to or
influencing the internal details of the underlying system. These
enriched behaviours are then compared against a tagged version of the
specification. Our main result is that detecting implied scenarios
becomes decidable in the presence of tagging.

This is joint work with Puneet Bhateja.
 Plus d'infos  


2012-05-03Bounded Phase Analysis of Message-Passing Programs
11:30-12:30
076
We describe a novel technique for bounded analysis of asynchronous
message-passing programs with ordered message queues. Our bounding
parameter does not limit the number of pending messages, nor the
number of “contexts-switches” between processes. Instead, we limit the
number of process communication cycles, in which an unbounded number
of messages are sent to an unbounded number of processes across an
unbounded number of contexts. We show that remarkably, despite the
potential for such vast exploration, our bounding scheme gives rise to
a simple and efficient program analysis by reduction to sequential
programs. As our reduction avoids explicitly representing message
queues, our analysis scales irrespectively of queue content and
variation.
 Plus d'infos  


2012-04-12Model Checking Languages of Data Words
11:30-12:30
076
We consider the model-checking problem for data multi- pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.

This is a joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar.
 Plus d'infos  


2012-04-05 Forward Analysis for WSTS : Beyond Regular Accelerations
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
The well-known Karp and Miller algorithm constructs the
coverability tree of a Vector Addition System, obtaining a finite representation
of the cover (the downward closure of the reachability set).
The series "Forward analysis in WSTS" aims to generalize this procedure for
arbitrary well-ordered state spaces. I'll first recall the earlier works by Finkel
and Goubbault-Larrecq, that introduced the notion of complete WSTS, in
which a finite representation of the cover as set of maximal elements exists.
Then, i'll present our formalization of acceleration strategy and a parameterized Karp Miller procedure that relies on these strategy in order to compute this
set of maximal elements.
As an illustration of these ideas, I'll present an acceleration strategy for
Vector Addition Systems with two resets that allows the previously defined
procedure to terminate, effectively computing the finite representation of the cover.

This is joint work with Alain Finkel.
 Plus d'infos  


2012-03-29The Quantitative Linear-Time–Branching-Time Spectrum
11:30-12:30
076
We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.
 Plus d'infos  


2012-03-22Exploiting Structure in LTL Synthesis
11:30-12:30
076
The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures.
Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem.
In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem
 Plus d'infos  


2012-03-15Compositional Specification Theories for Stochastic Systems
11:30-12:30
076
Markov Chains (MCs) and Probabilistic Automata (PAs) are
widely-recognized mathematical frameworks for the specification and
analysis of systems with non-deterministic and/or stochastic behaviors.
Notions of specification, implementation, satisfaction, and refinement,
together with operators supporting stepwise design, constitute a
specification theory. In the early 1990's, an abstraction of Markov
Chains, called Interval Markov Chains (IMCs) has been proposed as a
specification theory. This talk shows why IMCs are not perfectly suited
to play their role as a specification theory and instead introduces a
new, more permissive, abstraction called Constraint Markov Chains
(CMCs). We introduce all the operators that make CMCs a complete
specification theory and discuss computability and complexity. We then
show how to extend CMCs by mixing them with Modal Transition Systems in
order to propose a specification theory for Probabilistic Automata.
 Plus d'infos  


2012-03-08The Cost of Repairing Regular Specifications
11:30-12:30
Amphi
What do you do if a computational object (e.g., a document, a program trace) fails a specification?
An obvious approach is to perform a "repair": modify the object minimally to get something that
satisfies the constraints. This approach has been extensively investigated in the database community
for relational integrity constraints, and in the AI community for propositional logics. Different modification
operators have been considered on the basis of the application scenarios. For instance, a repair of an
XML document usually consists of applying to the underlying tree structure a certain number of editing
operations such as relabelings, deletions, and insertions of nodes.

In this talk I will survey some results related to the worst-case cost of repairing documents between
regular specifications. Precisely, I will focus on the number of edits that are needed to get from a
document (i.e., a word or a tree) that satisfies a source specification (i.e., a regular language S) to
some document that satisfies a target specification (i.e., a regular language T). As this number may
well be unbounded, I will consider the problem of determining those pairs of languages (S,T) such
that one can get from any word/tree in S to a word/tree in T using a finite, uniformly bounded number
of editing operations. I will give effective characterizations of these pairs when S and T are given by
finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity
bounds for the corresponding problems.

The presentation is based on joint works with Michael Benedikt, Cristian Riveros, and Sławek Staworko.
 Plus d'infos  


2012-02-16Fixed-word simulations and ranks
11:30-12:30
Amphi
Minimization of Buchi automata is an intriguing topic in automata theory,
both for a theoretical understanding of automata over infinite words, and for practical applications.
Ideally, for a given language, one would like to find an automaton recognizing it with the least number of states.
Since exact minimization is computationally hard (e.g., PSPACE-complete),
we concentrate on quotienting, which is a state-space reduction technique which works by "glueing together" certain states.
Which states can be merged is dictated by suitable preorders:
In this talk, we study fixed-word simulations, which are simulation-like preorders sound for quotienting.
We show that fixed-word simulations are coarser than previously studied simulation-like preorders,
by characterizing it with a natural (but non-trivial) ranking argument.
Our ranking construction is related to the so-called Kupferman-Vardi construction for complementing Buechi automata.
 Plus d'infos  


2012-02-15
11:30-12:30
 Plus d'infos  


2012-02-09Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
11:30-12:30
Salle 076, LaBRI, Rez-de-chaussée
We introduce a framework based on abstract interpretation for reasoning about programs with lists carrying integer numerical data.
In this framework, abstract domains are used to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, and on the data stored in the lists.
We consider a domain where data is described by formulas in a universally quantified fragment of the first-order logic over sequences, as well as a domain where data is described using constrains on the multisets of data in the lists.
Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called CELIA and experimented successfully on a large benchmark of programs.
 Plus d'infos  


2012-01-26Forest Automata for Verification of Heap Manipulation
11:30-12:30
076
We consider verification of programs manipulating
dynamic linked data structures such as various forms of singly and doubly-linked
lists or trees. We consider important properties for this kind of systems like
no null-pointer dereferences, absence of garbage, shape properties, etc. We
develop a verification method based on a novel use of tree automata to represent
heap configurations. A heap is split into several ``separated'' parts such that
each of them can be represented by a tree automaton. The automata can refer to
each other allowing the different parts of the heaps to mutually refer to their
boundaries. Moreover, we allow for a hierarchical representation of heaps by
allowing alphabets of the tree automata to contain other, nested tree automata.
Program instructions can be easily encoded as operations on our representation
structure. This allows verification of programs based on a symbolic state-space
exploration together with refinable abstraction within the so-called abstract
regular tree model checking. A motivation for the approach is to combine
advantages of automata-based approaches (higher generality and flexibility of
the abstraction) with some advantages of separation-logic-based approaches
(efficiency). We have implemented our approach and tested it successfully on
multiple non-trivial case studies.
(joint work with Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar)
 Plus d'infos  


2012-01-19Optimizing Buechi Automata Inclusion Checking with Subsumption Preorders
11:30-12:30
076
Inclusion checking is a central algorithmic problem in the theory of automata, with important applications, e.g., in formal methods.
The problem is PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected.

We optimize the so-called Ramsey-based approach to inclusion checking.
In this approach, one explores a semigroup of exponential size for a counter-example to inclusion.
The exploration starts from a small set of generators, and all elements of the semigroup are progressively computed by composition.
On the way, a test operation is used to check for counter-examples.
The exploration stops if a counter-example is found; otherwise, all elements are generated.

Clearly, exhaustive exploration of the semigroup is in general infeasible, due to its exponential size.
We show how coarse simulation-based subsumption preorders between elements of the semigroup can be designed,
allowing one to prune away significant parts of the search space.
Subsumption allows us to solve inclusion checking for automata with thousand states, which was unthinkable before.
More details can be found on http://www.languageinclusion.org/.
 Plus d'infos  


2012-01-12Robustness and Implementability of Timed Automata
11:30-12:30
076
Timed automata are a well established model in real-time system design. They offer an automata-theoretic framework to design, verify and synthesize systems with timing constraints. The theory behind timed automata has been extensively studied and mature model-checking tools are available. However, this model makes unrealistic assumptions on the system, such as the perfect continuity of clocks and instantaneous reaction times, which are not preserved in implementation even in digital hardware with arbitrary finite precisions. While these assumptions are natural in the design phase, they must be validated before implementing the system.
In this talk, I will first outline recent results on robustness analysis of timed automata, that is, deciding/computing an upper bound on the imprecisions under which a given property holds. I will then concentrate on the implementability problem, by presenting algorithms that render timed automata implementable: given a timed automaton, the goal is to construct a new timed automaton whose behavior under imprecisions is equivalent to the behavior of the first automaton.

Based on joint works with Patricia Bouyer, Kim Larsen, Nicolas Markey, Claus Thrane.
 Plus d'infos  


2011-12-08Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (3)
11:30-12:30
Salle 076, LaBRI, Rez-de-chaussée
Description: Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mu-calcul sur les arbres. Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que E-C est aussi dans Gamma, et A inclus dans C, B inclus dans E-C. Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie. A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009] Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2). Auparavant, le problème de la séparation dans la hiérarchie des omega-langages reconnus par des automates __déterministes__ à parité sera entièrement traité.
 Plus d'infos  


2011-12-01Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (2)
11:30-12:30
076
 Plus d'infos  


2011-11-24Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres
11:30-12:30
076
Description:
Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mu-calcul sur les arbres.

Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que E-C est aussi dans Gamma, et A inclus dans C, B inclus dans E-C.

Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie.

A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009]

Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2).

Auparavant, le problème de la séparation dans la hiérarchie des omega-langages reconnus par des automates __déterministes__ à parité sera entièrement traité.
 Plus d'infos  


2011-11-17Visibly Pushdown Transducers: Functionality, k-Valuedness and Streamability
11:30-12:30
075
Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly pushdown languages form a robust subclass of context-free languages. Along the same line, we show that word transductions defined by VPTs enjoy strong properties, in contrast to PTs. In particular, functionality is decidable in PTIME, k-valuedness is in NPTIME and equivalence of (non-deterministic) functional VPTs is EXPTIME-C.

In a second part, we study the problem of evaluating in streaming (i.e. in a single left-to-right pass) the transduction realized by a functional VPT. A transduction is said to be height bounded memory (HBM) if it can be evaluated with a memory that depends only on the height of the input word (and not on its length). We show that it is decidable in coNTPTime whether such a transduction is HBM. In this case, the required amount of memory may depend exponentially on the height of the input word. We exhibit a sufficient, decidable condition for a VPT to be evaluated with a memory that depends quadratically on the height of the input word. This condition defines a class of transductions that strictly contains all determinizable VPTs.

This talk is based on the two following papers :

Properties of Visibly Pushdown Transducers. Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier Reynier, Frédéric Servais and Jean-Marc Talbot. In Proc. MFCS’10.
Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais. In Proc. FSTTCS’11.
 Plus d'infos  


2011-11-10Vpraxis et évolution d'application internet
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Pratiquement toutes les applications s’exécutent aujourd’hui sur Internet,
quel que soit leur usage et quel que soit leur domaine. Une application qui
s’exécute sur internet fait partie d’un réel écosystème d’applications. Elle
utilise et propose des ressources (donnée et/ou traitement) qui forment
l’écosystème. Ces ressources, qui étaient il y a quelques années encore du
simple texte, des images ou des vidéos, sont aujourd’hui beaucoup plus
complexes, tels que des données sémantiques ou des services web par exemple.

Cette complexité croissante fait que le développement des applications
internet, et donc de l’écosystème, ne peut plus se faire par des équipes
bien structurées, maîtres des artefacts logiciels qu’elles produisent et
appliquant des cycles de développement traditionnels. Nous soutenons que le
développement d’application internet doit nécessairement prendre en
considération le concept d’écosystème logiciel. Les applications de demain
seront de plus en plus dépendantes de leur écosystème. Sans une forte
réactivité de développement face aux évolutions de l’écosystème, une
application deviendra vite dépassée et donc inutilisable ou extrêmement
couteuse en maintenance.
Le thème Sphere du LaBRI (http://sphere.labri.fr) développe l’approche
VPraxis qui vise à contrôler l’évolution des applications internet. Notre
objectif est de modéliser les histoires des différents composants des
applications internet afin de contrôler leur interdépendance. Cette
présentation portera sur VPraxis et montrera le modèle qu’il propose afin de
modéliser l’évolution d’un écosystème logiciel.
 Plus d'infos  


2011-11-03Controlling distributed systems
11:30-12:30
076
We consider the problem of controlling distributed automata that cooperate via
shared variables (rendez-vous). The setting corresponds to the framework of
Ramadge and Wonham, where certain actions (controllable ones) can be forbidden
by the local controller. Although the general question is still open, we
show that the problem is decidable on acyclic architectures, albeit of
non-elementary complexity.

Joint work with B. Genest, H. Gimbert and I. Walukiewicz.
 Plus d'infos  


2011-10-13Weighted Expressions and Pebble Automata over Nested Words
11:30-12:30
L'Amphi
We introduce a calculus over nested words (or equivalently, trees) to express quantitative properties of XML documents or recursive programs. Our weighted expressions borrow purely logical constructs from XPath, but they also involve rational arithmetic expressions. The latter allow us to perform computations in an arbitrary (commutative) semiring. For instance, one can count how often a given entry occurs in an XML document, or compute the memory consumption of a program execution. We characterize a fragment of weighted expressions in terms of a new class of weighted automata. In the spirit of tree-walking automata, our device traverses a nested word along its edges and may place pebbles during a traversal.
After proving this expressiveness result, we give a list of interesting decision or computation problems, with some hints on their resolution, and a set of possible applications of these problems, depending of the chosen semiring.
 Plus d'infos  


2011-10-06Model Checking the Quantitative mu-Calculus on Infinite Transition Systems
11:30-12:30
076
We consider the model-checking problem for a quantitative
extension of the modal mu-calculus on two classes of infinite
quantitative transition systems. The first class, initialized linear
hybrid systems, is motivated by verification of systems which
exhibit continuous dynamics. We show that the value of a formula
of the quantitative mu-calculus can be approximated with arbitrary
precision on initialized linear hybrid systems. The other class,
increasing tree rewriting systems, is motivated by efforts to allow
counting formulas in discrete verification. On such systems, we
show that the value of a quantitative formula can be computed
exactly. For both these classes of systems, the problem in the end
reduces to solving a new form of parity games with counters.
 Plus d'infos  


2011-09-29Quantitative Verification and Synthesis
11:30-12:30
076
Quantitative constraints have been successfully used to state and
analyze non-functional properties such as energy consumption,
performance, or reliability. Functional properties are typically
viewed in a purely qualitative sense. Desired properties are written
in temporal languages and the outcome of verification is a simple Yes
or No answer stating that a system satisfies or does not satisfy the
desired property. We believe that this black and white view is
insufficient both for verification and for synthesis. Instead, we
propose that specifications should have a quantitative aspect.

Our recent research shows that quantitative techniques give new
insights into qualitative specifications. For instance,
average-reward properties allow us to express properties like default
behavior or preference relations between implementations that all
satisfy the functional property. These additional properties are
particularly useful in a synthesis setting, where we aim to
automatically construct a system that satisfies the specification,
because they allow us to guide the synthesis process making the outcome
of synthesis more predictable.

In this talk I will give an overview of
(1) how classical specification can be augmented with quantitative constraints,
(2) list different quantitative constraints that arise in this way, and
(3) show how to verify and synthesize systems that satisfied the
initial specification and optimize such quantitative constraints.

This is joint work with R. Bloem, K. Chatterjee, K. Greimel, T. Henzinger,
A. Radhakrishna, R. Singh, and C. von Essen.
 Plus d'infos  


2011-09-22Model checking vector addition systems with one zero-test
11:30-12:30
076
We design a variation of the Karp-Miller algorithm to compute a
finite representation of the cover (i.e., the downward closure of
the reachability set) of a vector addition system with one
zero-test. This algorithm yields decision procedures for several
problems on these systems, open until now, such as
place-boundedness or LTL model-checking.

The proof techniques to handle the zero-test are based on two new
notions of cover: the refined and the filtered cover. The refined
cover is hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality
of two refined covers is undecidable, even for usual Vector
Addition Systems (with no zero-test), but the refined cover of a
Vector Addition System is a recursive set. The second notion of
cover, called the filtered cover, is the central tool of our
algorithms. It inherits properties of the classical cover, and in
particular, one can effectively compute a finite representation
of this set, even for Vector Addition Systems with one zero-test.
 Plus d'infos  


2011-06-30A game approach to determinize timed automata
11:30-12:30
Salle 076
Timed automata are frequently used to model real-time systems.
Their determinization is a key issue for several validation problems.
However, not all timed automata can be determinized, and determinizability
itself is undecidable. In this talk, we will present a game-based algorithm
which, given a timed automaton,
tries to produce a language-equivalent deterministic timed automaton,
otherwise a deterministic over-approximation. Our method subsumes two
recent contributions: it is at once more general than a recent determinization
procedure and more precise than the existing over-approximation algorithm.Then, we will explain how this method can be adapted to be usefull for test generation.
This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers will be presented at FoSSaCs'11 and TACAS'11.
 Plus d'infos  


2011-06-23Génération de séquences de pannes de modèles AltaRica
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Les analyses de sûreté visent à réduire la probabilité
d'occurrence d'incidents critiques dans un système. Un des moyens
d'évaluer cette probabilité est de calculer les principales
combinaisons de pannes des composants du système qui engendrent
l'incident critique étudié. Cet ensemble de combinaisons permet
ensuite d'évaluer, éventuellement de manière pessimiste, la
probabilité de défaillance du système.

Lors de ce séminaire je présenterai comment nous avons utilisé de
vieilles recettes pour calculer l'ensemble des séquences critiques
d'un système modélisé en langage AltaRica.

Ces algorithmes sont désormais disponibles dans ARC, le model-checker
pour AltaRica.

La présentation sera en français.
 Plus d'infos  


2011-06-09Vers un modèle de contrôle temps-réels, hiérarchique, concurrent et réactifs
11:30-12:30
076
A priori, tout et dans le titre, les mots clés qui le composent et les questions qui en découlent. Quelles peuvent être les motivations pour définir de tels contrôleurs ? Comment ordonner les paradigmes (parfois transversaux) de modélisation qu'ils doivent inclure ? Que sait-on déjà de ce type de contrôleurs ? Comment le modèle qui s'impose peut-il être relié aux notions déjà existantes d'automates d'états finis, d'automates synchrones, d'automates à piles, de diagrammes d'états (statecharts), d'automates temps réels, de modèles de flux synchrones, etc....
Dans cet exposé, à travers la définition d'un modèle de contrôleurs qui tente d'intégrer tout les paradigmes évoqués, je tâcherais d'illustrer par l'exemple quelques éléments de réponses à ces questions en m'appuyant notamment sur la problématique de "la modélisation à visée applicative" qui agit comme un filtre à concepts selon le principe "si ça marche, ça doit avoir des propriétés mathématiques intéressantes".
 Plus d'infos  


2011-05-19Power of Randomization in Finite State Monitoring
11:30-12:30
076
We introduce the model of finite state probabilistic monitors (FPM), which are finite state automata on infinite strings that have probabilistic transitions and an absorbing reject state. FPMs are a natural automata model that can be seen as either randomized run-time monitoring algorithms or as models of open, probabilistic reactive systems that can fail. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of languages recognized by FPMs. We also study the emptiness and universality problems for such automata and give exact complexity bounds for these problems. Joint work with A. Prasad Sistla and Mahesh Viswanathan.
 Plus d'infos  


2011-05-12Hybrid syntactic/semantic computer virus detection scheme
11:30-12:30
076
The detection problem in computer virology is known to be undecidable. Nonetheless, a large body of work is still devoted to the subject. We will present the state of the art on detection schemes: the syntactic and semantic detection schemes.

Subsequently, we will introduce a new hybrid syntactic/semantic detection scheme, where the extraction of the virus signature is performed through abstract interpretation techniques while virus detection is let to efficient syntactic detectors. We will present a new abstract domain that is able to automatically extract the signature of a polymorphic virus as a context free grammar. Preliminary results on some real polymorphic virus samples will also be shown.
 Plus d'infos  


2011-05-05Computing Optimal Strategies for Markov Decision Processes with Parity and Positive-Average Conditions
11:30-12:30
076
We study Markov decision processes (one-player stochastic games)
equipped with parity and positive-average conditions.

In these games, the goal of the player is to maximize the probability that both the
parity and the positive-average conditions are fulfilled.
We show that the values of these games are computable in polynomial time.
We also show that optimal strategies exist, require only finite memory and can be effectively computed.

Joint work with Hugo Gimbert and Soumya Paul.
 Plus d'infos  


2011-04-28A lazy reachability algorithm for timed automata
11:30-12:30
076
We consider the classic reachability problem for timed automata:
given an automaton, decide if there exists a path from its initial state
to a given target state. The standard solution to this problem involves
computing the *zone graph* of the automaton, which in principle could be
infinite. In order to make the graph finite, zones are approximated using
an extrapolation operator. For reasons of efficiency it is required that an
extrapolation of a zone is always a zone; and in particular that it is *convex*.

We propose a new solution to the reachability problem that uses no
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the
*region closure* of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.

The structure of this new algorithm permits to calculate
approximating parameters on-the-fly during exploration of the zone
graph, as opposed to the current methods which do it by a static
analysis of the automaton prior to the exploration. This allows for
further improvements in the algorithm. Promising experimental results
are presented.

Joint work with Frédéric Herbreteau, Dileep Kini, Igor Walukiewicz

 Plus d'infos  


2011-04-07Contraintes sur le temps logique dans la conception de systemes embarques
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Je presenterai un langage de contrainte permettant d'exprimer des contraintes chronologiques et causales
sur les evenements du systeme (horloges logiques) et certains de mes travaux en cours sur ce langage: d'une
part la comparaison de ce langage avec la logique temporelle lineaire et d'autre part l'extension de ce langage
avec un systeme de priorites.
 Plus d'infos  


2011-02-17Unfoldings of contextual Petri nets
07:00-07:00
Salle 076, LaBRI, Rez-de-chaussée
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finite-state) Petri nets, which can be used for verification purposes.

Contextual nets are a generalisation of Petri nets suited to model systems with read-only access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan's construction to a suitable encoding of the contextual net into an ordinary net.

However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. We propose a an unfolding algorithm that works for arbitrary semi-weighted, bounded contextual nets.

The talk is based on joint work with Paolo Baldan, Andrea Corradini, and Barbara Koenig.
 Plus d'infos  


2011-02-03Global Model Checking of Ordered Multi-Pushdown Systems
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
In this talk, we address the verification problem of ordered multi-pushdown systems, a multi-stack extension of pushdown systems that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time µ-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of w-regular properties for ordered multi-pushdown systems (matching its lower-bound).
 Plus d'infos  


2010-12-16Energy and Mean-Payoff Games
11:30-12:30
Salle 076, LaBRI, Rez-de-chaussée
We consider game models for the design of reactive systems
working in ressource-constrained environments.
In mean-payoff games, the ressource usage is computed as
the long-run average ressource level.
In energy games, the ressource usage is the intial amount
of ressource necessary to maintain the ressource level positive.
The resource can be memory, battery, or network usage for example.

While mean-payoff games are a well-established model in game theory
and computer science, energyy games have received attention only recently.
The talk reviews recent results about these games and their relationship.
Although they differ very basically in their definition,
it is known that energy and mean-payoff games are equivalent for
the simple decision problem of existence of a winning strategy.
This observation provides new complexity results for solving
mean-payoff games, and new insights for mean-payoff games combined
with other conditions such as fairness, imperfect information,
or multi-ressource systems, though the strong equivalence with
energy games usually breaks in such cases.
 Plus d'infos  


2010-12-09What Can You Verify and Enforce at Runtime ?
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Runtime verification is an effective technique to ensure at execution time that a system meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together untrusted software components. In runtime verification, a run of the system under scrutiny is analyzed incrementally using a decision procedure: a monitor. This monitor may be generated from a user-provided high level specification (e.g. a temporal property, an automaton). Runtime enforcement is an extension of runtime verification aiming to circumvent property violations. In runtime enforcement the monitors watch the current execution sequence and modify the execution sequence of the underlying program whenever it deviates from the desired property. More than simply halting an underlying program, some enforcement mechanisms can also ``suppress'' (i.e. freeze) and ``insert'' (frozen) actions in the current execution sequence. Runtime verification and enforcement have
proved to be effective techniques to achieve software reliability.

The questions we consider in this talk are the following: what are the classes of properties that can be verified and enforced at runtime, and is there a difference between the techniques we are interested in? These questions are not new, but we propose here to address them within a unified framework: the Safety-Progress classification of properties introduced by Manna and Pnueli.

In this talk, we start first by customizing the Safety-Progress classification in a runtime verification and enforcement context. Then we revisit the existing classical definition of monitorability, and
characterize the set of monitorable properties according to this definition. Then, we parameterize this definition according to the truth-domain under consideration. Moreover, we introduce a new definition of monitorability based on distinguishability of ``good'' and ``bad'' execution sequences. This definition is weaker than the classical one, but we believe that it better corresponds to practical needs and tool implementations. Furthermore, we characterize the set of enforceable properties in a way that is independent from any enforcement mechanism. A consequence is that the proposed set of enforceable properties is an upper bound of any enforcement mechanism.

This is joint work with Pr. Jean-Claude Fernandez and Dr. Laurent Mounier from Vérimag (Grenoble).
 Plus d'infos  


2010-12-02Efficient Emptiness Check for Timed Büchi Automata
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
The Büchi non-emptiness problem for timed automata concerns deciding
if a given automaton has an infinite non-Zeno run satisfying the
Büchi accepting condition. The standard solution to this problem involves
adding an auxiliary clock to take care of the non-Zenoness. In this talk, we
show that this simple transformation may sometimes result in an
exponential blowup. Then, we propose a method avoiding this blowup.
However, in many cases, no extra construction is needed to ascertain
non-Zenoness. Hence, we finally present an on-the-fly algorithm for the
non-emptiness problem, using an efficient non-Zenoness construction
only when required.
 Plus d'infos  


2010-10-21The complexity of Nash Equilibria in Reward Games
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
We study the complexity of Nash equilibria in games with limit-average objectives. While an arbitrary Nash equilibrium of such a game can be found in polynomial space, we show that deciding whether a game has an equilibrium whose payoff meets certain constraints is, in general, undecidable. A more refined analysis takes into account the complexity of the strategies that realise the equilibrium. While for stochastic games, the above problem is undecidable for both pure and randomised strategies, the problem becomes decidable when one looks for a pure-strategy equilibrium in a non-stochastic game.
 Plus d'infos  


2010-10-14Expected Reachability-Time Games
11:30-12:45
Salle 178, LaBRI
In an expected reachability-time game (ERTG) two players, Min and
Max, move a token along the transitions of a probabilistic timed automaton,
so as to minimise and maximise, respectively, the expected time to reach a
target. We show that ERTGs are positionally determined. Using the boundary
region graph abstraction, and a generalisation of Asarin and Maler’s
simple function,
we show that the decision problems related to computing the value of ERTGs
are decidable and their complexity is in NEXPTIME ∩ co-NEXPTIME.
 Plus d'infos  


2010-10-07Traitement et programmation synchrone des flux musicaux
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Notre exposé repose sur le couplage de deux thématiques souvent
considérées comme distinctes, mais qui sont indissociables dans un
contexte musical :
(1) Traitement et reconnaissance temps réel des flux sonores
(2) Langage de programmation synchrone pour l'informatique musicale
Ce couplage émerge de la pratique musicale et compositionnelle,
faisant appel aux formalismes d'écriture synchrone et concurrente,
comme un système réactif aux jeux des musiciens en temps réel. Le
premier volet nous ramène aux problèmes des représentations
hétérogènes propres à l'information musicale avec des solutions
proposées venant de la littérature émergeant de la géométrie de
l'information. Le deuxième au temps hétérogène dans écriture des
processus musicaux et des systèmes hybrides. L'incarnation actuelle de
ces deux thématiques est la recherche et développement autour de
l'environnement Antescofo, un jeune langage de programmation synchrone
pour la composition musicale couplée avec la reconnaissance des
paramètres musicaux lors d'une performance temps réel.

liens: http://imtr.ircam.fr/imtr/Score_Following
http://imtr.ircam.fr/imtr/Music_Information_Geometry
 Plus d'infos  


2010-09-30The Vector Addition System Reachability Problem
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. The new proof is based on the notion of productive sequences inspired from Hauschildt that directly provides the existence of Presburger inductive invariants.
 Plus d'infos  


2010-09-16Distributed Timed Automata with Independently Evolving Clocks
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
We propose a model of distributed timed systems where each component is a
timed automaton with a set of local clocks that evolve at a rate independent
of the clocks of the other components. A clock can be read by any component in
the system, but it can only be reset by the automaton it belongs to. Since we
have unrelated time values on different components, we are interested in the
underlying untimed behaviors of these distributed timed automata rather than
their timed behaviors. Thus, the clocks (and time itself) are synchronization
tools rather than being a part of the observation.

There are two natural semantics for such systems. The universal semantics
captures behaviors that hold under any choice of clock rates for the
individual components. Thus, it can be considered as an underapproximation
of the actual behavior. This is a natural choice when checking that a system
always satisfies a positive specification. However, to check if a system
avoids a negative specification, it is better to use the existential
semantics (an overapproximation of the actual system behavior): the set of
behaviors that the system can possibly exhibit under some choice of clock
rates.

We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness or
universality turns out to be undecidable, which is shown by a reduction from
Post’s correspondence problem. This result is further strengthened to some
bounded cases, where we have restrictions on the relative time rates such as
fixed slopes.

As an alternative to the universal semantics, we propose a game-based
reactive semantics that allows us to check positive specifications and yet
describes a regular set of behaviors.

This is joint work with S. Akshay, Paul Gastin, Madhavan Mukund, and
K. Narayan Kumar.
 Plus d'infos  


2010-07-01Solving Simple Stochastic Tail Games
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Stochastic games are a natural model for open reactive processes: one player represents the controller and his opponent represents a hostile environnment. The evolution of the system depends on the decisions of the players, supplemented by random transitions. There are two main algorithmic problems on such games: computing the values (quantitative analysis) and deciding whether a player can win with probability 1 (qualitative analysis). In this paper we reduce the quantitative analysis to the qualitative analysis: we provide an algorithm for computing values which uses qualitative analysis as a sub- procedure. The correctness proof of this algorithm reveals several nice properties of perfect-information stochastic tail games, in particular the existence of optimal strategies. We apply these results to games whose winning conditions are boolean combinations of mean-payoff and Buchi conditions.
 Plus d'infos  


2010-06-03A formal framework for social Networking
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
The talk presents Popar, an ongoing project that aims at using several formal
methods tools and techniques to develop a full-fledged social-network service implementing stipulated policies. The system includes a B method definition for social networking, modelling social-network content, privacy policies, social-networks friendship relations, and how these relations affect users' policies. This core is expected to be extended by third-party plug-ins in such a way that adherence to system policies is guaranteed by formal techniques such as proof-carrying code.
 Plus d'infos  


2010-05-27Static analysis of positional and non positional properties of arrays
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
(joint work with Mathias Péron and Valentin Perrelle)

Although array bound checking was a motivation of the very first
work on abstract interpretation, there are only few proposals about
dealing with array *contents* in program analysis. The reason is,
of course, that the general problem is difficult: array indexing
induces complex semantics, and in particular the possibility of
aliasing; moreover, since the size of an array can be large or
unknown, it represents a large or unbounded number of variables.

In this talk, we present two complementary analyses dealing with
properties of array contents in some simple cases: one-dimensional
arrays, traversed by simple "for" loops. Both analyses are based
on abstract interpretation:
- the first one aims at discovering positional properties of arrays
elements. For instance, it is able to discover that the result of
an insertion sort is a sorted array.
- the second one addresses non positional properties, like the
fact that, at some point of a program, the content of an array is
a permutation of its initial content.
 Plus d'infos  


2010-05-20Implicit Real Vector Automata
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
This work addresses the efficient handling of non-convex real
polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean
combinations of linear constraints. We develop a symbolic data
structure for representing such sets, based on an implicit and concise
encoding of a known structure, the Real Vector Automaton. The
resulting formalism provides a canonical representation of non-convex
polyhedra, is closed under Boolean operators, and admits an efficient
decision procedure for testing the membership of a vector.

Joint work with Julien Brusten and Jean-François Degbomont
 Plus d'infos  


2010-04-22Datalog-based Program Analysis with BES and RWL
10:00-11:15
Salle 050, LaBRI, Rez-de-chaussée
In this talk, we present two powerful, fully automated methods to
evaluate Datalog queries in the context of object-oriented program
analyses: the first approach transforms the Datalog program in an
implicit Boolean Equation Systems (BESs) solved by existing general
purpose verification toolboxes, such as CADP, providing local BES
resolutions with linear-time complexity; the second approach
transforms Datalog programs into Rewriting Logic and produces an
efficient rewrite system exploiting the main features of the
high-level programming language Maude. Datalog is used as a
specification language for expressing both complex interprocedural
program analyses involving dynamically created objects and queries. We
confirm our results experimentally by applying it to some real-world
Datalog-based analyses.
 Plus d'infos  


2010-04-15Volume and entropy of regular timed languages
11:30-12:30
Salle 076, LaBRI, Rez-de-chaussée
For timed languages, we define measures of their size: volume for a fixed finite number of events, and entropy (growth rate) as asymptotic measure for an unbounded number of events. These measures can be used for comparison of languages, and the entropy can be viewed as information contents of a timed language. In case of languages of deterministic timed automata, we give exact formulas for volumes. Next we characterize the entropy, using methods of functional analysis, as a logarithm of the leading eigenvalue (spectral radius) of a positive integral operator. We devise several methods to compute the entropy: a symbolical one for so-called “1 1/2-clock" automata, and two numerical ones: one using techniques of functional analysis, another based on discretization.

(joint work with Aldric Degorre, Concur'09+ Formats'09)
 Plus d'infos  


2010-04-01When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (one-counter machines, reversal-bounded counter machines, vector additions systems with states, flat counter machines). Freeze LTL is an extension of the linear temporal logic to which registers are added. In this logic, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. We provide a systematic classification for the model-checking problem of freeze LTL over counter machines that distinguishes determinism vs. nondeterminism and we also consider subclasses of formulae by restricting the set of atomic formulae or/and the polarity of the occurrences of the freeze operators, leading to the flat fragment.

This is a joint work with Stéphane Demri (LSV, CNRS, ENS de Cachan) and Ranko Lazic (Department of Computer Science, University of Warwick).
 Plus d'infos  


2010-03-11Static Analysis of x86 Executables
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Due to indirect branch instructions, analyses on executables commonly
suffer from the problem that a complete control flow graph of the
program is not available. Data flow analysis has been proposed before
to statically determine branch targets in many cases, yet a generic
strategy without assumptions on compiler idioms or debug information
was missing.

We have devised a framework for generic low level programs with
indirect jumps which safely combines a pluggable abstract domain with
the notion of partial control flow graphs. Using our framework, we
were able to show that the control flow reconstruction algorithm of our
disassembly tool Jakstab produces the most precise overapproximation
of the control flow graph with respect to the used abstract domain.

Based on this rigorous approach to disassembly, Jakstab has evolved
into a flexible program analysis framework on binaries. Preliminary
experiments with Windows driver binaries show that it can successfully
check API specifications with higher precision than existing
approaches, while achieving complete independence from source code.
 Plus d'infos  


2010-02-25Craig Interpolation for Quantifier-Free Presburger Arithmetic
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Craig interpolation has become a versatile tool in formal verification,
for instance to generate intermediate assertions for safety
analysis. Interpolants are often determined by annotating the steps
of an unsatisfiability proof with partial interpolants. In this
talk, I consider Craig interpolation for full quantifier-free
Presburger arithmetic (QFPA), for which until recently no efficient
interpolation procedures were known. As one such procedure, I introduce
an interpolating sequent calculus for QFPA and prove it to be sound
and complete. In particular, the complexity of extracting interpolants
from proofs is discussed. Finally, I add support for uninterpreted
predicates to the calculus, thus extending it to important theories such
as arrays and uninterpreted functions.

The talk describes joint work with Angelo Brillout, Daniel Kroening, and
Thomas Wahl.
 Plus d'infos  


2010-02-18On non-deterministic automata for Presburger arithmetic.
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
A well-known decision procedure for Presburger arithmetic (PA)
uses deterministic finite-state automata. While the complexity
of the decision procedure for PA based on quantifier elimination
is known (triple-exponential), the exact complexity of the
automata-based procedure was unknown. We show that it is triple-exponential
as well by analysing the structure of the non-deterministic automata
obtained during the construction building on results from Klaedtke.
Furthermore, we analyse the sizes of deterministic and non-deterministic
automata built for several subclasses of Presburger arithmetic.
To retain a canonical representation which is one of the strengths of
the use of automata we use a class of non-deterministic automata
called residual finite-state automata introduced by Denis, Lemay and Terlutte.
 Plus d'infos  


2010-02-11Towards a Computational Modeling of an Heterogeneous System for Interactive Musical Scores
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Interactive scores (IS) are a formalism for composition and performance of musical pieces composed by temporal objects, temporal structures and discrete interactive events. IS may be used for the composition and performance of Electroacoustic music; to control image, video, audio and lights on live spectacles and interactive museums; and to help handicapped and begginer musicians to perform a difficult piece. Currently, there is not an IS model that allows temporal constraints, logical branching, global constraints, and audio/video streams simultaneusly. We propose using the FAUST system to process audio/video streams and the Non-deterministic Timed Concurrent Constraint (ntcc) calculus to cope with the other phenomena. We plan to develop a model for IS, where ntcc and FAUST interact, and to use model checking techniques to verify it*.

*This is one of the objectives to accomplish in my doctorate, which I started on october 2009.
 Plus d'infos  


2010-02-04Recurrence and Transience for Probabilistic Automata
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Dans le context des automates de Buchi sur les mots infinis, la
condition d'acceptation classique (de Buchi) pour un run est qu'il passe
infiniment souvent sur un etat acceptant. Un mot est alors accepté s'il
existe un run acceptant pour ce mot. Dans un contexte d'automates
probabilistes (PBA), un mot est accepté si la probabilité de l'ensemble
des runs pour ce mot qui passent infiniment sur un etat acceptant est
strictement positive. Avec cette definition, il devient indecidable de
decider si le language d'un PBA est vide ou non. On relaxe la definition
d'acceptation d'un run en demandant maintenant que la proportion du temps
passé sur un des etats acceptants ne tend pas vers zero. Decider le vide
du language devient alors decidable. Nous etudions la complexité du
probleme de decision associé (PSPACE complet), et nous etudions les
propriétés de cloture de notre nouvelle classe d'automates probabilistes.
L'essentiel de l'etude se ramene à l'etude de la notion de recurrence dans
le cas des chaines de Markov non-homogenes.
 Plus d'infos  


2010-01-14L'approche SAT pour lpour automates temporisés avec étapes parallèles
11:30-12:45
Salle 076, LaBRI, Rez-de-chaussée
Plusieurs travaux ont exploré la possibilité d'améliorer les algorithmes d'exploration d'états symboliques (zones) pour automates temporisés par une sémantique d'ordres partiels. A priori, ces sémantiques sont contre-intuitives, parce que le temps, représenté par des nombres réels, est un ordre total.
D'un autre coté, pour des systèmes non-temporisés, on connaît des réductions SAT qui utilisent une sémantique avec transitions parallèles : la possibilité d'exécuter plusieurs transitions indépendantes en parallèle raccourcit des séquences témoin et permet ainsi d'aller plus loin avec la vérification bornée.
Dans notre travail, nous combinons les deux améliorations, ordres partiels pour automates temporisés et transitions parallèles pour une meilleure réduction SAT. Il se pose alors la question de ce que sont des « transitions parallèles » pour un automate temporisé. Autre que la réponse intuitive « en parallèle est en même temps » nous explorons deux autres sémantiques avec des notions plus relâchées pour les transitions parallèles. Il s'avère que les trois sémantiques ont des performances incomparables, selon les exemples considérés.
À l'occasion, je présente aussi le vérificateur POEM, qui est la plate forme expérimentale avec laquelle nous avons réalisé le prototype et les expériences.
 Plus d'infos  


2010-01-07Un Langage Synchrone pour les Systèmes Embarqués Critiques Temps Réel
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Ce séminaire sera l'occasion de présenter les travaux effectués au cours de ma thèse.
L'exposé porte sur la programmation de systèmes de Contrôle-Commande. Ces systèmes sont constitués d'une boucle de contrôle qui acquiert l'état actuel du système par des capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Ces systèmes sont critiques, leur implantation doit donc être déterministe, sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates).

Nous définissons un langage de description d'architecture logicielle temps réel et son compilateur pour programmer de tels systèmes. Il permet d'assembler les composants fonctionnels d'un système multi-rythme avec une sémantique formelle synchrone. Un programme consiste en un ensemble d'opérations importées, reliées par des dépendances de données. Des contraintes de périodicité ou d'échéance peuvent être spécifiées sur les opérations et un ensemble réduit d'opérateurs de transition de rythme permet de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes.

Des analyses statiques assurent que la sémantique d'un programme est bien définie. Un programme correct est ensuite compilé en un ensemble de tâches temps réel concurrentes implantées sous forme de threads C communicants. Le code généré préserve la sémantique du programme
original et s'exécute à l'aide d'un Système d'Exploitation Temps Réel standard disposant de la politique d'ordonnancement EDF.
 Plus d'infos  


2009-12-17Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk, we show how to apply recent tools for the automatic synthesis of robust and near-optimal controllers for a real industrial case study. We show how to use three different classes of models and their supporting existing tools, UPPAAL - TIGA for synthesis, PHAVER for verification, and SIMULINK for simulation, in a complementary way.
 Plus d'infos  


2009-12-10Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents.
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Les systèmes d'addition de vecteurs arborescents (BVAS) forment un modèle
formel de calcul qui est
utilisé par exemple en linguistique ou pour la vérification de protocoles
cryptographiques. Ce modèle a
aussi des liens étroits avec des logiques de données interprétées sur des
arbres avec valeurs mais aussi
avec la logique linéaire MELL. La décidabilité du problème d'accessibilité
pour ces systèmes demeure
encore aujourd'hui ouverte, et ce problème est équivalent à divers
problèmes essentiels des domaines
cités plus haut.
Récemment, Verma et Goubault-Larrecq ont réussi à montrer que les
problèmes de finitude et de
couverture pour les BVAS sont décidables.

Dans cet exposé, je vais présenter comment caractériser la complexité des
problèmes de couverture
et de finitude pour les BVAS. Une partie de la preuve consiste à raffiner
les travaux de Rackoff dans le
cas linéaire correspondant au modèle des réseaux de Petri.

Ce travail a été mené conjointement avec Marcin Jurdzinski, Oded Lachish
et Ranko Lazic
(University of Warwick, UK).
 Plus d'infos  


2009-12-03Alternating-time Temporal Logic: Expressivity, Complexity, Extensions
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk we will consider several temporal logics for
expressing properties over games (modeled with
Concurrent Game Structures).
We will present ATL, ATL* and also two extensions:
with strategy contexts and with memory constraints.
The first extension makes strategy quantifiers to
not ``forget'' the strategies being executed by the other players.
The second extension allows strategy quantifiers to restrict to
memoryless or bounded-memory strategies.

We will first consider expressiveness issues. We show that our logics can
express important properties such as equilibria, and we formally
compare them with other similar formalisms ATL, ATL*, Game Logic, AMC,
Strategy Logic,... We will also address the problem of model-checking
for these logics.

Joint work with: Th. Brihaye, A.. Da Costa, N. Markey.
 Plus d'infos  


2009-11-26Games on Infinite Domains and Approximation
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
I'll give an overview of research I have been
doing over the last few years in semantic models
of mixed non-deterministic and probabilistic choice.
One can also see this as models for two-player
turn-based (stochastic) games, where the state space
X is infinite. The approach is topological and
domain-theoretical. In particular, X need not
be Hausdorff, which leads to interesting models
where the knowledge of the current state can itself
be approximate.
We shall give a brief tour of these, through capacity-based
models, prevision models, simulation and (if time
permits) simulation (hemi-)metrics.
 Plus d'infos  


2009-11-12Reachability Analysis of Communicating Pushdown Systems
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The reachability analysis of recursive programs that communicate
over asynchronous and reliable fifo channels calls for restrictions
to ensure decidability. We extend here a model proposed by La Torre,
Madhusudan and Parlato [TACAS08], based on communicating pushdown
systems that can dequeue with empty stack only. Our extension adds
the dual modality, which allows to dequeue with non-empty stack, thus
modelling interrupts for working threads. We study (possibly cyclic)
network architectures under a semantic assumption (mutex
communication) that ensures the decidability of reachability for
finite state systems. Subsequently, we determine precisely how
pushdowns can be added to this setting while preserving the
decidability; in the positive case we obtain exponential time as the
exact complexity bound of reachability. A second result is a
generalization of the doubly exponential time algorithm of [LaTorre
et al: TACAS08] for bounded context analysis to our symmetric
queueing policy. We provide here a direct (and simpler) proof.

Joint work with Jérôme Leroux, Anca Muscholl, Grégoire Sutre
 Plus d'infos  


2009-11-05On the Verification Problem for Weak Memory Models
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We address the verification problem of finite-state concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multi-processor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performance-critical system services employing lock-free synchronization, as well as for the correctness of compiler backends that generate code targeted to run on such architectures.

We consider in this work combinations of three well-known program order relaxations. We consider first the "write to read" relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the "write to write" relaxation (leading to a model which is essentially PSO), or (2) the "read to read/write" relaxation, or (3) both of them (as it is done in the RMO model for instance).

We define abstract operational models for these weak memory models based
on state machines with (potentially unbounded) FIFO buffers, and we
investigate the decidability of their reachability and their repeated
reachability problems.

We prove that the reachability problem is decidable for the TSO model, as well as for its extension with "write to write" relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the "read to read/write" relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. As for the repeated reachability problem, we prove that it is undecidable already for the TSO model.

(Joint work with Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi)
 Plus d'infos  


2009-10-22Control of Infinite Symbolic Transition Systems under Partial Observation
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We propose algorithms for the synthesis of state-feedback
controllers through partial observation of infinite state systems
modelled by Symbolic Transition Systems.

To obtain algorithms for solving these problems, we use abstract
interpretation techniques which provide over-approximations of the
transitions set to be disabled.

We implemented those algorithm in a tool and made an empirical validation of our
methods to show their feasibility and usability.


Keywords: Symbolic Transition Systems, Control Synthesis,
Partial Observation, Abstract Interpretation.


Joint work with Gabriel Kalyon, Tristan Le Gall, Hervé Marchand and Thierry Massart.
 Plus d'infos  


2009-09-29Parity Games on Multistack Systems
11:00-12:15
Salle 075, LaBRI, Rez-de-chaussée
In this talk we present higher order multi-stack
pushdown systems (hmpds). We show that parity games
over bounded phase hmpds are effectively solvable and
winning strategy in these games can be effectively
synthesized.
The proof is by reducing the parity games over bounded
phase hmpds to finite state parity games. We shall
describe this reduction in some detail.
 Plus d'infos  


2009-06-18Edition Collaborative d'arbres XML
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
L'edition collaborative consiste à travailler sur un document commun de
manière distribuée et concurrente. Un problème essentiel est d'assurer la
cohérence du processus, car des opérations concurrentes peuvent etre
conflictuelles (ajouter ou supprimer une lettre à la meme position). De
nombreux systèmes reposent sur une centralisation implicite (par des
time-stamps par exemple) ou explicite (existence d'un site maitre comme avec
svn). L'approche Pair à Pair ne permet pas cette centralisation, et à tout
moment de nouveaux sites peuvent rejoindre le processus d'édition. Dans ce
cadre l'approche optimiste considère que toutes les opérations doivent etre
prises en compte, et utilise une approche transformationnelle pour intégrer
les opérations concurrentes: au lieu d'effectuer l'opération o2 concurrente à
o1, on effectue une opération modifiée IT(o1,o2). Quand l'opérateur de
transformation IT satisfait deux propriétés TP1 et TP2, il existe un
algorithme qui assure la convergence du processus (chaque site a la meme
copie du document à la fin du processus). Pour le cas des mots aucun des
jeux
d'opérations et des transformations proposées ne satisfont ces propriétés et
des contre-exemples montrent qu'ils n'assurent pas la convergence (cf thèse
d'A. Imine). Dans cet exposé nous nous intéressons à l'édition des arbres
étiquetés non-ordonnés avec des opérations d'ajout, suppression ou
réétiquetage. Le premier résultat est de montrer qu'il n'existe pas de
transformation satisfaisant TP1 et TP2 dans ce cadre. Le deuxième résultat
consiste à étendre la structure de données par des informations fournies
naturellement par le processus d'édition qui garantissent l'unicité des
étiquettes et de montrer que les propriétés TP1 et TP2 sont satisfaites ce
qui autorise l'edition collaborative sur cette structure. Finalement, nous
montrons comment garder ces propriétés en ajoutant une opération de
déplacement de sous-arbres à condition de modifier la structure de donnée en
ajoutant une mémoire. Nous terminerons en discutant le cas des arbres
ordonnés et le problème du undo (annulation d'une opération).

Travail en commun avec Stéphane Martin.
 Plus d'infos  


2009-06-04Contrôleurs non déterministes de processus non déterministes
11:00-12:15
Salle 076
Arnold, Vincent, Walukiewicz en 2003, puis Briand en 2006, on tracé une frontière entre les cas où la synthèse (centralisée ou décentralisée) de contrôleurs déterministes de processus déterministes est effective et ceux où elle est indécidable, lorsque les contrôleurs et le système contrôlé sont soumis à des contraintes d'inobservabilité et d'indiscernabilité exprimables dans un mu-calcul modal étendu.

En 2008 Arnold et Walukiewicz ont étendu ces résultats au cas où les contrôleurs et les processus ne sont pas nécessairement déterministes.

Ce sont ces extensions qui seront présentées.
 Plus d'infos  


2009-05-28When are Timed Automata Determinizable?
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We describe an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. Under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition we exhibit is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata).

This is a joint work with C. Baier, P. Bouyer and T. Brihaye.
 Plus d'infos  


2009-05-14What's decidable for Asynchronous Programs ?
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
An asynchronous or "event-driven'' program is one that contains
procedure calls which are not directly executed from the call site,
but stored and executed later by an external scheduler.
By providing a low-overhead way to manage concurrent interactions,
asynchronous programs form the core of many server programs, embedded
systems, and popular programming styles for the web (Ajax).
Unfortunately, such programs can be hard to write and maintain as
sequential control flow needs to be split into several disjoint
handlers.
They are a challenge for static analysis tools as they are infinite
state: both the program stack and the number of outstanding
asynchronous requests may be unbounded.
We show that safety and liveness properties can be checked effectively
for the class of Boolean asynchronous programs, thus enabling
automatic static techniques to check for correctness or for errors.
 Plus d'infos  


2009-05-07Well Structured Transition Systems everywhere and everytime !
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The theory of Well Structured Transition Systems provides the good structure for computing a finite basis of the set of predecessors of the upward closure of a finite set of states. We address here the dual problem which is to compute a finite representation of the set of successors of the downward closure of a finite set of states (called the cover). This last problem is, a priori, more difficult because in general, the cover has no finite basis.
It is possible to complete any well-ordered set to obtain a cpo in which every downward closed set has a finite representation.
We then define the framework of Complete Well Structured Transition Systems and we propose a simple and a conceptual procedure for computing the covering set and the covering graph. This procedure terminates more often than the generalized Karp-Miller tree procedure when applied on extended Petri nets and lossy channel systems.
 Plus d'infos  


2009-04-30Algorithmes de théorie des jeux en analyse statique de programme
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Nous ferons un tour d’horizon de résultats portant sur la
correspondance entre les équations de point fixe rencontrées en
analyse statique de programme par interprétation abstraite et celles
qui apparaissent dans l’approche par programmation dynamique des
jeux répétés à somme nulle. Cette correspondance permet en
particulier d’appliquer des algorithmes de type itération sur les
politiques afin de déterminer des invariants de nature numérique sur
le programme analysé (par exemple des invariants polyédraux).
Cependant, deux difficultés apparaissent. La première, très
inhabituelle, est que les jeux considérés peuvent avoir un taux
d’escompte négatif (l’ensemble des points fixes n’est plus alors
nécessairement connexe). Une seconde difficulté est que l’algorithme
d’itération sur les politiques le plus simple peut terminer avec un
point fixe non minimal, alors que c’est le point fixe minimal qui
fournit le meilleur invariant. Nous montrons cependant comment
utiliser des techniques de théorie de Perron-Frobenius non-linéaire
(rayons spectraux, calcul semi-différentiel) pour obtenir toujours
le plus petit point fixe, à condition que le taux d’escompte ne soit
pas négatif. Ces résultats sont issus d’une série de travaux avec
Éric Goubault, Matthieu Martel, Sylvie Putot, Alexandru Costan,
Ankur Taly, et Assale Adjé.
 Plus d'infos  


2009-04-23Robustesse environnementale dans les réseaux d'automates à seuil : théorie et application en biologie.
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Nous allons nous intéresser à l'influence des conditions de bords dans les réseaux d'automates booléens à seuil, objets mathématiques pertinents pour la modélisation des réseaux de régulation biologique. L'objectif est de montrer que les bords (qui peuvent représenter des potentiels électriques externes dans les réseaux de neurones et des flux d'hormones ou encore des micro-ARN dans les réseaux de régulation génétique) sont des éléments qui peuvent changer radicalement le comportement dynamique de tels réseaux, aussi bien dans le cas de réseaux théoriques tels que les automates cellulaires que dans celui des réseaux biologiques réels. La démarche scientifique proposée est de se focaliser dans un premier temps sur des réseaux dits "parfaits", énormément contraints sur la nature des interactions et la topologie de manière à obtenir des résultats théoriques sur Z^d. Ensuite, en relâchant progressivement les contraintes, nous mettrons en évidence, par simulation, des domaines d'influence des conditions de bord pour des réseaux plus complexes sur Z2. Enfin, pour faire un pas de plus en direction de la biologie, nous verrons que les conditions de bord jouent un rôle dans les réseaux réels. Nous présenterons alors une méthode générique d'étude de la robustesse environnementale des systèmes dynamiques réels (basée sur la notion de bassin d'attraction). Nous terminerons en présentant les résultats que cette méthode permet d'obtenir, dans le contexte des réseaux de régulation génétique, à propos de la morphogenèse florale de la plante Arabidopsis thaliana.
 Plus d'infos  


2009-04-02Extrapol, des systèmes de types dépendants à la sécurité système
11:00-12:15
Dans le domaine de la sécurité, l'un des problèmes récurrents est celui
de déterminer quels effets l'exécution d'un programme peut avoir sur le
système qui l'héberge. Ces effets peuvent prendre la forme de
modification de fichiers, de communication avec des processus,
d'installation de services web... Dans d'autres cas, c'est
l'installation d'un programme ou d'une bibliothèque qui pourra donner à
d'autres programmes des points d'entrée pour avoir ce même genre
d'effets, de manière potentiellement accidentelle et potentiellement
malicieuse.

Le plus fréquemment, pour détecter les effets d'un programme ou les
points d'entrée d'une bibliothèque, l'administrateur d'un système a le
choix entre des outils dynamiques (bacs à sable) et des outils
post-mortem (analyse de trace) -- mais pas réellement d'outils d'analyse
statique.

Au cours de notre exposé, nous présenterons une technique d'analyse
statique pour les propriétés de sécurité de code source écrit en langage
C. Nous partirons du modèle de sécurité SELinux, tel qu'intégré à de
nombreuses distributions de Linux, et nous avancerons progressivement
jusqu'à une notion de types avec effets et de types dépendants. La
technique a été implantée en OCaml, sous la forme d'un outil de
diagnostic automatique, Extrapol.
 Plus d'infos  


2009-03-19AltaRica : passé, présent et futur.
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
AltaRica est un formalisme qui a été défini pour la description fonctionnelle
et dysfonctionnelle des systèmes industriels critiques. Depuis la première
version du langage en 2000, différentes variantes et outils associés ont été
proposés. Aujourd'hui, ces outils sont réellement utilisés de façon
productive dans certaines entreprises.
Dans la première partie de l'exposé, je présenterai le formalisme initial et
sa sémantique. Je donnerais ensuite les diverses évolutions et les raisons
pour lesquelles elles ont été introduites.
La dernière partie de l'exposé listera des travaux futurs possibles dans le
cadre "AltaRica, un formalisme d'aide à la conception sûre de systèmes
critiques".
 Plus d'infos  


2009-03-12How to get decidability of distributed synthesis ?
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The distributed synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification.

Our general aim is to define natural conditions under which synthesis or control are decidable for distributed systems. It is known that these problems are undecidable for most synchronous systems. So in this work we study asynchronous systems which communicate through signals -- actions that are immediately received by the target process. Another main cause of undecidability comes from the specifications. Here, we consider emph{external} specifications over emph{partial orders}. External means that specifications only relate input and output actions from and to the environment and not internal signals exchanged by processes. We also ask for some natural closure properties of the specification. We obtain decidability for the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures.
 Plus d'infos  


2009-03-05 Modal Logics with Presburger constraints
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk, we present an extended modal logic EML with regularity constraints and
full Presburger constraints on the number of children that generalize graded modalities,
also known as number restrictions in description logics.
We show that the satisfiability problem for EML can be solved with polynomial space.
This extends a well-known and non-trivial PSPACE upper bound for graded modal logic.
Furthermore, we provide a detailed comparison with logics that contain
Presburger constraints and that are dedicated to query XML documents. As an
application, we provide a reduction from Sheaves logic SL into EML,
which allows to improve the best known upper bound for SL satisfiability.

This is a joint work with Denis Lugiez (LIF, Marseille, France).
 Plus d'infos  


2009-02-12Spécification et Contrôle des Systèmes temps-réel faibles
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Nous introduisons la Logique $WT_mu$ pour décrire les propriétés des systèmes temps-réel faibles et nous synthétisons les contrôleurs des ces systèmes lorsque les propriétés sont écrites en $WT_mu$.
 Plus d'infos  


2009-01-23Max-regular languages
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
A new class of languages of infinite words is introduced, called the
max-regular languages, extending the class of omega-regular languages.
The class has two equivalent descriptions: in terms of automata (a
type of deterministic counter automaton), and in terms of logic (weak
monadic second-order logic with a bounding quantifier). Effective
translations between the logic and automata are given.
 Plus d'infos  


2009-01-08Génération Automatique d'Approximations Régulières
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Etant donnés deux langages réguliers d'arbres I et B, et un système de
réécriture R, on ne peut pas décider si R*(I) et B ont une intersection
vide, même pour des systèmes de réécritures simples. Une approche pour
résoudre ce problème consiste alors à utiliser des approximations de
R*(I). Nous montrerons dans cet exposé comment une technique manuelle
d'approximations introduite par Th. Genet en 98 peut être automatisée,
notamment pour la vérification de protocoles cryptographiques.

 Plus d'infos  


2008-12-18CEGAR for Communicating Fifo Systems
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The automatic verification of asynchronous communication
protocols demands for methods that are able to process
infinite state spaces and emergent behaviour. Communicating
fifo systems are a standard model for distributed
processes which are represented by a set of finite
automata that exchange messages over a network of reliable,
unbounded fifo channels.

We utilize the counterexample-guided abstraction
refinement technique (CEGAR) for the automatic
verification of communicating fifo systems regarding
safety properties. This is accomplished with the help of
predicate abstraction and a predicate refinement strategy
relying on the computation of path
invariants based on an additional extrapolation operator
for recognizable languages.

The presentation of the verification algorithm is completed
by a brief presentation of a prototypical implementation.
 Plus d'infos  


2008-12-11XPath evaluation in linear time
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We consider a fragment of XPath where attribute values can only be tested for equality. We show that for any fixed unary query in this fragment, the set of nodes that satisfy the query can be calculated in time linear in the document size.
 Plus d'infos  


2008-12-04Analyzing Asynchronous Programs with Preemption
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Multiset pushdown systems have been introduced by Sen and Viswanathan as
an adequate model for asynchronous programs where some procedure calls
can be stored as tasks to be processed later. The model is a pushdown
system supplied with a multiset of pending tasks. Tasks may be added to
the multiset at each transition, whereas a task is taken from the
multiset only when the stack is empty. In this paper, we consider an
extension of these models where tasks may be of different priority
level, and can be preempted at any point of their execution by tasks of
higher priority. We investigate the control point reachability problem
for these models. Our main result is that this problem is decidable by
reduction to the reachability problem for a decidable class of Petri
nets with inhibitor arcs. We also identify two subclasses of these
models for which the control point reachability problem is reducible
respectively to the reachability problem and to the coverability problem
for Petri nets (without inhibitor arcs).

This is a joint work with Mohamed Faouzi Atig and Tayssir Touili.
 Plus d'infos  


2008-11-27On the Reachability Analysis of Acyclic Networks of Pushdown Systems
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We address the reachability problem in acyclic networks of pushdown systems. We consider
communication based either on shared memory or on message passing through unbounded
lossy channels. We prove mainly that the reachability problem between recognizable sets of
configurations (i.e., definable by a finite union of products of finite-state automata) is decidable
for such networks, and that for lossy channel pushdown networks, the channel language is
effectively recognizable. This fact holds although the set of reachable configurations
(including stack contents) for a network of depth (at least) 2 is not rational in general (i.e., not
definable by a multi-tape finite automaton). Moreover, we prove that for a network of depth 1,
the reachability set is rational and effectively constructible (under an additional condition on
the topology for lossy channel networks).

This is a joint work with Mohamed Faouzi Atig and Ahmed Bouajjani
 Plus d'infos  


2008-11-20Inferring Min and Max Invariants Using Max-plus Polyhedra
11:00-12:15
Salle 076
We introduce a new numerical abstract domain able to infer min and max invariants over
the program variables, based on max-plus polyhedra. Our abstraction is more precise than
octagons, and allows to express non-convex properties without any disjunctive
representations. We have defined sound abstract operators, evaluated their complexity,
and implemented them in a static analyzer. It is able to automatically compute precise
properties on numerical and memory manipulating programs such as algorithms on strings
and arrays.
 Plus d'infos  


2008-11-13Reversal-Bounded Counter Machines Revisited
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We extend the class of reversal-bounded counter machines by authorizing a finite number of alternations between increasing and decreasing mode over a given bound. We prove that extended reversal-bounded counter machines also have effective semi-linear reachability sets and enjoy the same properties as the original reversal-bounded counter machines. We also prove that the property of being reversal-bounded is undecidable in general even when we fix the bound, whereas this problem becomes decidable when considering Vector Addition System with States.

This is a joint work with Alain Finkel.
 Plus d'infos  


2008-11-06Quasi-Static Scheduling of Communicating Tasks
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining existence of quasi-static scheduling policies is undecidable. However, we show that the problem is decidable for the important sub-class of “data branching” systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components. This decidability result—which is non-trivial to establish—exploits ideas derived from the Karp and Miller coverability tree as well as the existential boundedness notion of languages of message sequence charts.


This is a joint work with philippe Darondeau, P.S. Thiagarajan and Shaofa Yang.
 Plus d'infos  


2008-10-16Logiques pour le model checking des chaînes de Markov à temps continu
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Markov chains are a well-known stochastic process that provide a
balance between being able to adequately model the system's behavior
and being able to afford the cost of the model solution.
Systems can be modelled directly as Markov chains, or with a higher-level
formalism for which Markov chains represent the underlying semantics.
Markov chains are widely used to study the performance of
computer and telecommunication systems.
The definition of stochastic temporal logics like Continuous Stochastic
Logic (CSL)
and its variant asCSL, and of their model-checking algorithms,
allows a unified approach
to the verification of systems, allowing the mix of performance evaluation and
probabilistic verification.


In this talk we present the stochastic logic CSLTA,
which is more expressive than
CSL and asCSL, and in which properties can be specified using automata
(more precisely, timed automata with a single clock).
The extension with respect to expressiveness allows the specification of
properties referring to the probability of a finite sequence of timed events.
A typical example is the responsiveness property
``with probability at least 0.75, a message sent at time 0 by a system A
will be received before time 5 by system B and the acknowledgment will be back at A before time 7'', a
property that cannot be expressed in either CSL or asCSL.
Furthermore, the choice of using automata rather than the
classical temporal operators
Next and Until should help in enlarging the accessibility of model checking to a larger
public.
We also present a model-checking algorithm for CSLTA.
 Plus d'infos  


2008-10-09A rewrite-based approach for security policies
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
We show how strategic rewriting and narrowing provide a foundational framework
for the compositional design, maintenance and verification of security policies.
Rewrite rules transform input terms representing policy requests into decision terms.
Strategies are used to explicitly control the rule application.
Parameterized queries are solved by narrowing.
Relying on the correspondences between the properties of the rewrite system and the policy it implements,
we are able to reuse existing proof techniques and analysis tools in the security policies context.


Joint work with Claude Kirchner and Anderson Santana de Oliveira
 Plus d'infos  


2008-09-25An Easy Algorithm For The General Vector Addition System Reachability Problem
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The reachability problem for Vector Addition Systems (VAS) or equivalently for Petri Nets is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney (KLMST) decomposition. This decomposition is difficult and it just has a non-primitive recursive upper-bound complexity. In this paper, we prove that if a final configuration is not reachable from an initial one, there exists a pair of Presburger formulas denoting an inductive separator proving this property. Since we can decide with any decision procedure for the Presburger arithmetic if pairs of Presburger formulas denote inductive separators, we deduce that there exist checkable certificates of non-reachability. In particular, there exists an easy algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by fairly enumerating finite sequence of actions and a second one that tries to prove the non-reachability by fairly enumerating pairs of Presburger formulas. Even if the KLMST decomposition is used for proving the termination, this algorithm is the very first one that can be implemented without using it.
 Plus d'infos  


2008-09-18(1) Utilisation de prouveurs SMT pour la preuve de programmes et (2) Vérification de propriétés de programmes avec Alt-Ergo
11:00-12:15
Salle 075, LaBRI, Rez-de-chaussée
(1)
Cet exposé présente l'utilisation de prouveurs SMT pour la preuve de
programmes C et Java dans le cadre de la plateforme Why
(http://why.lri.fr/). En particulier, on justifie le choix d'une logique
du premier ordre polymorphe comme langage d'entrée pour utiliser les
différents prouveurs SMT, et on explique comment cette logique est
encodée lorsque le prouveur SMT ne l'implante pas nativement.
Cet exposé indique également quelles sont les théories pertinentes pour
la vérification de programmes, et comment leur absence dans certains
prouveurs SMT peut être contournée à l'aide de modèles axiomatiques.
Enfin, on explique comment les prouveurs SMT peuvent être utilisés
depuis l'assistant de preuve Coq, lorsque la preuve interactive devient
nécessaire.


(2)
Alt-Ergo est un démonstrateur automatique de théorèmes dédié à la
vérification de propriétés de programmes. Les formules logiques
envoyées à Alt-Ergo sont écrites dans la logique du 1er ordre
polymorphe multi-sortée de l'outil Why.

Dans cet exposé nous décrirons l'architecture d'Alt-Ergo. Elle est
composée d'un SAT-solver qui interagit avec un algorithme de
combinaison de procédures de décision et un mécanisme d'instanciation
pour traiter les formules quantifiées.

Le code d'Alt-Ergo est très court (environ 4000 lignes d'Ocaml) ce qui
en fait un bon candidat pour réaliser la preuve en Coq d'un
démonstrateur automatique. Alt-Ergo est disponible à
http://alt-ergo.lri.fr
 Plus d'infos  


2008-06-12Fixpoint-based Abstraction Refinement and an Application to the converability problem for Petri Nets
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk, we present an abstract fixpoint checking algorithm with
automatic refinement by backward completion in Moore closed abstract
domains. We study the properties of our algorithm and prove it to be
more precise than the counterexample guided abstract refinement
algorithm (CEGAR). Contrary to several works in the literature, our
algorithm does not require the abstract domains to be partitions of
the state space. We also show that our automatic refinement technique
is compatible with so-called acceleration techniques.
Then, we show how to develop, from this general algorithm, an abstract interpretation
based analysis that reduces the dimensionality of state spaces that are
explored during verification of Petri nets. The dimensionality is reduced
by trying to gather places that may not be important for the property to
establish. If the abstraction that is obtained is too coarse, an automatic
refinement is performed and a more precise abstraction is obtained. The
refinement is computed by taking into account information about the
inconclusive analysis. The process is iterated until the property is proved
to be true or false.
 Plus d'infos  


2008-05-22On decision problems for Probabilistic Büchi Automata
11:00-12:15
Salle 178, LaBRI, Premier étage
Probabilistic Büchi automata (PBA) are finite-state acceptors for infinite words where all choices are resolved by fixed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. In this work we describe a complementation operator for PBA and a discuss on several algorithmic problems for PBA. All interesting problems, such as checking emptiness or equivalence for PBA or checking whether a finite transition system satisfies a PBA-specification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partially-observable Markov decision processes (POMDP) and $omega$-regular winning objectives. Furthermore, we study an alternative semantics for PBA where it is required that almost all runs for an accepted word are accepting, which turns out to be less powerful, but has a decidable emptiness problem.

This is a joint work with Christel Baier and Marcus Groesser.
 Plus d'infos  


2008-04-17Test de systèmes dynamiques à partir de spécifications modales
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Parmi d'autres techniques de vérification et de validation, le
test est une méthode très largement utilisée pour assurer la qualité des
systèmes informatiques. Lorsque l'implantation du système n'est pas
connue, celui-ci peut être testé par rapport à une spécification formelle
ou informelle. Utiliser une spécification formelle comme référence de
correction du système permet de formaliser le processus de test et ainsi
de faciliter son automatisation. On distingue classiquement deux approches
du test à partir de spécifications formelles : les spécifications logiques
sont utilisées pour tester les comportements fonctionnels d'un système,
tandis que la dynamique est testée à l'aide de modèles à base d'états tels
que les systèmes de transitions. On montrera dans cet exposé de quelle
façon l'approche du test à partir de spécifications logiques, lorsqu'on
considère des spécifications exprimées en logique modale, peut être
utilisée pour tester des systèmes dynamiques.
 Plus d'infos  


2008-04-10Treillis abstraits et alphabets infinis
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Cet exposé propose de voir les langages réguliers avec un alhabet fini ou infini comme un treillis. Ce treillis est utilisé, dans le cadre de l'interpréstation abstraite, pour vérifier des systèmes avec des files ou des piles non bornées.

Si les langages réguliers avec un alphabet fini sont bien connus, des problèmes de représentation et de manipulation surgissent quand l'alphabet est infini. J'introduirai la notion d'automates de treillis, qui sont semblables aux automates finis mais dont les transitions sont étiquetées par des éléments d'un treillis atomique infini.

Je détaillerai les opérations de déterminisation et de minimisation sur ce type d'automate et j'expliquerai comment on peut définir un opérateur d'élargissement. Je présenterai aussi quelques résultats expérimentaux.

En collaboration avec Bertrand Jeannet

 Plus d'infos  


2008-03-27Accelerated Data-flow Analysis
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this talk, we show how to extend the acceleration framework to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. We illustrate our approach on convex polyhedral data-flow analysis, and we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.
Joint work with Jérôme Leroux.
 Plus d'infos  


2008-03-20Accelerating Interpolant-based Model-checking
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Interpolation-based model-checking and acceleration techniques
have been widely proved successful and efficient for reachability
checking. Surprisingly, these two techniques have never been combined
to strengthen each other. Intuitively, acceleration provides under-
approximation of the reachability set by computing the exact effect
of some control-flow cycles and combining them with other
transitions. On the other hand, interpolation-based model-checking is
refining an over-approximation of the reachable states based on
spurious error-traces.
In this talk we present a technique to combine acceleration
with interpolation-based model-checking at the refinement stage.
Our method, called “interpolant acceleration”, helps to refine the
abstraction, ruling out not only a single spurious error-trace but a
possibly infinite set of error-traces obtained by any unrolling of
its cycles. Interpolant acceleration is also proved to strictly
enlarge the set of transformations that can be usually handled by
acceleration techniques.
 Plus d'infos  


2008-03-13Probabilities in Timed Automata
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk I will present a probabilistic semantics for timed automata, that allows to measure the likelihood of properties in a timed systems. I will then describe an abstraction that can be used to verify almost-surely LTL properties, and I will present limits of the approach. I will then turn to quantitative aspects, and present an approximation scheme that can be used to compute the probabilities of LTL properties in a timed automaton.
This is based on joint works with Christel Baier, Nathalie Bertrand, Thomas Brihaye, Nicolas Markey and Marcus Groesser.
 Plus d'infos  


2008-03-06On the Relationship between Interval Analysis and Mean Payoff Games
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In a paper at ESOP 2007, we have presented an algorithm
for precise interval analysis based on strategy iteration.
While practically observed run-times are quite decent,
precise upper and lower complexity bounds have been unknown.
In this talk, we clarify the relationship of precise interval
analysis to mean-payoff games. In particular, we show that
mean-payoff games are polynomially equivalent to a class of
total-payoff games which in turn are equivalent to simple
integer equations. Since the latter form a sub-class of interval
equations, this means that proving precise interval analysis to
be polynomial is at least as hard as proving mean-payoff games
to be polynomial - which would solve a long-standing open problem
in theoretical computer science.

This work is an extension of joint work with Thomas Gawlitza
and based on late night discussions with Marcin Jurdzinski and
Uri Zwick at Dagstuhl.
 Plus d'infos  


2008-02-14Jeux avec observation partielle
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Dans un jeu avec observation partielle,
les joueurs prennent leurs décisions sans connaître l'état exact du système,
ils n'ont accès qu'à des signaux émis lors des changements d'état.

Le calcul des valeurs et des stratégies optimales de ces jeux
se révèle beaucoup plus ardu que dans le cas des jeux avec information parfaite:
au cours de cet exposé, nous présenterons plusieurs résultat
d'indécidabilité et de calculabilité, certains classiques, d'autres
récents ou inédits.
 Plus d'infos  


2008-02-07path invariants
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The success of software verification depends on the ability to find a
suitable abstraction of a program automatically. We propose a method
for automated abstraction refinement which overcomes some limitations
of current predicate discovery schemes. In current schemes, the cause
of a false alarm is identified as an infeasible error path, and the
abstraction is refined in order to remove that path. By contrast, we
view the cause of a false alarm ---the spurious
counterexample--- as a full-fledged program, namely, a fragment of
the original program whose control-flow graph may contain loops and
represent unbounded computations. There are two advantages to using
such path programs as counterexamples for abstraction
refinement. First, we can bring the whole machinery of program
analysis to bear on path programs, which are typically small compared
to the original program. Specifically, we use constraint-based
invariant generation to automatically infer invariants of path
programs ---so-called path invariants. Second, we use path
invariants for abstraction refinement in order to remove not one
infeasibility at a time, but at once all (possibly
infinitely many) infeasible error computations that are represented by
a path program. Unlike previous predicate discovery schemes, our
method handles loops without unrolling them; it infers abstractions
that involve universal quantification and naturally incorporates
disjunctive reasoning.
 Plus d'infos  


2008-01-24A Generalization of Cobham's Theorem to Automata over Real Numbers
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Joint work with Julien Brusten.

This work studies the expressive power of finite-state automata
recognizing sets of real numbers encoded positionally.
Those automata can be used as data structures for representing the sets of
values that have to be handled during state-space exploration of systems
relying on integer and real variables, such as timed or hybrid automata.
It is known that the sets that are definable in the first-order additive
theory of real and integer variables ( R, Z, +, leq) can
all be recognized by weak deterministic Büchi automata, regardless of
the encoding base r geq 1. In this paper, we prove the reciprocal
property, i.e., that a subset of R that is recognizable by
weak deterministic automata in every base r geq 1 is necessarily
definable in ( R, Z, +, leq ). This result generalizes to real numbers
the well-known Cobham's theorem on the finite-state recognizability
of sets of integers. Our proof gives interesting insight into the
internal structure of automata recognizing sets of real numbers, which
may lead to efficient data structures for handling these sets.
 Plus d'infos  


2008-01-17CEGAR Model-Checking pour AltaRica
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Le Model Checking est une technique permettant de vérifier si une propriété est satisfaite par un système.
Il présente l'avantage de produire une trace de tout comportement indésirable (décrit par une expression logique) du système. Mais cette méthode présente l'inconvénient d'exploser en mémoire (the state explosion problem).
L'approche CEGAR (CounterExemple Guided Abstraction Refinement) permet de vérifier un système en utilisant une abstraction
finie de ce dernier. Grâce à cette approche il est possible de vérifier des gros systèmes et des systèmes infinis.
Une implémentation de la méthode CEGAR pour les modèles AltaRica à été rélisée dans Mec V, afin de comparer cette approche par
rapport aux méthodes de vérifications exhaustives classiques.
 Plus d'infos  


2007-12-13V and V dans le cadre des systèmes certifiables
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Les méthodes formelles ont été mises en oeuvre avec succés dans le cadre de la
réalisation de système complexe ayant un impact sur la vie des personnes. De
tel systèmes sont dit "critique" et "sûr de fonctionnement". Pour chaque
domaine (ferroviaire, nucléaire, aéronautique, ...), il existe des référentiels
définissant les processus a mettre en oeuvre. Dans certain cas, il existe
parmis ces processus des activités obligatoires liées à la certification du
système.



Dans le cadre de cette présentation, nous rappelerons les exigences associées
aux systèmes certifiables. Nous ferons le point de ce qui a été fait et nous
montrerons les contraintes qui restent a prendre en compte et les évolutions en
cours.



Mot-clés : méthode formelle, SAET-METEOR, Système certifiable, système critique,
UML, ...
 Plus d'infos  


2007-11-29_HMSC Causaux_
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Les formalismes permettant de décrire l'interaction entre plusieurs entités distribuées et concurrentes ne manquent pas : automates asynchrones, automates communicants, réseaux de Petri, HMSC ... Ces formalismes sont tous très expressifs, et par conséquence il est souvent impossible de vérifier certaines propriétés basiques sur ces modèles. Ainsi, en général, on essaye de limiter la puissance d'expression de ces formalismes (en ajoutant, par exemple, des contraintes syntaxiques ou des bornes sur les canaux de communication) afin de rendre certains problèmes décidables.

Dans cet exposé nous introduisons une extension des HMSC appelée HMSC causaux, qui ajoute aux HMSC classiques la possibilité de commuter sur chaque processus certains évènements. Cette extension permet de modéliser des langages de MSC non finiment engendrés et non existentiellement bornés. Nous introduisons ensuite deux sous-classes syntaxiques de cette extension, les HMSC causaux réguliers et les HMSC causaux globalement-coopératifs, qui étendent strictement les classes du même nom pour les HMSC. Nous montrons que pour la première de ces classes, la régularité du langage des entrelacement est assurée, et pour la seconde l'inclusion et la vacuité de l'intersection est décidable.
 Plus d'infos  


2007-10-25Des Fruits Aléatoires sur l'Arbre de Zielonka
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Les jeux stochastiques constituent un modèle naturel
pour la synthèse de contrôleurs en milieux ouvert,
lorsque certaines actions peuvent être considérées
comme aléatoires. Les jeux $omega$-réguliers, dont
les parties sont de longueur infinie, peuvent ainsi
représenter des systèmes réactifs qui doivent réagir
correctement à un flux continuel d'évènements. Une
ressource critique pour ce genre d'applications est la
mémoire utilisée lors de l'implémentation effective du
contrôleur. Pour chaque condition de Muller, on peut
déduire de l'"arbre de Zielonka" la quantité de
mémoire nécessaire et suffisante pour définir des
stratégies gagnantes.

Dans cet exposé, je montrerai comment l'utilisation de
stratégies randomisées permet de gagner "presque
sûrement" à moindre coût dans chaque arène. Dans ce
contexte également, c'est à partir de l'étude de
l'"arbre de Zielonka" que l'on définit une meilleure
borne supérieure. De plus, pour chaque condition, il
existe certaines arènes (de taille exponentielle) pour
lesquelles des stratégies utilisant moins de mémoire
sont presque sûrement perdantes.
 Plus d'infos  


2007-10-11The quest for quantifiable quality
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
_Model checking_ is one of the main strategies to guarantee correctness
of system design. In the era of modern, power-aware, wireless and
distributed systems, correctness guarantees for such systems must become _quantifiable_. Instead of guaranteeing that a system is performing the
expected tasks, we are ultimately interested in guaranteeing that the
system performs its task within a given _time_ bound and with (energy)
_costs_ within a given limit. Or better: that the _probability_ thereof
is above a given threshold. In this talk I paint the landscape of
behavioural models for probability, time, and cost, and discuss
foundational and practical aspects of model checking such systems.
A more detailled look into our own work on continuous-time,
concurrent Markov models concludes the presentation.
 Plus d'infos  


2007-09-27A lower bound on web-services composition
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this talk a web service is modeled as a finite state machine. A composition
problem for web services is to decide if a given web service can be
constructed from a given set of web services; where the construction
is understood as a simulation of the specification by a fully asynchronous
product of the given services. We present an EXPTIME-lower bound for this problem,
thus matching the known upper bound. Our result
also applies to richer models of web services, such as the Roman
model.
 Plus d'infos  


2007-06-28A probabilistic semantic for timed automata
11:00-12:15
Salle 178, LaBRI, Rez-de-chaussée
Like most models used in model-checking, timed automata are an ideal mathematical model to represent systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely events. Following ideas of Varacca and Völzer in their LICS'06 paper, we aim at defining a notion of ``fair'' correctness for timed systems. For this purpose, we introduce a probabilistic semantics for timed automata, which ignores unlikely events, and naturally raises a notion of almost-sure satisfaction of properties in timed systems. We prove that the almost-sure satisfaction has a corresponding topological interpretation in terms of largeness of the set of paths satisfying the property. Moreover, we show PSPACE-Completeness for the LTL model-checking problem over finite computations.

Il s'agit d'un travail en collaboration avec Christel Baier, Nathalie Bertrand, Patricia Bouyer et Marcus Größer

 Plus d'infos  


2007-06-26Logiques pour la Spécification et Vérification
11:00-12:15
Salle 267, LaBRI
Dans cet exposé, je vais reprendre la présentation de ma soutenance d'habilitation centrée sur les
logiques pour la spécification et vérification. Ce sera l'occasion de rappeler la place des formalismes
logiques en informatique avec un éclairage particulier pour la vérification formelle et l'interrogation de
données. Parmi les sujets abordés plus en détail, on peut trouver les logiques temporelles avec mécanisme
de mémoire et les contraintes de régularité dans les graphes.

Plus de détails sont disponibles sur www.lsv.ens-cachan.fr/~demri/soutenance.php

 Plus d'infos  


2007-06-21Accélération de l'algorithme Cegar
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Le semi-algorithme de model-checking Cegar (Counter-example guided
abstraction refinement) connait un très vif succès au sein de la
communauté de la vérification. Il a permis de vérifier des systèmes de
taille conséquente et réaliste. Cependant, inhérent à sa nature de
semi-algorithme, il existe encore de nombreux cas, parfois triviaux,
dans lequel il se comporte mal, voir échoue.
Dans cette exposé, on commencera par redéfinir Cegar et expliquer
son fonctionnement. On mettra en suite en avant quelques exemples de
systèmes (très simples) sur lesquels l'algorithme se comporte de fa-
çon inappropriée. On proposera ensuite quelques solutions envisagées
pour améliorer le comportement dans l'algorithme, au moyen de techni-
ques d'accélération et d'interpolation.


 Plus d'infos  


2007-06-07Minimizing variants of visibly pushdown automata
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The minimization problem for visibly pushdown automata (VPA) is
studied. Two subclasses of VPA are introduced: call driven automata,
and block automata. For the first class, minimization results are
presented unifying and generalizing those present in the
literature. A drawback of this class, and all the other classes
known till now, is that it is exponentially less succinct than
VPA. The second class, block automata, is introduced to address this
problem. These automata are as succinct as VPA. A minimization
procedure for them is presented that requires one additional
parameter to be fixed. An example of an exponential gain in
succinctness is presented.
 Plus d'infos  


2007-05-31Don't Care Words with an Application to the Automata-based Approach for Real Addition
11:00-11:15
Salle 076, LaBRI, Rez-de-chaussée
As already pointed out by Büchi, automata can be used to decide
certain first-order theories of linear arithmetic, like the
first-order theory over the reals with addition and the ordering.
Reals are represented as infinite words, and the automata are
recursively constructed from the formulas. This automata-based
approach for representing and manipulating sets of reals has also
applications in infinite-state model checking. However, analogous to
BDDs to represent finite sets, the sizes of the automata are an
obstacle in the automata-based set representation.

In this talk, I will show how so-called "don't cares sets" for BDDs
can be generalized to languages as a means to reduce the automata
sizes and how "don't care words" can be used to build a more efficient
automata-based decision procedure for real addition. A general result
about don't care words is that the minimal weak deterministic B"uchi
automaton with respect to a given don't care set with certain
restrictions is uniquely determined and can be constructed
efficiently. Our implementation LIRA uses don't care words and
outperforms other state-of-the-art tools.
 Plus d'infos  


2007-04-26Hybrid Acceleration
11:00-12:30
Salle 076, LaBRI, Rez-de-chaussée
Linear hybrid automata are convenient for modeling systems with both discrete and continuous features, and for checking that requirements are met by the model. However, since model-checking is undecidable for linear hybrid automata, existing verification techniques choose to over approximate state-space computation in order to guarantee its termination. We present an acceleration technique that only helps termination without guarantee, but preserves exactness of the computed state-space. It is based on the ability to compute the transitive closure of loops in the model. This appears to yield termination of state-space computation on several examples (but of course, not always). Our acceleration technique for loops is able to handle so-called "periodic loops". However, many loops are not periodic, hence our technique has been extended with reduction rules that transforms some non-periodic loops into periodic ones. In particular, we show a reduction rule for timed automata (a decidable subclass of linear hybrid automata) that transforms any timed loop into a periodic one. Since timed automata can be flattened (Comon and Jurski), these entails that their state-space is effectively computable using our approach.
 Plus d'infos  


2007-04-05Décidabilité et contrôle de logiques temps-réel
11:00-12:15
salle 076, LaBRI, rez-de-chaussée
La logique temporelle MTL (Metric Temporal Logic) est une extension de LTL avec des contraintes quantitatives : elle permet par exemple d'exprimer qu'un événement se produira dans moins de 5 unités de temps. MTL a longtemps été supposée indécidable; ce n'est que récemment que Ouaknine et Worrel ont montré que la décidabilité de MTL dépend en fait de la sémantique considérée ("pointwise" ou "interval-based"). Nous revisiterons les résultats d'indécidabilité de MTL et étudierons la synthèse de contrôleur pour des spécifications MTL.
 Plus d'infos  


2007-03-22Vérification des Lossy Channel Systems probabilistes et non-déterministes.
11:00-12:15
salle 076, LaBRI, rez-de-chaussée
Dans les années 90, le modèle de Lossy Channel System (LCS) a été
introduit pour représenter des protocoles de communication par file
d'attentes imparfaites. Ce modèle a permis de vérifier des propriétés
de sureté pour des protocoles de communication asynchrone concus pour
pallier les pertes de messages. Néanmoins, il était trop pessimiste
concernant les questions de vivacité, car il introduisait des
comportements marginaux très peu probables (tels que l'exécution où
tous les messages sont systématiquement perdus).


Nous avons défini un modèle combinant probabilités et non-déterminisme
pour les LCS, dénoté NPLCS. Ce modèle permet de représenter les pertes
de messages comme des événements aléatoires, et les lectures ou
écritures dans les canaux par des choix non-déterministes. Nous avons
alors considéré le problème de la vérification qualitative, dont une
instance est par exemple : " existe-t-il un comportement
non-déterministe (appelé adversaire) pour lequel la probabilité de
vérifier une formule est positive ?". On montre que la vérification
qualitative est indécidable pour les NPLCS. Néanmoins, lorsqu'on
considère la classe raisonnable des adversaires à mémoire finie, la
vérification qualitative est décidable. Nous exposerons ces résultats
(indécidabilité et décidabilité), en détaillant en particulier les
ingrédients qui fournissent la décidabilité, à savoir : (1)
l'existence d'un attracteur fini, et (2) un théorème de convergence du
calcul itératif de certains points fixes.
 Plus d'infos  


2007-03-15Sociable Interfaces: Theory, Implementation, and Future
11:00-12:30
Salle 076, LaBRI, Rez-de-chaussée
Open systems are systems whose behavior is jointly determined by their internal structure, and by the inputs that they receive from their environment. A component of a larger system is, therefore, an open system, as its behavior depends on the inputs it receives from the other system components.

Since the last decades, various models have been introduce to model open systems. Among them one finds game-based models that represent the interaction between the behavior originating within a component, and the behavior originating from the component's environment as a game.

In this talk, I will first recall the basic advantages of using a game-based model for the specification, verification, composition, and refinement of open systems.

I will then introduce sociable interfaces, a recent concrete asynchronous game-based model where components have rich communication primitives that facilitate the modeling of software and distributed systems as well as global resources.

The Sociable Interfaces model has been implemented in a tool called TICC. I will describe the main features of TICC, and explain the difficulties of moving from the theoretical description of the model to its implementation.

Finally, I will discuss the possibility of adding time to the model.

Joint work with Luca de Alfaro and Marco Faella.
 Plus d'infos  


2007-03-08Dépliages temporisés de réseaux d'automates temporisés
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Alors que les méthodes d'ordres partiels ont prouvé leur efficacité pour l'analyse de systèmes à événements discrets, leur application aux systèmes temporisés reste un sujet de recherche délicat . Nous proposons ici une méthode de vérification pour les réseaux d'automates temporisés avec invariants. Fondée sur la technique du dépliage, notre méthode produit un processus branchant, exprimé comme un réseau de Petri acyclique étendu avec des arcs de lecture. Ces arcs nous permettent d'obtenir une relation de concurrence entre les événements la plus large possible. D'autre part, nous attachons à chaque événement, en plus d'un marquage, une zone qui représente les contraintes temporisées associées à cet événement. Nous expliquons alors comment se limiter à une partie bornée de ces zones, correspondant au marquage de cet événement. Nous calculons enfin un préfixe fini et complet de ce dépliage, permettant de résoudre le problème de l'accessibilité.
 Plus d'infos  


2007-02-15Flat Parametric Counter Automata
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this paper we study parametric flat counter automata and their relation with various
decidable fragments of integer arithmetic. We establish a hierarchy of flat counter automata,
by restricting the number of parameters, the number of loops and the form of the transition
relations. For each class in the hierarchy, we found a matching subtheory of integers, in the
sense that, for each automaton in the class, the reachability (emptiness) problem can be
expressed as the satisfiability of a formula in the language of a given theory, and viceversa.
Using the same arithmetic theories allowed us to also establish the relation of flat counter
automata with previous work on 2-way reversal bounded counter machines. Last, we report on an
effective procedure to answer the question whether a given 1-parametric linear Diophantine system
has a solution.
 Plus d'infos  


2007-02-01Verification of (One-clock) Priced Timed Automata
11:00-11:30
Salle 076, LaBRI, Rez-de-chaussée
Priced timed (game) automata are timed (game) automata
extended with cost functions [ATP01,BFH+01]. The cost
functions are just "observers", and cannot act upon the
behavior of the automaton.

We consider two classical problems:
- computation of optimal cost and optimal winning strategies
in PTGAs,
- quantitative (w.r.t. costs) CTL model-checking in PTAs.
We show that they are undecidable in general for priced timed
automata, and prove that they are decidable when restricting
to one-clock PTAs.
 Plus d'infos  


2007-01-25Certification de la résistance des réseaux de programmes synchrones aux erreurs matérielles
11:00-12:30
Salle 076, LaBRI, Rez-de-chaussée
Nous définissons un modèle de l'exécution des programmes
synchrones communicants tenant compte des imperfections matérielles
(désynchronisation des horloges, retards dans la transmission des
données). Ces imperfections étant inévitables, les programmes
incluent des techniques de robustesse qui permettent d'implémenter
leur spécification malgré ces défauts. Cependant, ces techniques
sont complexes, modifient fortement les programmes, et sont souvent
ajoutées "à la main". Nous proposons donc une analyse statique
(i.e. sur le code source et pas à l'exécution) et automatique,
basée sur la théorie de l'interprétation abstraite, permettant
de prouver formellement certaines de ces spécifications.
 Plus d'infos  


2007-01-18Graf and Saïdi97'algorithm : Construction of abstract state graph Revisited
11:00-12:30
Salle 076, LaBRI, Rez-de-chaussée
Let given a system S and a property phi, the problem of model-checking is the verification of the formula S | = phi.
That requires
- the construction of a model (STE) of execution of the system
- a temporal logic
- evaluation of the satisfaction of the property on the model.
This method does not apply to the system having a infite number of states.
It has nevertheless the advantage of being entirely automatizable.
The abstraction is a technique of checking which consists in building a finite
model for a system having an infinite number of states. That makes it possible to verify the properties wished on the abstract model by model-checking.
The construction of an abstract model consists in defining an
abstract domain and building a system of transition on this domain.
Graf and Saïdi have proposed an automatic algorithm of connstruction of
abstraction which requires many obligation of proof.
The goal of the talk is to present a simplification of this construction.
 Plus d'infos  


2007-01-11Combining Widening and Acceleration in Linear Relation Analysis
14:00-15:30
Salle 178, LaBRI, Premier étage
Linear Relation Analysis is one of the first, but still one of
the most powerful, abstract interpretations working in an infinite
lattice. As such, it makes use of a widening operator to enforce the
convergence of fixpoint computations. While the approximation due to
widening can be arbitrarily refined by delaying the application of
widening, the analysis quickly becomes too expensive with the increase
of delay. Previous attempts at improving the precision of widening are
not completely satisfactory, since none of them is guaranteed to
improve the precision of the result, and they can nevertheless
increase the cost of the analysis. In this talk, we investigate an
improvement of Linear Relation Analysis consisting in computing, when
possible, the exact (abstract) effect of a loop. This technique is
fully compatible with the use of widening, and whenever it applies, it
improves both the precision and the performance of the analysis.
 Plus d'infos  


2006-12-14 L'analyseur statique Astrée
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Astrée est un analyseur statique, basé sur l'interprétation abstraite, qui vérifie l'absence d'erreurs à l'exécution pour un sous-ensemble du langage C. Astrée est sûr par construction: un sur-ensemble des comportements est calculé. Astrée est spécialisé dans l'analyse de codes synchrones réactifs de contrôle commande où il est précis et rapide (preuve d'absence de débordements de tableaux et d'erreurs arithmétiques sur les entiers et les flottants pour une application avionique critique de 400 000 lignes en 14h). Dans cet exposé, nous présenterons la méthodologie de conception d'analyseur spécialisé par raffinement des abstractions. Nous expliquerons le fonctionnement et la structure modulaire d'Astrée et donnerons quelques exemples précis de domaines abstraits qu'il nous a fallu concevoir ou adapter, tout en motivant les choix sémantiques et algorithmiques.
 Plus d'infos  


2006-12-07Logics and automata with infinite alphabets
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In this survey we give an overview of recent
results on logics and automata with infinite
alphabets. In this setting, we reason about
data word and data tree languages, where we allow
(in addition to usual regular operations) equality
tests on the infinite alphabet component.

At the beginning of the 90's, research on this
topic focused on automata models à la Kaminski/Francez,
and Neven/Schwentick/Vianu. However, the results obtained were
mostly about undecidability and noncomparability
of different automata models and of logics.

Motivated by applications in XML data reasoning
and in verification, recent work focused on
exhibiting restricted decidable logics with data. Some examples
are 1) two-variable FO logics with order and
successor over finite and infinite data words, 2) two-variable
FO logics with successor over data tree languages
(Bojanczyk et al.) and 3) fragments of LTL with freeze operator
(Demri/Lazic).
 Plus d'infos  


2006-11-30Unfolding Concurrent Well-Structured Transition Systems
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Joint work with Frédéric Herbreteau and Grégoire Sutre.
-------------------------------------------------------

In this work, our main objective is to combine partial-order methods with
verification techniques for infinite-state systems in order to obtain efficient
verification algorithms for concurrent infinite-state systems. This paper
presents a general framework for partial-order modeling and verification of
well-structured transition systems.

Firstly, McMillan has proposed a technique in the verification of
systems modelled with finite-state Petri nets [McM95]. This technique is based on the
concept of net unfoldings and a well-known partial-order semantics of Petri
nets. It construct only a finite complete prefix of the unfolding which
contains full information about the reachable states. The unfolding technique
has been later developed for other model of concurrency, e.g. Synchronous
Products of Transition Systems [ER99], High-Level Petri Nets [KK03], Extended
Finite State Machines [LI05]; and applied to other verification problems,
e.g. checking relevant properties of speed independent circuits [KKTV95], simple
branching time logic [Esp94].

Although the finite prefix obtained by unfolding technique avoids the
interleaving explosion, it is sometimes much larger than necessary. Several
works trying to resolve this problem can be classified into two types. The
first one is to give a more adequate criteria in truncating the unfolding, e.g.
based on a total order of trace [ER99], based on the symmetry of Petri Nets w.r.t
some notions [CGP01]; and the second one is to avoiding the unuseful
multiplication of a same labeled event when unfolding non-safe Petri nets
[KKKV05].

In our work, we model concurrent systems as synchronized
products of (heterogeneous) components, where the semantics of components is
given in terms of event structures. This allows us to benefit from the
intrinsic concurrency in each component. We propose event structures for
counters and queues, and we present an on-the-fly compositional unfolding
algorithm that computes event structures for synchronized products. For the
particular case of well-structured components, we give property-preserving
truncation criteria [FS01] on event structures in order to obtain effective decision
algorithms for the boundedness, termination and quasi-liveness problems.
Moreover, our technique for avoiding redundancy in the unfolding can also
resolving the irrelevant multiplication problem stated in [KKKV05].

We have implemented a tool, called ESU, for demonstrating the benefits of our
approach.

[CGP01] Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding
of products of symmetrical petri nets. In ICATPN, pages
121-143, 2001.

[ER99] J. Esparza and S. Römer. An unfolding algorithm for synchronous
products of transition systems. In International Conference on Con-
currency Theory, volume 1664 of Lecture Notes in Computer Sci-
ence, pages 2-20, 1999.

[Esp94] Javier Esparza. Model checking using net unfoldings. Sci. Comput.
Program., 23(2-3):151-195, 1994.

[FS01]Alain Finkel, Ph. Schnoebelen: Well-structured transition systems everywhere!
Theor. Comput. Sci. 256(1-2): 63-92 (2001)

[KK03] Victor Khomenko and Maciej Koutny. Branching processes of highlevel
petri nets. In TACAS, pages 458-472, 2003.

[KKKV05] Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter
Vogler. Merged processes - a new condensed representation of petri
net behaviour. In CONCUR, pages 338-352, 2005.

[KKTV94] Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor
Varshavsky. Analysis and identification of speed-independent
circuits on an event model. Formal Methods in System Design,
4(1):33-75, 1994.

[LI05] Yu Lei and S. Purushothaman Iyer. An approach to unfolding asynchronous
communication protocols. In FM, pages 334-349, 2005.

[McM95]Kenneth L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995).
 Plus d'infos  


2006-11-16Implementations distribuees du controle superviseur a la Ramadge et Wonham par synthese de reseaux de Petri
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
La theorie du controle superviseur de Ramadge-Wonham
permet, pour divers types de problemes de controle
poses en termes de langages reguliers, de decider si
ces problemes sont faisables, et de construire alors
des automates finis realisant le controle. Diverses
extensions de la theorie portent sur le controle des
systemes decentralises mais le controle des systemes
asynchrones et distribues reste un probleme ouvert.

Nous montrons comment integrer la synthese de reseaux
de Petri et la theorie de Ramadge-Wonham afin d'avoir
une reponse partielle a ce probleme.
 Plus d'infos  


2006-11-09The Cost of Punctuality
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
In an influential paper titled "The Benefits of Relaxing Punctuality" (JACM 1996), Alur, Feder, & Henzinger introduced the logic Metric Interval Temporal Logic (MITL), which is a fragment of the real-time logic Metric Temporal Logic (MTL) in which the time constraints on operators are not allowed to be punctual, i.e., singleton sets. They produced an intricate proof (11 pages) that MITL model checking and satisfiability are decidable -- in fact EXPSPACE-COMPLETE. This has led to considerable further work; in the last year alone, both Hirshfeld & Rabinovich, and Maler, Nickovic, & Pnueli, published new and simpler decision procedures for MITL.

An obvious question to ask is, what happens if punctuality is allowed? Until recently, it was widely believed that the faintest presence of punctuality in any linear-time timed temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no decidable punctual fragment of MTL was known to have even primitive recursive complexity (with certain fragments having provably non-primitive recursive complexity!).

Very recently, in joint work with Patricia Bouyer, Nicolas Markey, and James Worrell, we have been able to precisely pinpoint the complexity of the main decidable punctual fragments of MTL. Our complexity bounds involve a connection between MTL formulas and reversal-bounded Turing machines. We will present an overview of these results and how they relate to standard (untimed) verification.
 Plus d'infos  


2006-10-19Réseaux de Petri à Chronométre - temps dense ou temps discret ?
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
L'utilisation croissante (dans lÆindustrie automobile mais aussi aéronautique) de réseaux informatiques embarqués implique de vérifier a priori leur bon fonctionnement. Il convient ainsi de développer des formalismes permettant d'écrire et de valider les interactions entre les activités des processeurs et les réseaux de communication. Les réseaux de Petri temporels sont un de ces formalismes. Ils permettent de modéliser la durée de différentes actions sous la forme d'un intervalle de temps. Ils peuvent par ailleurs être enrichis afin de représenter des tâches susceptibles d'être suspendues puis relancées.

Deux approches peuvent alors être considérées. La première consiste à considérer le temps comme une grandeur continue (c'est-à-dire que le système peut changer d'état à n'importe quel moment), la seconde à l'envisager comme une grandeur discrète (la progression du temps est assurée par l'occurrence de tics d'horloge et le système ne peut alors évoluer qu'à des instants précis). Notre objectif durant cette thèse est de comparer ces deux approches : nous souhaitons dégager les spécificités de chacune et déterminer les différentes propriétés qu'elles permettent de vérifier. Ces recherches théoriques s'accompagnent d'un volet pratique. En effet, nous implantons nos résultats dans Roméo, un logiciel d'analyse de systèmes embarqués, et assurons ainsi leur valorisation auprès du tissu industriel.
 Plus d'infos  


2006-10-12On Zielonka's Theorem and its Application to Verification
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
The well-known algorithm of Zielonka describes how to transform automatically a sequential automaton into a deterministic (distributed) asynchronous trace automaton. A straigthforward application is synthesis/implementation of distributed system. It can also be applied to obtain deadlock-free systems. We show here another application in terms of Dynamic and Distributed Verification. Unfortunately, Zielonka's algorithm gives an asynchronous automaton that is doubly exponential in the number of processes (and simply exponential in the size of the automaton), which implies that the verification takes an exponential time to be performed. We show how we improve the generic Zielonka's algorithm, which in particular yields a polynomial time complexity for the distributed verification. Non deterministic Implementation will also be considered.
 Plus d'infos  


2006-10-05Réunion de rentrée du thème Modélisation Vérification
11:00-12:15
Salle 076, LaBRI, Rez-de-chaussée
Igor Walukiewicz animera la réunion.
 Plus d'infos  




Liste des événements répétitifs du groupe Modélisation et Verification




Retour
Retour à l'index