University of Birmingham > Talks@bham > Computer Security Seminars > Entropy model checking [NOTE: CHANGE OF LOCATION]

## 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
Note that ex-directory lists are not shown. |
## Other listsComputer Science Lunch Time Talk Series Computer Security Seminars Cond. Mat. seminar## Other talksThe Leech Lattice and the Conway Groups Algebraic and combinatorial decompositions of Fuchsian groups Subgroups of the Monster RSC 2019 Dalton Emerging Researcher Award Lecture TBA Role of Mechanics and Geometry in Cellular Information Processing |