Centre for Formal DesignandVerification of Software

Wednesday Seminars

Next SeminarSeminar ListingHome

December

Seminar-13-12-3
 Date - 23th Dec 2013 Time - 02:30 PM Speaker - Prof. Rohit Parikh, Distinguished Professor, Graduate Center,City University of New York and Brooklyn College Title - KNOWLEDGE FROM INADVERTANT AND STRATEGIC COMMUNICATION Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

A popular model in knowledge updating is where we receive true information from a trusted source. The work of Jan Plaza and others, and the AGM theory both use this paradigm. This is also the method used by Geanakoplos and Polemarchakis, and RP and Krasucki, in their "activist" versions of Aumann's result. However, the literature is rife with examples where information is revealed inadvertantly so that the one revealing information is not doing it deliberately but is tricked into it. We give examples from Shakespeare, Saki and Birbal. A second departure from the paradigm arises when the two sources do not share objectives, so that the Gricean assumption of cooperation does not hold. Nonetheless, some information can get across when the interests of the two parties overlap at least in part. We report on some theoretical work in this area, some of it falling under the heading of "cheap talk," and offer a model. Speaker Profile: Prof. Rohit Parikh is a Distinguished Professor of Computer Science, Mathematics and Philosophy at the Graduate Center, City University of New York. He is also affiliated with Department of Computer Science at Brooklyn College. Prof. Parikh has made deep contributions to wide range of areas including formal languages, recursive function theory, proof theory, non-standard analysis, logic of programs, logic of knowledge, philosophy of language, belief revision and game theory. The theme that concerns most of his recent papers is Social Software, which is an analysis of social procedures, from elections to cake cutting, using ideas from Computer Science, Game Theory and Logic. Organization: City University of New York and Brooklyn College

References
To be updated

Seminar-13-12-2
 Date - 18th Dec 2013 Time - 03:15 PM Speaker - Dr. Emmanuel Filiot Title - Exploiting Structure in LTL Synthesis Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures. Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem. In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem. Speaker Profile: Emmanuel Filiot (PhD 2008, INRIA Lille, France) is an FNRS research associate in the computer science department of Brussels University (ULB), since September 2013. His research interests cover the theoretical foundations of data-centric systems and synthesis of reactive systems from temporal specifications, based on automata, transducer and logics for strings and trees, and computational game theory. He teaches foundations of computer-science at Brussels University. Organization: Brussels University

References
To be updated

Seminar-13-12-1
 Date - 13th Dec 2013 Time - 03:00 PM Speaker - Dr. Emmanuel Filiot Title - TRANSDUCER THEORY AND STREAMING TRANSFORMATIONS Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Finite state automata are language acceptors. They map strings read on their input tape to {0,1}. Transducers extend automata with an output tape, and can therefore map strings to other strings. This talk will first survey some of the main results of the theory of finite state transducers. Then, several major extensions will be presented, that either increase the computational power of finite state transducers (e.g. by allowing the input head to move in both directions), or process more general structures, e.g. infinite strings or trees. Finally, an application to streaming transformations and its connection with strategy synthesis in game theory for reactive systems (Church problem) will be shown. Speaker Profile: Emmanuel Filiot (PhD 2008, INRIA Lille, France) is an FNRS research associate in the computer science department of Brussels University (ULB), since September 2013. His research interests cover the theoretical foundations of data-centric systems and synthesis of reactive systems from temporal specifications, based on automata, transducer and logics for strings and trees, and computational game theory. He teaches foundations of computer-science at Brussels University. Organization: Brussels University

References
To be updated

November

Seminar-13-11-2
 Date - 20th Nov 2013 Time - 03:15 PM Speaker - Arnaud Durand, Professor University Denis Diderot - Paris 7,France Title - Structural tractability of counting solutions to conjunctive queries Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Computing aggregates such as the sum or the counting of solutions is a natural task in databases. Conjunctive queries are a basic class of queries equivalent to select-project-join queries and strongly related to constraint satisfaction problems. Most research on conjunctive queries has focused on the so-called boolean conjunctive query problem, short CQ, which is, given a query and a database, to decide if the query has any answers with respect to the database. While CQ is hard in general, many 'islands of tractability' have been found based on the hypergraphs associated to queries. Recently, Pichler and Skritek have shown that these hypergraph based techniques are not sufficient to guarantee tractability for the associated counting problem #CQ, i.e., given a conjunctive query and a database, determine the number of answers to the query. I will give a short introduction into conjunctive queries and survey know results. I will also present an exact characterizion of the tractability frontier for #CQ for well-known classes of conjunctive queries. Joint works with Stefan Mengel (JCSS and ICDT 2013).

References
1. Structural tractability of counting of solutions to conjunctive queries. ICDT 2013: 81-92. by Arnaud Durand, Stefan Mengel.
2. The complexity of weighted counting for acyclic conjunctive queries. J. Comput. Syst. Sci. 80(1): 277-296 (2014). by Arnaud Durand, Stefan Mengel.

Seminar-13-11-1
 Date - 13th Nov 2013 Time - 03:15 PM Speaker - Nishanth Dikkala, 4th year UG student, Dept. of CSE Title - Effect of credit on revenue in advertisement auctions Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Among the applications of algorithmic game theory (AGT) are sponsored search auctions such as those of Google's AdWords. In on-line advertisement systems, advertisers are repeatedly involved in auctions to acquire advertisement spaces. Classical models of private value auctions assume that bidders know their own private value for the slot being auctioned. We explore games where players have a private value, but can only learn this value through experimentation, a scenario that is typical in AdAuctions. We consider this question in a repeated game context, where early participation in the auction can help the bidders learn their own value. We consider what is a good bidding strategy for a player in this game, and show that with low enough competition new bidders will enter and experiment, but with a bit higher level of competition, initial credit offered by the platform can encourage experimentation, and hence ultimately can increase revenue.

References
1. Can Credit Increase Revenue? In Proceedings of the Ninth ACM international conference on Web, Internet, Networking and Economics, WINE 2013. by Nishanth Dikkala and Eva Tardos.
2. Peaches, lemons, and cookies: Designing auction markets with dispersed information. ACM Confer- ence on Economic Commerce, 2013. by Ittai Abraham, Susan Athey, Moshe Babaio, and Michael Grubb.
3. Mean Field Equilibria of Dynamic Auctions with Learning, ACM Conference on Economic Commerce, 2011 by Krishnamurthy Iyer, Ramesh Johari, Mukund Sundararajan.
4. Optimal Bidding Strategies and Equilibria in Repeated Auctions with Budget Constraints. Ad Auc- tions Workshop, 2012. by Ramakrishna Gummadi, Peter Key and Alexandre Proutiere.

October

Seminar-13-10-1
 Date - 9th Oct 2013 Time - 03:15 PM Speaker - Ganesh Narwane, Ph.D. student, Dept. of CSE Title - Compositional Verification of Evolving Software Product Lines Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs at the feature level are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviourally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.

References
1. Automated analysis of feature models 20 years later: a literature review. Information Systems by Benavides, D., Segura, S., Ruiz-Corts, A
2. Modal i/o automata for interface and product line theories. In: Proceedings of ESOP 2007. by Larsen, K.G., Nyman, U., Wasowski, A.
3. Tracing software product line variability: from problem to solution space. In: Proceedings of SAICSIT '05. by Berg, K., Bishop, J., Muthig, D.
4. Disambiguating the documentation of variability in software product lines: A separation of concerns, formalization and automated analysis. In: Proceedings of RE 2007. by Metzger, A., Pohl, K., Heymans, P., Schobbens, P.Y., Saval, G.

September

Seminar-13-09-2
 Date - 25th Sept 2013 Time - 03:15 PM Speaker - Ganesh Narwane, Ph.D. student, Dept. of CSE Title - Compositional Verification of Evolving Software Product Lines Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs at the feature level are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviourally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.

References
1. Automated analysis of feature models 20 years later: a literature review. Information Systems. by Benavides, D., Segura, S., Ruiz-Corts, A.
2. Modal i/o automata for interface and product line theories. In: Proceedings of ESOP 2007. by Larsen, K.G., Nyman, U., Wasowski, A.
3. Tracing software product line variability: from problem to solution space. In: Proceedings of SAICSIT '05. by Berg, K., Bishop, J., Muthig, D.
4. Disambiguating the documentation of variability in software product lines: A separation of concerns, formalization and automated analysis. In: Proceedings of RE 2007. by Metzger, A., Pohl, K., Heymans, P., Schobbens, P.Y., Saval, G.

Seminar-13-09-1
 Date - 11th Sept 2013 Time - 03:15 PM Speaker - Ganesh Narwane, Ph.D. student, Dept. of CSE Title - Tracing SPLs Precisely and Efficiently Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

In a Software Product Line (SPL), the central notion of implementability provides the requisite connection between specifications (feature sets) and their implementations (component sets), leading to the definition of products. While it appears to be a simple extension (to sets) of the traceability relation between components and features, it actually involves several subtle issues which are overlooked in the definitions in existing literature. In this paper, we give a precise and formal definition of implementability over a fairly expressive traceability relation to solve these issues. The consequent definition of products in the given SPL naturally entails a set of useful analysis problems that are either refinements of known problems, or are completely novel. We also propose a new approach to solve these analysis problems by encoding them as Quantified Boolean Formula(QBF) and solving them through Quantified Satisfiability (QSAT) solvers. The methodology scales much better than the SAT-based solutions hinted in the literature and is demonstrated through a prototype tool called SPLANE(SPL Analysis Engine),on a couple of fairly large casestudies.

References
1. Automated analysis of feature models 20 years later: a literature review. Information Systems, 35(6):615636, 2010. by D. Benavides, S. Segura, and A. Ruiz-Cort¿½es
2. Tracing software product line variability: from problem to solution space. Proceedings of SAICSIT05, pages 182191, 2005. by K. Berg, J. Bishop, and D. Muthig
3. A feature-oriented reuse method with domain-specic reference architectures. Ann. Software Eng., 5:143168, 1998. by K. C. Kang, S. Kim, J. Lee, K. Kim, E. Shin, and M. Huh
4. Disambiguating the documentation of variability in software product lines: A separation of concerns, formalization and automated analysis. In Proceedings of RE 07, pages 243253, 2007. by A. Metzger, K. Pohl, P. Heymans, P. Schobbens, and G. Saval
5. Tracing SPLs precisely and efficiently, 16th International Software Product Line Conference (SPLC), 2012, pp. 186-195. by S. Mohalik, S. Ramesh, J. Millo, S. Krishna and G. Narwane

August

Seminar-13-08-3
 Date - 21st August 2013 Time - 03:15 PM Speaker - Ashish Chiplunkar, Ph.D. student, Dept. of CSE Title - On Randomized Memoryless Algorithms for the Weighted $k$-server Problem Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

n the $k$-server problem, $k$ servers occupy points in a metric space. An adversary presents a sequence of online requests, each of which is a point in the metric space. To serve the current request, the algorithm has to move one of the servers to the requested point, incurring a cost equal to the distance traveled by the server. The weighted $k$-server problem is a generalization of the $k$-server problem in which the servers have weights, and the cost of moving a server of weight $\beta_i$ through a distance $d$ is $\beta_i\cdot d$. In this talk I will discuss techniques for proving upper bounds for randomized memoryless algorithms for the weighted server problem on the uniform metric space. This models paging where pages may have different write costs. I will exhibit an algorithm that always outputs a solution to within roughly 2^2^k times the optimal. The interesting thing is that the approximation factor is a function of k alone and not of either the number of points in the metric space nor the length of the request sequence. Previously such a result was known only for $k=2$. Our result also significantly improves the best known upper bound for deterministic algorithms. I will also present a partial proof hinting at the optimality of these results. The paper is joint work with Sundar Vishwanathan and is available here

References
1. The Weighted 2-server Problem by Marek Chrobak, Jiri Sgall
2. Competitive algorithms for the weighted server problem by Amos Fiat, Moty Ricklin
3. The $k$-server problem by Elias Koutsoupias

Seminar-13-08-2
 Date - 14th August 2013 Time - 03:15 PM Speaker - Rajeev Alur, Zisman Family Professor, Department of Computer and Information Science, University of Pennsylvania Title - Nested Words and Trees Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

This talk is centered around our recent model of nested words as a representation of data with both a linear ordering and a hierarchically nested matching of items. Such dual structure occurs in diverse corners of computer science ranging from executions of structured programs where there is a natural well-nested matching of entries to and exits from functions and procedures, to XML documents with the well-nested structure given by start-tags matched with end- tags. Finite-state acceptors for nested words define the class of regular languages of nested words that has all the appealing theoretical properties that the class of classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, and Kleene-*; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We argue that for algorithmic linear-time verification of pushdown systems, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words, and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics. We also discuss nested trees that are obtained adding nesting edges along paths of trees, and finite-state acceptors over nested trees. This leads to a very expressive fixpoint logic (equivalently, alteranting parity nested tree automata) with a decidable model checking problem for pushdown systems.

References
1. Audio for this talk by Rajeev Alur

Seminar-13-08-1
 Date - 7th August 2013 Time - 03:00 PM Speaker - Akshay S., Dept. of CSE, IIT Bombay Title - On Skolem's problem with applications to program termination and probabilistic verification Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

In this talk, we will talk about decision problems for linear recurrence sequences (LRS), which are generalizations of the Fibonacci sequence. Starting from the long-standing open Skolem problem (which asks if a given LRS has a zero), we will look at several variants and survey some recent results in this area. Further, we will motivate these highly mathematical problems by showing how they occur rather naturally in the domains of program termination and probabilistic verification.

References
1. Asymptotic behaviour of linear recurrences. Fib. Quart., 19(4), 1981. by Burke and Webb
2. Polynomial time Algorithm for the Orbit Problem, JACM, 1986 by Kannan, Lipton
3. Termination of Linear Programs, CAV 2004. by Tiwari
4. Positivity of second order linear recurrent sequences. Disc. App. Math. 154(3), 2006. by Havala, Harju, Hirvensalo

July

Seminar-13-07-2
 Date - 22nd July 2013 Time - 02:15 PM Speaker - Prof. Rahul Mangharam Title - CLOSING THE LOOP WITH CYBER-PHYSICAL SYSTEM MODELING Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Cyber-Physical Systems are the next generation of embedded systems with the tight integration of computing, communication and control of â€œmessyâ€ plants. I will describe our recent efforts in modeling for scheduling and control of closed-loop Cyber-Physical Systems across the domains of medical devices, energy-efficient buildings, wireless control networks and programmable automotive systems.

The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs whose response is not fully understood. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600,000 devices. Of these, 200,000 or 41%, were due to firmware issues (i.e. software) that continue to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. I will describe our efforts to develop the foundations of modeling, synthesis and development of verified medical device software and systems from verified closed-loop models of the pacemaker and the heart. With the goal to develop a tool-chain for certifiable software for medical devices, I will walk through (a) formal modeling of the heart and pacemaker in timed automata, (b) verification of the closed-loop system, (c) automatic model translation from UPPAAL to Stateflow for simulation-based testing, and (d) automatic code generation for platform-level testing of the heart and real pacemakers. More details here.

As time permits, I will describe our investigations inenergy-efficient building automation in which we coordinate scheduling of controllers for peak power minimization across multiple plants. We will also briefly discuss in-vehicle and networked vehicle-to-vehicle programmable automotive architectures for the future.

Speaker Profile: Rahul Mangharam is the Stephen J Angello Chair and Assistant Professor in the Dept. of Electrical & Systems Engineering and Dept. of Computer &Information Science at the University of Pennsylvania. He directs the Real-Time and Embedded Systems Lab at Penn. His interests are in real-time scheduling algorithms for networked embedded systems with applications in automotive systems, medical devices and industrial control networks.

He received his Ph.D. in Electrical & Computer Engineering from Carnegie Mellon University where he also received his MS and BS in 2007, 2002 and 2000 respectively. In 2002, he was a member of technical staff in the Ultra-Wide Band Wireless Group at Intel Labs. He was an international scholar in the Wireless Systems Group at IMEC, Belgium in 2003. He has worked on ASIC chip design at Marconi Communications (1999) and Gigabit Ethernet at Apple Computer Inc. (2000). Rahul received the 2013 NSF CAREER Award, 2012 Intel Early Faculty Career Award and was selected by the National Academy of Engineering for the 2012 US Frontiers of Engineering.

References
To be updated

Seminar-13-07-1
 Date - 3rd July 2013 Time - 03:00 PM Speaker - Rajeev Alur, Zisman Family Professor of Computer and Information Science, University of Pennsylvania Title - Interfaces for Control Components Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

[This talk was a video screening of a talk by Rajeev Alur. Video link: here]

Modern software engineering heavily relies on clearly specified interfaces for separation of concerns among designers implementing components and programmers using those components. The need for interfaces is evident for assembling complex systems from components, but more so in control applications where the components are designed by control engineers using mathematical modeling tools and used by software executing on digital computers. However, the notion of an interface for a control component must incorporate some information about timing, and standard programming languages do not provide a way of capturing such resource requirements.

This talk will describe how finite automata over infinite words can be used to define interfaces for control components. When the resource is allocated in a time-triggered manner, the allocation from the perspective of an individual component can be described by an infinite word over a suitably chosen alphabet. The control engineer can express the interface of the component as an omega-regular language that contains all schedules that meet performance requirement. The software must ensure, then, that the runtime allocation is in this language. The main benefit of this approach is composability: conjoining specifications of two components corresponds to a simple language-theoretic operation on interfaces.

We have demonstrated how to automatically compute automata for performance requirements such as exponential stability and settling time for the LQG control designs. The framework is supported by a toolkit, RTComposer, that is implemented on top of Real Time Java. The benefits of the approach will be demonstrated using applications to wireless sensor/actuator networks based on the WirelessHART protocol and to distributed control systems based on the Control Area Network (CAN) bus.

References
1. Wiki link about the author by Wikipedia

June

Seminar-13-06-3
 Date - 19th June 2013 Time - 03:00 PM Speaker - Abhisekh Sankaran, Ph.D. student, Dept. of CSE Title - Some techniques to prove inexpressibility results in First Order Logic Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

[This is a continuation of the talk given by the speaker on June 12]
First Order Logic (FOL) is one of the most natural logics in which a wide variety of mathematical statements can be written. For example, various properties of widely used structures like groups, rings, fields, partial orders, lattices, etc., in fact their very definitions, can be expressed in FOL. In computer science, the flourishing area of descriptive complexity is all about giving logical characterizations of complexity classes that are defined using other mechanisms like turing machines, circuits, etc. -- and FOL is again useful in capturing several interesting complexity classes. SQL (Structured Query Language), which is one of the most widely used database query languages, is exactly FOL when aggregation and other counting constructs are dropped.

Ironically, as useful as it is in many contexts, FOL is as weak to express many natural properties that are of mathematical interest. In the context of graphs, FOL is incapable of expressing properties like connectedness, tree-ness, k-colourability, amongst many others. In fact as trivial a property as the evenness of the size of a graph is also FO inexpressible! In this talk, we shall look at these and other inexpressibility results and some techniques used in proving them. We shall also try to give an intuitive idea of why FOL must show this weakness in its expressiveness. Time permitting, we shall delve into the inexpressibility of FOL over arbitrary structures (i.e. infinite structures included) and present, amongst other techniques, some new techniques (having limited applicability) based on some our recent results in the area of model theory.

References
1. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press New York, NY, 2004, ISBN:052154310X by M. Huth and M. Ryan
2. Elements of Finite Model Theory. Springer, 2004. ISBN: 3-540-21202-7. by Leonid Libkin
3. Model Theory, Elsevier Science Publishers, 3rd edition, 1990. by C. C. Chang and H. J. Keisler
4. Using Preservation Theorems for Inexpressibility Results in First Order Logic. Technical Report, CFDVS, 2012. by Abhisekh Sankaran, Nutan Limaye, Akshay Sundararaman and Supratik Chakraborty

Seminar-13-06-2
 Date - 12th June 2013 Time - 03:00 PM Speaker - Abhisekh Sankaran, Ph.D. student, Dept. of CSE Title - Some techniques to prove inexpressibility results in First Order Logic Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

First Order Logic (FOL) is one of the most natural logics in which a wide variety of mathematical statements can be written. For example, various properties of widely used structures like groups, rings, fields, partial orders, lattices, etc., in fact their very definitions, can be expressed in FOL. In computer science, the flourishing area of descriptive complexity is all about giving logical characterizations of complexity classes that are defined using other mechanisms like turing machines, circuits, etc. -- and FOL is again useful in capturing several interesting complexity classes. SQL (Structured Query Language), which is one of the most widely used database query languages, is exactly FOL when aggregation and other counting constructs are dropped.

Ironically, as useful as it is in many contexts, FOL is as weak to express many natural properties that are of mathematical interest. In the context of graphs, FOL is incapable of expressing properties like connectedness, tree-ness, k-colourability, amongst many others. In fact as trivial a property as the evenness of the size of a graph is also FO inexpressible! In this talk, we shall look at these and other inexpressibility results and some techniques used in proving them. We shall also try to give an intuitive idea of why FOL must show this weakness in its expressiveness. Time permitting, we shall delve into the inexpressibility of FOL over arbitrary structures (i.e. infinite structures included) and present, amongst other techniques, some new techniques (having limited applicability) based on some our recent results in the area of model theory.

References
1. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press New York, NY, 2004, ISBN:052154310X by M. Huth and M. Ryan
2. Elements of Finite Model Theory. Springer, 2004. ISBN: 3-540-21202-7. by Leonid Libkin
3. Model Theory, Elsevier Science Publishers, 3rd edition, 1990. by C. C. Chang and H. J. Keisler
4. Using Preservation Theorems for Inexpressibility Results in First Order Logic. Technical Report, CFDVS, 2012. by Abhisekh Sankaran, Nutan Limaye, Akshay Sundararaman and Supratik Chakraborty

Seminar-13-06-1
 Date - 5th June 2013 Time - 03:00 PM Speaker - Moshe Vardi, Karen Ostrum George Distinguished Service Professor, Rice University, USA. Title - The Rise and Fall of Linear Temporal Logic Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

[This talk was a video screening of an invited talk at KR 2012 (Intl. Conference on Principles of Knowledge Representation and Reasoning)]

One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of linear temporal logic (LTL), a logic that emerged in philosophical studies of free will, as the canonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21st century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new canonical temporal logic: linear dynamic logic (LDL).

References
1. The video and slides of the talk by Moshe Vardi
2. Wiki link about the author by Wikipedia

May

Seminar-13-05-4
 Date - 29th May 2013 Time - 03:00 PM Speaker - Khushraj Madnani, M.Tech Student, Dept. of CSE Title - On the Decidability and Complexity of Some Fragments of Metric Temporal Logic Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

[This is a continuation of the talk given by the speaker on May 22]
Metric Temporal Logic, MTL^{pw} [ U_I , S_I ] is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints I. In this paper, we sharpen the decidability results by showing that the satisfiability of MTL^{pw} [ U_I , S_{NS} ] (where N S denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic MTL^{pw} [ U_I , S_{NS} ] to decidable logic MTL^{pw} [ U_I ] of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment MTL^{pw} [F_I ,P_I ] (a question posed by A. Rabinovich) and show that MTL^{c} [F_I ] over continuous time as well as MTL^{pw} [F_I ,P_I ] over finite point-wise time are both undecidable. Moreover, MTL^{pw} [F_I] over finite point-wise models already has Non primitive Recursive lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for MTL.

References
1. Logics and Models of Real Time: A Survey. Proceedings of REX Workshop 1991, 74-106. by Rajeev Alur and Thomas A. Henzinger
2. Logics for Real Time: Decidability and Complexity. Fundam. Inform., 62(1), 2004, 1-28. by Y. Hirshfeld and A. Rabinovich.
3. On Construction of Safety Signal Automata for MITL[ UI , SI ] using Temporal Projections. Proceedings of FORMATS 2011, 225-239. by D.Kini, S. N. Krishna and P. K.Pandya.
4. On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing. Proceedings of CONCUR 2011, 60-75. by P.K. Pandya, S. Shah.

Seminar-13-05-3
 Date - 22nd May 2013 Time - 03:00 PM Speaker - Khushraj Madnani, M.Tech Student, Dept. of CSE Title - On the Decidability and Complexity of Some Fragments of Metric Temporal Logic Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Metric Temporal Logic, MTL^{pw} [ U_I , S_I ] is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints I. In this paper, we sharpen the decidability results by showing that the satisfiability of MTL^{pw} [ U_I , S_{NS} ] (where N S denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic MTL^{pw} [ U_I , S_{NS} ] to decidable logic MTL^{pw} [ U_I ] of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment MTL^{pw} [F_I ,P_I ] (a question posed by A. Rabinovich) and show that MTL^{c} [F_I ] over continuous time as well as MTL^{pw} [F_I ,P_I ] over finite point-wise time are both undecidable. Moreover, MTL^{pw} [F_I] over finite point-wise models already has Non primitive Recursive lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for MTL.

References
1. Logics and Models of Real Time: A Survey. Proceedings of REX Workshop 1991, 74-106. by Rajeev Alur and Thomas A. Henzinger
2. Logics for Real Time: Decidability and Complexity. Fundam. Inform., 62(1), 2004, 1-28. by Y. Hirshfeld and A. Rabinovich.
3. On Construction of Safety Signal Automata for MITL[ UI , SI ] using Temporal Projections. Proceedings of FORMATS 2011, 225-239. by D.Kini, S. N. Krishna and P. K.Pandya.
4. On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing. Proceedings of CONCUR 2011, 60-75. by P.K. Pandya, S. Shah.

Seminar-13-05-2
 Date - 9th May 2013 Time - 03:00 PM Speaker - Dominik Wojtczak, Lecturer at University of Liverpool, UK. Title - Automated Analysis of Probabilistic Infinite-state Systems Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

[This is a continuation of the talk given by the speaker on May 1]
I will survey the state of the art in the automated analysis of several classes of probabilistic infinite-state systems which naturally arise when studying probabilistic programs with recursive calls, queueing systems, population dynamics and natural language processing. I will describe the relationships between these different models and recent developments in the computational complexity of their analysis. I will also briefly describe tool PReMo, which is able to analyse these models, along with some interesting performance results. (This talk is based on several joint papers with T. Brazdil, V. Brozek, K. Etessami, S. Kiefer, A. Kucera, and M. Yannakakis).

References
1. PReMo : An Analyzer for Probabilistic Recursive Models. TACAS 2007: 66-71 by Dominik Wojtczak, Kousha Etessami
2. Recursive Stochastic Games with Positive Rewards. ICALP (1) 2008: 711-723 by Kousha Etessami, Dominik Wojtczak, Mihalis Yannakakis
3. Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems. Perform. Eval. 67(9): 837-857 (2010) by Kousha Etessami, Dominik Wojtczak, Mihalis Yannakakis
4. On Probabilistic Parallel Programs with Process Creation and Synchronisation. TACAS 2011: 296-310 by Stefan Kiefer, Dominik Wojtczak

Seminar-13-05-1
 Date - 1st May 2013 Time - 03:00 PM Speaker - Dominik Wojtczak, Lecturer at University of Liverpool, UK. Title - Automated Analysis of Probabilistic Infinite-state Systems Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

I will survey the state of the art in the automated analysis of several classes of probabilistic infinite-state systems which naturally arise when studying probabilistic programs with recursive calls, queueing systems, population dynamics and natural language processing. I will describe the relationships between these different models and recent developments in the computational complexity of their analysis. I will also briefly describe tool PReMo, which is able to analyse these models, along with some interesting performance results. (This talk is based on several joint papers with T. Brazdil, V. Brozek, K. Etessami, S. Kiefer, A. Kucera, and M. Yannakakis).

References
1. PReMo : An Analyzer for Probabilistic Recursive Models. TACAS 2007: 66-71 by Dominik Wojtczak, Kousha Etessami
2. Recursive Stochastic Games with Positive Rewards. ICALP (1) 2008: 711-723 by Kousha Etessami, Dominik Wojtczak, Mihalis Yannakakis
3. Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems. Perform. Eval. 67(9): 837-857 (2010) by Kousha Etessami, Dominik Wojtczak, Mihalis Yannakakis
4. On Probabilistic Parallel Programs with Process Creation and Synchronisation. TACAS 2011: 296-310 by Stefan Kiefer, Dominik Wojtczak

April

Seminar-13-04-3
 Date - 24th April 2013 Time - 03:00 PM Speaker - Ashish Chiplunkar, Ph.D. student, CSE, IIT Bombay Title - Online Computation and the k-server problem Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Online computation involves processing "pieces" of input by taking irrevocable decisions on the arrival of every piece. For instance, the caching problem involves servicing each request in a sequence of requests to pages, without the knowledge the future requests. The performance of online algorithms is traditionally expressed by a quantity called "competitive ratio". I will discuss a few elementary techniques to prove bounds on the competitive ratios of online problems, and briefly mention the $k$-server problem, and the best known bounds for this problem. If time permits, I will introduce the weighted $k$-server problem and discuss our recent result about the competitive ratio of memoryless algorithms for this problem.

References
1. The k Server Problem by Elias Koutsoupias
2. New Results on Server Problems by Chrobak et. al.
3. On Randomized Memoryless Algorithms for the Weighted k-server Problem by Sundar Vishwanathan and Ashish Chiplunkar

Seminar-13-04-2
 Date - 17th April 2013 Time - 03:00 PM Speaker - Srikanth Srinivasan, Dept. of Mathematics, IIT Bombay Title - The Exponential Time Hypothesis Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Despite many decades of trying, we do not have algorithms that run in time 2^{o(n)} for 3-SAT. A reasonable hypothesis, therefore, is that such algorithms do not exist. This is called the Exponential Time Hypothesis, and like P \neq NP, it has many implications for other problems. We will see some of them.

References
1. Which Problems Have Strongly Exponential Complexity? by Russell Impagliazzo, Ramamohan Paturi, Francis Zane
2. Complexity of k-SAT by Russell Impagliazzo, Ramamohan Paturi
3. Lower bounds based on the Exponential Time Hypothesis by Daniel Lokshtanov, Daniel Marx, Saket Saurabh
4. On problems as hard as CNF-SAT by Cygan et al.

Seminar-13-04-1
 Date - 10th April 2013 Time - 03:00 PM Speaker - Prof. V. R. Sule, Dept. of Electrical Engg, IIT Bombay Title - Solutions of Boolean equations by orthonormal expansions Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

The talk will address the problem of solving a system of Boolean equations in several variables over finite Boolean algebra co-efficients. The well known Boole-Shannon expansion of a Boolean function is a basis for the method of elimination of variables and condition of consistency in Boolean equations. On the other hand it is always possible to carry out expansion of a Boolean function in a system of orthonormal terms which generalizes the Boole-Shannon expansion vastly. However an equivalent condition for consistency is not available which generalizes the one variable counterpart of Boole-Shannon case. This talk shows that such a condition is possible with respect to two specialized sets of orthonormal terms when the Boolean functions belong to a restricted class.

References

March

Seminar-13-03-2
 Date - 13th March 2013 Time - 04:30 PM Speaker - Prof. Supratik Chakraborty, CSE, IIT Bombay Title - Practical Quantifier Elimination for Linear Bitvector Arithmetic Venue - SIC 301, Kanwal Rekhi bldg., IIT Bombay

Show Details

Abstract

(This was a talk given as a part of the Faculty Seminar Series of the Dept. of CSE.)

Reasoning about fixed width bit-vectors (as opposed to reasoning about integers or reals) is important in the formal verification and analysis of software and hardware systems that use fixed-width words in the underlying machine architecture. While restricting the domain to fixed width bit-vectors renders all interesting problems decidable, the worst-case complexities may still be high, and one needs to exercise care in designing algorithms that scale to problems of practical size. In this talk, we look at the problem of quantifier elimination for linear arithmetic expressions, a key operation in verification, automated synthesis and analysis of important classes of software and hardware systems. We present a layered algorithm for scalable quantifier elimination from Boolean combinations of linear bitvector arithmetic expressions. Our algorithm invokes cheaper, relatively less complete heuristics initially, and invokes more expensive and complete techniques only when needed. We present a substitution based heuristic and a counting based heuristic that are extremely efficient and succeed in eliminating almost all quantifiers in an extensive set of benchmarks from the public-domain. To handle cases that are not amenable to these heuristics, we also present an adaptation of the classical Fourier-Motzkin quantifier elimination algorithm for reals to linear bitvector arithmetic. While this is an expensive step, our experiments indicate that this is invoked in a very small fraction of cases. Our experiments clearly show that a layered approach with carefully designed heuristics lends both precision and scalability to bit-precise quantifier elimination. We are currently working on extending this work to eliminating quantifiers from non-linear bit-vector inequalities and also for combinations of bit-vector theories. This is joint work with Ajith John.

References
To be updated

Seminar-13-03-1
 Date - 6th March 2013 Time - 03:30 PM Speaker - Prof. Paritosh Pandya, TIFR Title - In quest of Logic-Automaton Connection for Unambiguous Star-free Regular Languages Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Unambiguous star-free langauges (UL) were defined by Schutzenberger in 1976 as the variety DA. Since then, this langauge class has found diverse characterizations in logics and automata over finite words. Pioneering work of Pin, Weil, Therien and Wilke showed that logics FO2[<] as well as Delta2[<] characterize this class. Etessami, Vardi and Wilke showed effective equivalence between FO2[<] and the well known "unary" temporal logic TL[F,P]. Schwentik, Volmer and Therien showed that UL are precisely the langauges recognized by Partially ordered 2-way DFA (PO2DFA). The talk will provide a quick overview of these results.

We will then move to more recent work on temporal logics for UL. Four widely different temporal logics over finite words, namely TL[F,P], TL[Xa,Ya], Recursive TL[Xphi,Yphi] and interval logic UITL+- can be shown to be equally expressive and to precisely characterize the language class UL, Moreover, they all have NP complete satisfiability.

Clearly, an explanation of robustness and efficient decidability of temporal logics for UL is needed. Towards this, we formulate effective reductions between these logics and also to PO2DFA, showing that these logics are equally expressive. Moreover, the reductions from logics to automata are efficient and they allows us to establish the NP-Complete satisfiability of all the four logics. We observe that these reductions rely upon on some important properties of "deterministic" temporal logics, namely, unique parsability, ranker directionality and ranker convexity. These will be explained and motivated. (joint work with Simoni Shah.)

References
1. A Survey on Small Fragments of First-Order Logic over Finite Words, Int. J. Found. Comput. Sci.,vol 19, 2008, p 513-548 by Volker Diekert, Paul Gastin and Manfred Kufleitner
2. First-order logic with two variables and unary temporal logic,Inf. Comput.,vol 179, 2002 p 279-295 by K.Etessami, M.Y. Vardi and T.Wilke
3. Partially-ordered two-way automata: a new characterization of DA, Proc.DLT '01,ed Vienna,W.Kuich, G.Rozenberg and A.Salomaa,LNCS,vol 2295, 2002, p 239-250 by T.Schwentick, D.Th'erien and H.Vollmer
4. Marking the chops: an unambiguous temporal logic,Proc. 5th IFIP TCS, Milano, ed G.Ausiello, J.Karhum"aki, G.Mauri and L.Ong, IFIP Series, vol 273, Springer, 2008, p 461-476 by K.Lodaya, P.K. Pandya and S.S. Shah

February

Seminar-13-02-2
 Date - 27th February 2013 Time - 03:30 PM Speaker - Robert I. Soare, Paul Snowden Russell Distinguished Service, Professor of Mathematics and Computer Science at the University of Chicago Title - The Art of Classical Computability: Why Turing and not Church? Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

(This seminar was the video screening of a lecture delivered at the Isaac Newton Institute, University of Cambridge, UK. Video link: Click here)

Why give so much credit to Turing and not to Church? Church was a full professor at Princeton in 1936 when Turing was a mere graduate student. Church had studied Hilbert's papers a decade before Turing and had explained them to his Princeton thesis adviser, Oswald Veblen. Church was working in the Herbrand-Godel recursive functions defined by Godel, the most eminent logician at the time. These used the concept of recursion (induction) which had appreared in mathematics since Dedekind [1888]. In contrast, Turing machines were a fanciful new invention without such a concise, mathematical definition in a familiar formalism. By 1934, Church and Kleene had shown that most number theoretic functions were $\lambda$-definable and therefore recursive, giving clear evidence for Church's Thesis.

Church was the first to propose Church's Thesis when even Godel did not believe it. Church got it right and he got it first. The effectively calculable functions _are_ the recursive functions. By any purely quantifiable evaluation, Church's contribution was at least as important as Turing's. However, characterizing human computability was _not_ a purely quantifiable process.

References
To be updated

Seminar-13-02-1
 Date - 6th February 2013 Time - 03:30 PM Speaker - Prof. V. R. Sule, Dept. of Electrical Engg, IIT Bombay Title - Orthonormal Expansions and Solutions of Boolean Equations Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

This talk is aimed at presenting an approach for solving Boolean equations by expanding the. Functions involved in terms of special systems of orthonormal (ON) terms. These special systems are polynomial order as compared to ON terms such asminterms which are of exponential order. ON expansions bring in a natural parallelism in the computation. This expansion generalizes the Bool-Shannon expansion and the resulting elimination theory of Boolean algebras.

References
1. Boolean functions and equations (ISBN-13: 978-0444105202) by Sergiu Rudeanu

January

Seminar-13-01-4
 Date - 30th January 2013 Time - 03:30 PM Speaker - Dinesh Chattani and Tanmay Haldankar, Dept. of CSE, IIT Bombay Title - Introduction to Symbolic Trajectory Evaluation Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

STE is a symbolic technique for hardware model checking. It supports three valued abstraction(0,1,X). It is a BDD (binary decision diagram) based model checking technique. The abstraction is generated from the user specifications. This evaluation boils down to checking the property that given the antecedent(A) and the circuit specifications, does the consequent (C) hold true. i.e. A => C.

References
1. Symbolic Trajectory Evaluation (STE): Automatic Reﬁnement and Vacuity Detection by Orna Grumberg

Seminar-13-01-3
 Date - 23rd January 2013 Time - 03:30 PM Speaker - Ritwika Ghosh, Visiting student, Chennai Mathematical Institute (CMI) Title - On The Decidability of the First Order Theory of Reals Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

If a theory admits quantifier elimination, then there is a decision procedure for it. Tarski (1951) proved that the theory of real closed fields in the first order language of partially ordered rings(consisting of the binary predicate symbols "=" and "ï¿½ï¿½", the operations of addition, subtraction and multiplication and the constant symbols 0,1) admits quantifier elimination. We shall look at these and related results in the talk.

References

Seminar-13-01-2
 Date - 16th January 2013 Time - 03:30 PM Speaker - Srikanth Srinivasan, Dept. of Mathematics, IIT Bombay Title - The Exponential complexity of k-SAT: some classical results Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

k-SAT, the canonical NP-complete problem, is an algorithmic question of immense theoretical as well as practical relevance. Consequently, algorithms that significantly improve on brute-force search for this problem are of great interest. In this talk, we survey some exponential-time algorithms for k-SAT along with, time permitting, relations to some questions in Boolean Circuit Complexity.

References
1. Satisfiability Coding Lemma by Ramamohan Paturi, Pavel Pudlï¿½k, Francis Zane
2. A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems by Uwe Schoning
3. Worst-case upper bounds by Evgeny Dantsin and Edward A. Hirsch

Seminar-13-01-1
 Date - 9th January 2013 Time - 03:00 PM Speaker - Prof. Nutan Limaye, Dept. of CSE, IIT Bombay Title - DLOGTIME Proof Systems Venue - CFDVS Conference room, IIT Bombay.

Show Details

Abstract

Cook and Reckhow defined the notion of a proof system for a language. They defined a proof system for a language L as a polynomial time computable function f whose range is exactly L. In the past, proof systems with varying complexity of the function f have been studied. In this talk we will discuss a proof system in which the function f is computable by a deterministic log-time machine.

References
1. The Relative Efficiency of Propositional Proof Systems by Stephen A. Cook, Robert A. Reckhow. J. Symb. Log. 44(1): 36-50 (1979)
2. Verifying Proofs in Constant Depth by Olaf Beyersdorff et al. Electronic Colloquium on Computational Complexity (ECCC) 19: 79 (2012)

People
—> Principal Investigators
—> Research Employees
—> Students

Activities
—> Weekly Meetings
—> Formal Methods Update '05
—> Workshop'05
—> Workshop 2002
—> Workshop 2017

Projects
—> R & D Projects
—> Exploratory Projects

Papers/Reports
—> Papers
—> Technical Reports
—> Theses