Where :

Keywords:

finite automata theory, model-checking, algorithms.

Description:

Traditionally, the behaviour of a system can be described by a set of traces (i.e., a language) where each letter corresponds to a particular action or event in the system. The correctness of a system design is then expressed by a condition on this language, namely that all traces of the system satisfy a certain property (or specification). Correctness is then established by mean of language-theoretic constructions from automata theory.

This traditional view is qualitative and boolean: (1), the specification sharply separates the good and the bad traces (without any nuance), and (2) a system is evaluated as either correct or incorrect, leaving no space for intermediate evaluation. However, the reality is often richer, and for instance among two correct systems, one may be more desirable than the other; or for an incorrect system, it may be useful for a designer to know how far it is from a correct solution. Moreover, the traditional boolean view is not robust since a slight change in the behavior of a correct system may turn it into an incorrect one (and vice versa). Therefore, the traditional view is limited and we advocate a richer notion of language and correctness, namely quantitative languages and quantitative correctness.

>From a mathematical standpoint, a quantitative language assigns to every trace a value (e.g., a real number) instead of a boolean, and a quantitative notion of correctness assigns a value (e.g., a distance) to a pair of system and specification. Some recent works have proposed quantitative frameworks [1, 2, 3], and we propose to further develop them. In particular, we will study theoretical foundations of quantitative languages, using the theory of weighted automata. The objective is to describe canonical ways of defining quantitative languages, as well as decomposition of quantitative languages into simple building blocks, with the objective of providing a compositional (or hierarchical) theory of such languages, in analogy to the theory of ω-regular languages where for instance a classification such as the Borel hierarchy, or the decomposition of any language into safety and liveness languages are fundamental for a better understanding of the theory. In this context, it will be useful to explore logical characterizations of quantitative languages, and of quantitative correctness, and/or to propose equivalent automata-based approaches to the specification of classes of quantitative languages.

An important aspect of this research proposal is the complexity and algorithmic issue. It will be of interest to study the computational complexity of the classical problems of satisfiability and model-checking (or their quantitative counterpart), and to propose algorithms to solve (or approximate) the verification problems that will arise. As it can be expected that the quantitative problems lie in higher complexity classes than the boolean problems, we will need to construct abstraction-refinement techniques for quantitative verification. While abstraction is well studied in the traditional setting of boolean verification and languages, it is a much more open topic in the quantitative world.

Expected skills of the student:

Knowledge in automata theory, combinatorics, and analysis. Language: French or English.

Contact :

References

[1]

P. A. Abdulla, P. Krcál, and W. Yi. R-automata. In Proc. of CONCUR, LNCS 5201, pages 67–81. Springer, 2008.

[2]

K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. In Proc. of CSL, LNCS 5213, pages 385–400. Springer, 2008.

[3]

T. Colcombet, D. Kuperberg, and S. Lombardy. Regular temporal cost functions. In Proc. of ICALP, LNCS. Springer, 2010.

This document was translated from L^AT_EX by H^EV^EA.