Entropy model checking [NOTE: CHANGE OF LOCATION]

Add to your list(s) Download to your calendar using vCal

• Chunyan Mu, University of Birmingham
• Thursday 26 June 2014, 11:00-12:00
• Room 217, School of Computer Science.

If you have a question about this talk, please contact Matthijs Melissen.

NOTE : PLEASE NOTE THAT DUE TO ANOTHER MEETING TAKING PLACE IN ROOM 245 , THIS SEMINAR WILL BE IN ROOM 217 .

Classical model-checking answers whether the behaviours of a given system S meets a given specification P. Quantitative model-checking tries to give a quantitative measure characterising to which extent S satisfies P. One of the approaches is to quantify how many behaviours of S satisfy (or violate) P, and the most popular way is to compute probabilities. In many situations probabilistic verification is highly relevant, but it has one important limitation: for many interesting properties, the probability (on infinite-behaviours) is either 0 or 1 – and thus no quantitative analysis is possible. We introduce an alternative approach to the quantitative “model-measuring”, generalising and formalising the problem based on the notion of entropy, we also study the asymptotic behaviour in temporal logic based on the entropy interpretation. A straightforward application would be an information flow capacity calculation for instance.

In the talk, I will recall the notion of the entropy of an \omega-language from the beginning, explain how to compute the entropy of temporal logic formulas (LTL, without time bounds), describe its application to model-checking, formulate its basic properties in model-checking context, apply the approach to a simplified version of dining philosophers problem.

Furthermore, if we have enough time, we will look at time-bounded operators (PLTL), study the “approximability” of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to \infinity—convergence in entropy, i.e. \limit_{t → \infinity} H(\phi) = H(\phi)?? (where H denotes entropy, \phi denotes a time-bounded logic formula).

This talk is part of the Computer Security Seminars series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Security Seminars
• Room 217, School of Computer Science
• computer sience

Note that ex-directory lists are not shown.