Abstract:
The study of the growth rate (or entropy, capacity, information content) of formal languages has drawn the attention of the communities of automata theory, symbolic dynamics and ergodic theory, coding theory, Kolmogorov complexity etc. Its interest to the formal methods community is related with quantitative verification problems, where one needs to evaluate the degree of satisfaction of some property in a model, and the growth rate of the set of behaviors in the model corresponding with the desired property represents an alternative to probabilistic approaches, alternative grounded in deep results from the above-cited domains. We propose here a notion of bandwidth, or information content per time unit, which generalizes growth rate to timed languages, and more particularly to timed automata. We show that timed automata can be partitioned in three classes: (1) meager automata, whose bandwidth is O(1), (2) normal automata, whose bandwidth is Θ(log(1/ε)), and (3) obese, whose bandwidth is Θ(1/ε). Additionally, we provide algorithms for computing the bandwidth for each class of automata. The techniques utilized combine the introduction of a pseudo-distance which defines a pseudo-compact space of timed words, semiring presentations of refinements of the region graph of a timed automaton, spectral radius computation of adjacency matrices of graphs, and the Simon factorization theorem. Based on joint work with Eugène Asarin, Aldric Degorre and Bernardo Jacobo Inclán.
Short Bio:
Catalin Dima is a full professor at Laboratoire d’Algorithmique, Complexité et Logique (LACL) of the Université Paris Est Créteil in France. He has graduated from the University of Bucharest in 1995 and received a PhD from the Unviersité Joseph Fourier Grenoble in 2001, and a Habilitation from Université Paris-Est Créteil in 2010.
His research interests focus on the study of the algorithmic properties for logics for temporal, strategic and probabilistic reasoning, their relationship with classes of automata and game structures, and their applications in the modeling, specification and verification of qualitative and quantitative properties inspired from the domain of safety critical and/or secure systems. He is also interested in the algorithmic study of automata-related notions of entropy and their applications in security for specifiying and verifying anonymity and the existence of covert channels.
