Temporal Quantitative Specification

Date: Thursday, October 07, 2010
Speaker: Udi Boker
Venue: IST Austria

We aim to enrich the specifications of finite state systems with quantitativeaspects. Specifically, we consider systems (Kripke structures) with numericvariables, and look for a suitable specification language in the form ofa temporal-logic over the accumulative sum and average of the variables. Anexample for such a specification is Always( Sum(energy) > 0 or Sum(money)> 0 ) and Eventually-Always( Average(Revenue) > 1,000,000 ). As a first stage,we examine the expressiveness limits that still allow for a decidablemodel-checking procedure. In the talk, I plan to explain our research directionand the results we have so far. This is a joint work with KrishnenduChatterjee, Thomas Henzinger and Orna Kupferman.

Posted in RiSE Seminar