Talks & Seminars
Title: Specification and Verification of Quantitative Properties via Expressions, Logics, and Automata
Prof. Paul Gastin, Ecole Normale Superieure (ENS) de Cachan, France
Date & Time: January 15, 2014 15:30
Venue: Conference Room, C Block, 01st Floor, Department of Computer Science and Engineering, Kanwal Rekhi Building
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. Examples of quantitative properties are the lifespan of an equipment, the 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. In this talk, we will investigate several formalisms, equipped with weights, able to specify such properties : denotational ones — like regular expressions, first-order logic with transitive closure, or temporal logics — or more operational ones, like navigating automata, possibly extended with pebbles. A first objective is to study some expressiveness results comparing 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. This permits to handle finite words and trees, nested words, pictures or Mazurkiewicz traces, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modeling databases for example), or natural language processing. Second, we tackle some of the algorithmic questions that naturally arise in this context, like evaluation and satisfiability. In particular, we study some decidability and complexity results of these problems depending on the underlying semiring and the structures under consideration (words, trees...). Finally, we consider some interesting restrictions of the previous formalisms. Some permit to extend the class of semirings on which we may specify quantitative properties. Another is dedicated to the special case of probabilistic specifications : in particular, we study syntactic fragments of our generic specification formalisms generating only probabilistic behaviors.
Speaker Profile:
Prof Paul Gastin is a professor of computer science and the current head of the computer science department at Ecole Normale Superieure (ENS) de Cachan, France. He is also the co-director of the Indo-French International Laboratory (InForMeL). His research domain is the verification and control of safety critical systems, with a focus on concurrent and real-time systems. His works include models for such systems (distributed, quantitative, real-time automata, sequence diagrams, Mazurkiewicz traces); specification formalisms such as temporal logics (expressivity, decidability, complexity); and the development of efficient algorithms for verification and control.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback