Publications du projet SOAPDC

A netchart is basically a Petri net whose places are located at some process and whose transitions are labeled by message sequence charts (MSCs). Two recent papers showed independently that any globally-cooperative high-level MSC corresponds to the behaviors of some communicating finite-state machine - or equivalently a netchart. These difficult results rely either on ThomasÇ graph acceptors or ZielonkaÇs construction of asynchronous automata. In this paper we give a direct and self-contained synthesis of netcharts from globally-cooperative high-level MSCs by means of a simpler unfolding procedure.

Zielonka's theorem shows that each regular set of Mazurkiewicz traces can be implemented as a system of synchronized processes provided with some distributed control structure called an asynchronous automaton. This paper gives a new algorithm for the synthesis of a non-deterministic asynchronous automaton from a regular Mazurkiewicz trace language. Our approach is based on an unfolding procedure that improves the complexity of Zielonka's and Pighizzini's techniques: Our construction is polynomial in terms of the number of states but still double-exponential in the size of the alphabet. As opposed to Métivier's work, our algorithm does not restrict to acyclic dependence alphabets.

Recently, a new approach to the symbolic model checking of timed automata based on a partial order semantics was introduced, which relies on event zones that use vectors of event occurrences instead of clock zones that use vectors of clock values grouped in polyhedral clock constraints. A key property of that approach is that the exchange of independent actions in a sequence preserves the event zones, whereas the clock zone may change. As a result, symbolic state exploration with event zones rather than clock zones can result in significant reductions in the number of symbolic states explored. Moreover, the formal development allowed for the class of timed automata proposed by Alur-Dill, except for state invariants. In this work, we show how to extend the event zone approach to net- works of automata with local state invariants, an important feature for modeling complex timed systems. We give a formalization of local in- variants that avoids the burden of formal specialization to a particular kind of model: Rather than formalizing local states, we attach to each transition an urgency constraint that relates to the global state invariant like a local invariant, thus allowing straight a forward application of the current work to networks of timed automata. Surprisingly, under highly reasonable assumptions, the independence relation as previously formalised without invariants, is preserved. We give a Èrelaxed seman- ticsÉ of runs in the presence of these local invariants and show that it is consistent with non-relaxed semantics. We have integrated the extension into a prototype tool with event zones and can report very promissing experimental results.

Local First Search (LFS) is a partial order technique for reducing the number of states to be explored when trying to decide reachability of a local (component) property in a parallel system; it is based on an analysis of the structure of the partial orders of executions in such systems. Intuitively, LFS is based on a criterion that allows to guide the search for such local properties by limiting the Èconcurrent progressÉ of components. In this paper, we elaborate the analysis of the partial orders in ques- tion and obtain related but significantly stronger criteria for reductions, show their relation to the previously established criterion, and discuss the algorithmics of the proposed improvement. Our contribution is both fundamental in providing better insights into LFS and practical in pro- viding an improvement of high potential.

There are many cases where we want to verify a system that does not have a usable formal model: the model may be missing, out of date, or simply too big to be used. A possible method is to analyze the system while learning the model (black box checking). However, learning may be an expensive task, thus it needs to be guided, e.g., using the checked property or an inaccurate model (adaptive model checking). In this paper, we consider the case where some of the system components are completely specified (white boxes), while others are unknown (black boxes), giving rise to a grey box system.We provide algorithms and lower bounds, as well as experimental results for this model.

We present the implementation of the trace theory in a new model checking tool framework, POEM, that has a strong emphasis on Partial Order Methods. A tree structure is used to store trace systems, which allows sharing common prefixes among traces and therefore, re- duces memory cost. This structure is easy to extend to incorporate ad- ditional features. Two applications are shown in the paper: An extended structure to support an adequate order for Local First Search, and an acceleration of event zone based state space search for timed automata.

Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Examples of such properties are serializability of a database or snapshots. Recently, a modest extension for LTL by an operator that expresses snapshots has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot (also called a slice or a cut) was passed, perhaps not in the observed (interleaved) execution sequence, but possibly in a (trace) equivalent one. A model checking algorithm was suggested for a subset of this logic, with PSPACE complexity in the size of the system and the checked formula. For the whole logic, a solution that is in EXSPACE in the size of the system (PSPACE in the number of its global states) was given. In this paper, we provide a model checking algorithm in PSPACE in the size of a system of communicating sequential processes when restricting snapshots to boolean combinations of local properties of each process. Concerning size of the formula, it is PSPACE for the case of snapshot properties expressed in DNF, and EXPSPACE where a translation to DNF is necessary.

Proof-nets are special graphs (proof-structures) representing de-sequentialised proofs of the linear logic (LL) sequent calculus. Each proof-net stands for a class of sequent proofs which are equivalent modulo irrelevant permutations of logical rules. In our work we present an interactive characterisation of those cut-free proof-structures coming from proofs of the multiplicative-additive fragment of linear logic (MALL). This work is intended to extend to MALL proof-nets an original proposal by Girard for an interactive correction criterion for proof-nets of the multiplicative fragment of linear logic (MLL). Its natural consequence we will be the study of the question of “modularity” for additive proof-nets.

For L a finite lattice, let C(L) denote the set of pairs γ= (γ₀,γ₁) such that γ₀ is a lower cover of γ₁ and order it as follows: γ<=δ iff γ₀ <= δ₀, γ₁ <=δ₁, but γ₁ <=δ₀ does not hold. Let C(L,γ) denote the connected component of γ in this poset. Our main result states that C(L,γ) is a semidistributive lattice if L is semidistributive, and that C(L,γ) is a bounded lattice if L is bounded. Let S_n be the permutohedron on n letters and T_n be the associahedron on n+1 letters. Explicit computations show that C(S_n,α) = S_n-1 and C(T_n,α) = T_n-1, up to isomorphism, whenever α is an atom. These results are consequences of new characterizations of finite join semidistributive and finite lower bounded lattices: (i) a finite lattice is join semidistributive if and only if the projection sending γin C(L) to γ₀ inL creates pullbacks, (ii) a finite join semidistributive lattice is lower bounded if and only if it has a strict facet labelling. Strict facet labellings, as defined here, are generalization of the tools used by Barbut et al. to prove that lattices of Coxeter groups are bounded.

We study the congruence lattices of the multinomial lattices L(v) introduced by Bennett and Birkhoff. Our main motivation is to investigate Parikh equivalence relations that model concurrent computation. We accomplish this goal by providing an explicit description of the join dependency relation between two join irreducible elements and of its reflexive transitive closure. The explicit description emphasizes several properties and makes it possible to separate the equational theories of multinomial lattices by their dimensions. In their covering of non modular varieties Jipsen and Rose define a sequence of equations SD_n(/\), for n >=0. Our main result sounds as follows: if v = (v₁,...,v_n) inNⁿ and v_i > 0 for i = 1,...,n, then the multinomial lattice L(v) satisfies SD_n-1(/\) and fails SD_n-2(/\).

We address the problem of finding nice labellings for event structures of degree 3. We develop a minimum theory by which we prove that the labelling number of an event structure of degree 3 is bounded by a linear function of the height. The main theorem we present in this paper states that event structures of degree 3 whose causality order is a tree have a nice labelling with 3 colors. Finally, we exemplify how to use this theorem to construct upper bounds for the labelling number of other event structures of degree 3.

Parity games are combinatorial representations of closed Boolean μ-terms. By adding to them draw positions, they have been organized by Arnold and one of the authors into a μ-calculus. As done by Berwanger et al. for the propositional modal μ-calculus, it is possible to classify parity games into levels of hierarchy according to the number of fixed-point variables. We ask whether this hierarchy collapses w.r.t. the standard interpretation of the games μ-calculus into the class of all complete lattices. We answer this question negatively by providing, for each n >= 1, a parity game G_n with these properties: it unravels to a μ-term built up with n fixed-point variables, it is semantically equivalent to no game with strictly less than n-2 fixed-point variables.

Given a set Γ of modal formulas of the form γ(x,p), where x occurs positively in γ, the language L_#(Γ) is obtained by adding to the language of polymodal logic K connectives #_γ, γin Γ. Each term #_γ is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x). Given such a Γ, we construct an axiom system K_#(Γ) which is sound and complete w.r.t. the concrete interpretation of the language L_#(Γ) on Kripke frames. If Γ is finite, then K_#(Γ) is a finite set of axioms and inference rules.

Entanglement is a complexity measure of directed graphs that origins in fixed point theory. This measure has shown its use in designing efficient algorithms to verify logical properties of transition systems. We are interested in the problem of deciding whether a graph has entanglement at most k. As this measure is defined by means of games, game theoretic ideas naturally lead to design polynomial algorithms that, for fixed k, decide the problem. Known characterizations of directed graphs of entanglement at most 1 lead, for k = 1, to design even faster algorithms. In this paper we present an explicit characterization of undirected graphs of entanglement at most 2. With such a characterization at hand, we devise a linear time algorithm to decide whether an undirected graph has this property.

An event structures is a mathematical model of a concurrent process. It consists of a set of local events ordered by a causality relation and separated by a conflict relation. A global state, or configuration, is an order ideal whose elements are pairwise not in conflict. Configurations, ordered by subset inclusion, form a poset whose Hasse diagram codes the state-transition graph of the process. By labelling edges, the state-transition graph can be enriched with the structure of a deterministic concurrent automaton on some alphabet. The nice labelling problem asks to minimize the cardinality of the alphabet. In this talk we shall first introduce the nice labelling problem and show how it translates to a graph coloring problem. We shall then survey on the problem and present the results that are available to us nowadays. Thus we shall The survey will also be the occasion to point out new perspectives, open problems, and research paths.

Parity games are combinatorial representations of closed Boolean μ-terms. By adding to them draw positions, they have been organized by Arnold and one of the authors into a μ-calculus. As done by Berwanger et al. for the propositional modal μ-calculus, it is possible to classify parity games into levels of hierarchy according to the number of fixed-point variables. We ask whether this hierarchy collapses w.r.t. the standard interpretation of the games μ-calculus into the class of all complete lattices. We answer this question negatively by providing, for each n >= 1, a parity game G_n with these properties: it unravels to a μ-term built up with n fixed-point variables, it is semantically equivalent to no game with strictly less than n-2 fixed-point variables.

Nous souhaitons illustrer comment la notion de structure, algébrique et d'ordre, peut être un guide fructuex dans l'étude de sujets importants de l'informatique tels que les processus concurrents et les logiques modales et temporales pour la vérification des systèmes informatiques.

Motivated by the nice labeling problem for event structures, we study the topological properties of the associated graphs. For each n >=0, we exhibit a graph G_n that cannot occur on an antichain as a subgraph of the graph of an event structure of degree n. The clique complexes of the graphs G_n are disks (n even) and spheres (n odd) in increasing dimensions. We strengthen the result for event structure of degree 3: cycles of length greater than 3 do not occur on antichains as subgraphs. This amount to saying that the clique complex of the graph of an event structure of degree 3 is acyclic.

The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as processes which communicate by two-way channels. The maps of an SP-category may also be viewed as a proof theory for a simple logic with a game theoretic intepretation. The cut-elimination procedure for this logic determines equality only up to certain permuting conversions. As the equality classes under these permuting conversions are finite, it is easy to see that equality between cut-free terms (even in the presence of the additive units) is decidable. Unfortunately, this does not yield a tractable decision algorithm as these equivalence classes can contain exponentially many terms. However, the rather special properties of these free categories - and, thus, of two-way communication - allow one to devise a tractable algorithm for equality. We show that, restricted to cut-free terms s,t : X -> A, the decision procedure runs in time polynomial on |X||A|, the product of the sizes of the domain and codomain type.