| Title | : | LTL can be more succinct |
| Speaker | : | Sreejith A.V. (Universrity of Warsaw, Poland) |
| Details | : | Tue, 14 Feb, 2017 2:30 PM @ BSB 361 |
| Abstract: | : | In this talk, we will look at an extension of Linear time Temporal Logic (LTL) using modular counting and a further extension which includes group modalities. We see that the modular counting extension of LTL increases the expressive power. The logic can now talk about periodic properties. Moreover, we see that the satisfiability and model checking problem for this logic is in PSPACE. Note that, the satisfiability and model checking problem for LTL is Pspace-complete. We also identify a sublogic which is hard for PSPACE. Next, we look at similar extensions over Unary Temporal Logic (UTL). We will see that the satisfiability problem for an interesting extension of UTL is complete for the third level of the Polynomial Time Hierarchy.
Along with the algorithmic problems, we will also look at algebraic characterizations for these logics. This helps us compare the expressive power of various logics. Speaker Bio: Dr. A. V Sreejith is currently a post doctoral fellow at the University of Warsaw. Prior to this he has held postdoctoral positions at TIFR Mumbai, LIAFA Paris, CMI Chennai. He has completed his PhD from IMSc Chennai and masters from IIT Madras. He specializes in the areas of Verification, Logic for Computer Science and Descriptive Complexity Theory. |
