Evènement pour le groupe Graphes et Logique

Date 2013-07-02  11:00-12:00
TitreSpecification of Quantitative Properties: Logics, Automata, Expressions 
RésuméAutomatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. We study several formalisms, equipped with weights, able to specify such properties: denotational ones – like regular expressions, first-order logic, or temporal logics – or more operational ones, like navigating automata, possibly extended with pebbles. We study the compared expressiveness of these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures permitting to handle finite words, ranked trees, nested words, pictures or messsage sequence charts, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modelling databases for example), or natural language processing. We also present results about algorithmic questions that naturally arise in this context, like evaluation and satisfiability. 
LieuSalle 076 
OrateurBenjamin Monmege 
UrlENS Cachan 

Aucun document lié à cet événement.

Retour à l'index