Next: Composition
Action spécifique
Méthodes formelles pour la mobilité
- Composition
- Description
- Première Reunion.
- Deuxième Reunion : ENS-Lyon, 10--11 Mars..
- Troisième Reunion: Marseille, 7 Septembre.
- Projets IST Global Computing en relation avec l'action : PROFUNDIS, MYTHS, MRG.
- Logiciels developpes par des participants a l'action :
CDUCE.
- Bilan et perspectives de l'AS présenté au GDR ALP, le 7/12/2004 à Paris.
- Rapports redigés dans le cadre de l'action :
-----------------------Mobilité et contrôle de ressources.-------------------------
*** Max-plus quasi-interpretations
Roberto M. Amadio
RR LIF 10-2002, extended abstract in Typed Lambda Calculi and
Applications, Springer LNCS 2701, 2003.
Quasi-interpretations are a tool to bound the size of the values
computed by a first-order functional program (or a term rewriting
system) and thus a mean to extract bounds on its computational
complexity. We study the synthesis of quasi-interpretations selected
in the space of polynomials over the max-plus algebra determined by
the non-negative rationals extended with -infinite and equipped with
binary operations for the maximum and the addition. We prove that in
this case the synthesis problem is NP-hard, and in NP for the
particular case of multi-linear quasi-interpretations when programs
are specified by rules of bounded size. The relevance of multi-linear
quasi-interpretations is discussed by comparison to certain syntactic
and type theoretic conditions proposed in the literature to control
time and space complexity.
*** Soft lambda-calculus: a language for polynomial time computation.
Patrick Baillot, Virgile Mogbil. 18 p., octobre 2003. Soumis pour publication.
Soft linear logic ([Lafont02]) is a subsystem of linear logic
characterizing the class PTIME. We introduce Soft
lambda-calculus as a calculus typable in the intuitionistic and
affine variant of this logic. We prove that the (untyped) terms of
this calculus are reducible in polynomial time. We then extend the
type system of Soft logic with recursive types. This allows us to
consider non-standard types for representing lists. Using these
datatypes we examine the concrete expressivity of Soft lambda-calculus
with the example of the insertion sort algorithm.
*** Type inference for polynomial time complexity via constraints
on words.
Patrick Baillot.
Prepublication LIPN Universite Paris Nord 2003-02, janvier 2003.
Light Affine Logic (LAL) is a system due to Girard and Asperti
capturing the complexity class P in a proof-theoretical approach based
on linear logic. LAL provides a typing for lambda-calculus which
guarantees that a well-typed program is executable in polynomial-time
on any input. We prove that the LAL type inference problem for
lambda-calculus is decidable (for propositional LAL). To establish
this result we reformulate the type-assignement system into an
equivalent one which makes use of subtyping and is more flexible. We
then use a reduction to a satisfiability problem for a system of
inequations on words over a binary alphabet, for which we provide a
solving algorithm.
*** Bisimulation Proof Methods for Mobile Ambients
M. Merro, F. Zappa Nardelli
Technical Report COGS 2003:1. An extended abstract appeared in
Proc. ICALP 2003.
We study the behavioural theory of Cardelli and Gordon's Mobile
Ambients. We give an lts based operational semantics, and a labelled
bisimulation based equivalence that coincides with reduction barbed
congruence. We also provide two up-to proof techniques that we use to
prove a set of algebraic laws, including the perfect firewall equation.
*** D. Teller, "Formalisms for Resource Control", proc. of Foundations of
Global Computing (FGC) 2003.
Failing to control resources in mobile, concurrent and distributed
systems may lead to important breakdowns or Denial of Service-like
attacks. In order to address this problem, we present enhanced
versions of several calculi for mobile and distributed computing,
namely NBA, Seals, Nomadic Pi and Kells. In each case, we make the
formalism resource-conscious and define a type system in order to
guarantee statically compliance with resource control
policies. Comparing the solutions we proposed for these calculi, we
try and define the necessities of resource-control in mobile and
distributed formalisms.
-----------------------Logiques spatiales-----------------------------------
*** Multitrees Automata, Presburger's Constraints and Tree Logics.
Silvano Dal Zilio, Denis Lugiez.
Research Report 08-2002, LIF, June 2002.
We describe multitree automata and a related logic on multitrees with
applications to various areas of Computer Science. Multitrees are
extensions of trees with both associative and associative-commutative
symbols that may bear an arbitrary number of sons. An originality of
our approach is that transitions of an automaton are restricted using
Presburger's constraints. The benefit of this extension is that we
generalize, all together, automata with equality and disequality
constraints as well as counting constraints. This new class of
automata appears very general as it may encompass hedge automata, a
simple yet effective model for XML schemata, feature tree automata,
automata with constraints between brothers and automata with
arithmetical constraints. Moreover, the class of recognizable
languages enjoys all the typical good properties of traditional
regular languages: closure under boolean operations and composition by
associative and associative-commutative operators, determinisation,
decidability of the test for emptiness, ...
We apply our automata to query languages for XML-like documents and to
automated inductive theorem proving based on rewriting, obtaining each
time new results. Using a classical connection between logic and
automata, we design a decidable logic for (multi)trees that can be
used as a foundation for querying XML-like document. This proposition
has the same flavour as a query language for semi-structured recently
proposed by Cardelli and Ghelli, that we appear to include. The same
tree logic is used to yield decidable cases of inductive reducibility
modulo associativity-commutativity, a key property in inductive
theorem proving based on rewriting.
*** A Logic You Can Count On. Silvano Dal Zilio, Denis Lugiez, Charles
Meyssonnier. Proc. of POPL 2004, Symposium on Principles of Programming
Languages, ACM.
We prove the decidability of the static fragment of ambient logic, with
composition adjunct and iteration, which corresponds to a kind of regular
expression language for semistructured data. The essence of this result
is a surprising connection between formulas in the ambient logic and
counting constraints on (nested) vectors of integers.
Our proof method is based on a new class of tree automata for unranked,
unordered trees, which may result in practical algorithms for deciding
the satisfiability of a formula. A benefit of our approach is to
naturally lead to an extension of the logic with recursive definitions,
which is also decidable. Finally, we identify a simple syntactic
restriction that improves the effectiveness of our algorithms on large
examples.
*** Minimality results for the spatial logics
D. Hirschkoff, E. Lozes, D. Sangiorgi,
proc. of FSTTCS 2003, LNCS, a paraitre.
A spatial logic consists of four groups of operators: standard
propositional connectives; spatial operators; a temporal modality;
calculus-specific operators. The calculus-specific operators talk
about the capabilities of the processes of the calculus, that is, the
process constructors through which a process can interact with its
environment. We prove some minimality results for spatial logics.
The main results show that in the logics for pi-calculus and
asynchronous pi-calculus the calculus-specific operators can be
eliminated. The results are presented under both the strong and the
weak interpretations of the temportal modality. Our proof techniques
are applicable to other spatial logics, so to eliminate some of -- if
not all -- the calculus-specific operators. As an example of this, we
consider the logic for the Ambient calculus, with the strong
semantics.
*** Adjunct Elimination in the Static Ambient Logic
E. Lozes,
Proc. of Express 2003.
The Ambient Logic (AL) has been proposed for expressing spatial
properties of processes of the Mobile Ambient calculus (MA).
Restricting both the calculus and the logic to their static part
yields static ambients (SA) and the static ambient logic (SAL), that
form a model for queries about semistructured data. SAL also includes
the non-standard fresh quantifier.
This work adresses the questions of expressiveness and minimality of
SAL from the point of view of adjuncts. We define the intensional
fragment of the logic (SAL_int), the logic without adjuncts, and prove
that it captures all the expressiveness of the logic.
We moreover study the question of adjuncts elimination in SAL^\forall,
where the fresh quantifier is replaced by classical universal
quantification. We conclude with a proof of the minimality of SAL_int.
*** Multitree Automata with counting and Equality Constraints. Denis Lugiez.
Proc. of FoSSaCS 2003. Lecture Notes in Computer Science, vol. 2620, p.
328 - 342, 2003
Multitree are unranked, unordered trees and occur in many Computer
Science applications like rewriting and logic, knowledge representation,
XML queries, typing for concurrent systems, cryptographic protocols....
We define constrained multitree automata which accept sets of multitrees
where the constraints are expressed in a first-order theory of multisets
with counting formulae which is very expressive and decidable. The
resulting class of multitree automata is closed under boolean
combination, has a decidable emptiness problem and we show that this
class strictly embeds all previous classes of similar devices which have
been defined for a whole variety of applications.
------------------------Données Semi-structurées----------------------------
*** CDuce: An XML-Centric General-Purpose Language.
V. Benzaken, G. Castagna, and A. Frisch.
Proceedings of the ACM International Conference on Functional Programming, 2003.
http://www.cduce.org/papers/cduce-design.ps.gz
We present the functional language CDuce, discuss some design issues,
and show its adequacy for working with XML documents. Distinctive
features of CDuce are a powerful pattern matching, first class
functions, overloaded functions, a very rich type system (arrows,
sequences, pairs, records, intersections, unions, differences), precise
type inference for patterns and error localization, and a natural
interpretation of types as sets of values. We also outline some
important implementation issues; in particular, a dispatch algorithm
that demonstrates how static type information can be used to obtain very
efficient compilation schemas.
*** Security analysis for XML transformations.
V. Benzaken, M. Burelle, and G. Castagna.
In Asian '03, LNCS, 2003. (to appear)
In this article we give a formal definition of information flows
in the context of XML transformations and, more generally, in
the presence of type dependent computations. We formalize a
sound technique to detect XML document transformations that may
leak private or confidential information. By defining security
annotations and by relating various kind of analyses to
different query scenarios, we also establish a general framework
for checking middleware-located information flows.
*** XML Schema, Tree Logic and Sheaves Automata.
Silvano Dal Zilio, Denis Lugiez.
In Proc. of RTA - Rewriting Techniques and Applications, R.
Nieuwenhuis (Ed.), Lecture Notes in Computer Science, Vol. 2706,
Springer-Verlag, June 2003. pp. 246-263. An extended version of this paper
appears as Research Report 4631, INRIA, November 2002.
We describe a new class of tree automata, and a related logic on
trees, with applications to the processing of XML documents and XML
schemas.
XML documents, and other forms of semi-structured data, may be roughly
described as edge labeled trees. Therefore it is natural to use tree
automata to reason on them and try to apply the classical connection
between automata, logic and query languages. This approach has been
followed by various researchers and has given some notable results,
especially when dealing with Document Type Definition (DTD), the
simplest standard for defining XML documents validity. But additional
work is needed to take into account XML schema, a more advanced
standard, for which regular tree automata are not satisfactory. A
major reason for this inadequacy is the presence of an
associative-commutative operator in the schema language, inherited
from the &-operator of SGML, and the inherent limitations of regular
tree automata in dealing with associative-commutative algebras.
The class of automata considered here, called sheaves automata, is a
tailored version of automata for unranked trees with both associative
and associative-commutative symbols already proposed by the
authors. In order to handle both ordered and unordered operators, we
combine the transition relation of regular tree automaton with regular
word expression and counting constraints. This extension appears quite
natural since, when no counting constraints occurs, we obtain hedge
automata, a simple model for XML schemata, and when no constraints
occur, we obtain regular tree automata.
Building on the classical connection between logic and automata, we
also present a decidable tree logic that embeds XML Schema as a plain
subset.
------------------------------------------------------------------------------
- About this document ...
Roberto Amadio
2002-10-22