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
- computer sience
Note that ex-directory lists are not shown. |
## Other listsApplied Topology Colloquium Particle Physics Seminars Geometry and Mathematical Physics seminar## Other talksTBA Counting cycles in planar graphs TBC Quantum Sensing in Space TBA Proofs of TurĂ¡n's theorem |