My Third Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)

This is the third guest post by MohammadReza Mousavi on ICALP 2008.

Ran Canetti: Composable Formal Security Analysis (Invited Speech)

Ran underscored the fact that the most challenging part of verifying security is to guarantee that protocols remain secure when put in arbitrary contexts and composed with other protocols. He defined a notion of security which basically requires that the observational behavior of a protocol in the presence of an "environment" machine (which can interfere in all possible ways) emulates the behavior of a perfectly secure protocol with a trusted third party. Combining symbolic methods with concrete cryptographic protocols is another aspect of composition theorem. Explicit analysis of all possible combination of such protocols is infeasible.

The message of the talk can be nicely summarized in the following nice quote (unfortunately forgot from whom):

"In security, the sum of the parts is a hole."

Addendum from Luca: Ran attributed the above quote to Dave Safford.

Patricia Bouyer: On Expressiveness and Complexity in Real-time Model Checking

Metric Temporal Logic (MTL) is a popular extension of Linear Temporal Logic (LTL) with quantitative timing, for which model-checking problem over dense-time models is undecidable. The main culprit for the undecidability is the presence of punctuality, i.e., formulae in which one can talk about exact time moments of events. Thus, punctuality-free fragments of MTL, such Metric Interval Temporal Logic (MITL), are proposed which are decidable. Patricia introduced a new subset of MTL, called coFlat-MTL, which can express properties such as global invariance, bounded response, and some kinds of punctuality (e.g., punctual response), for which model-checking over timed-automata models is in EXPSPACE. She also gave a tableau construction algorithm for this logic.

Antonin Kucera: Controller Synthesis and Verification of Markov Decision Processes

Antonin first showed why we need randomized and history dependent strategies (even bounded memory is insufficient) to control CMDP in order to satisfy qPCTL formulae. Then he presented a study of the complexity of the controller synthesis problem for Markov Decision Processes, which is the following question:

Is there a history dependent randomized strategy such that a given model satisfies a given qPCTL(*) formula?

(qPCTL is an extension of CTL, which allows for specifying properties like: with a probability less than .5, a state with a certain property will be reached.) According to his study, if I remember well, the controller synthesis problem for qPCTL(*) formulae is (2-)EXPTIME-complete in the size of the formula and polynomial in the size of the MDP.