S Akshay (NUS, Singapore)
Approximate methods for probabilistic inference in Dynamic Bayesian Networks (Slides: PDF)
Abstract:
Probabilistic models are often used to describe the dynamics of biochemical networks. To analyze these models one must compute the probability of a state at a given time in a large Markov chain. Doing this exactly is intractable for large networks and hence succinct representations and approximate methods of computation are needed.
We consider the setting where we exploit the structure of the Markov chain to represent it succinctly as a Dynamic Bayesian Network (DBN). Now, exact analysis corresponds to performing probabilistic inference on the DBN, which is still infeasible in general. In this light, we will describe an algorithm that performs this computation approximately. We analyse the error made by the algorithm and come up with new variants where we trade-off computational speed for accuracy.
Nathalie Bertrand (INRIA)
A game approach to determinize timed automata (Slides: PDF)
Abstract:
Benedikt Bollig (LSV, ENS Cachan)
An automaton over data words that captures EMSO logic (Slides: PDF)
Abstract:
Supratik Chakraborty (IIT Bombay)
Ranking function based disambiguation techniques for Büchi automata (Slides: PDF)
Abstract:
To be announced.
Deepak D'Souza (IISc)
Conflict Tolerant Specifications for Hybrid Systems (Slides: PDF)
Abstract:
We propose a framework for developing hybrid systems that are composed of a plant with multiple controllers, each of which controls the plant intermittently in the presence of a supervisory controller. The framework is based on the notion of a "conflict-tolerant" specification for a controller, and provides a modular way of developing and reasoning about such systems. We propose a way of defining conflict-tolerant specifications using a hybrid system model. We also give a decision procedure for verifying whether a controller satisfies its conflict-tolerant specification, in the special case when the components are modeled using initialized rectangular hybrid automata.
This is joint work with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath.
Hugo Gimbert (LaBRI, Bordeaux)
Stochastic Games with Partial Observation: Decidable and Undecidable Problems (Blackboard talk)
Abstract:
Algorithmics of stochastic games with partial observation is a challenging research field, where the undecidability frontier is easily crossed. In this talk, we will survey classical and recent algorithmics and determinacy results about stochastic games with partial observation. We will especially focus on the special case of probabilistic automata and present some recent work.
Stefan Haar (INRIA/LSV, ENS Cachan)
A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata (Slides: PDF)
Abstract:
Loïc Hélouet (IRISA)
Diagnosis with Dynamic MSC Languages (Slides: PDF)
Abstract:
Manfred Kufleitner (Stuttgart)
On languages of dot-depth one over infinite words (Blackboard talk)
Abstract:
Over finite words, languages of dot-depth one are exactly those which are definable by Boolean combinations of existential first-order sentences with precicates [<,+1,min,max]. A famous result by Knast yields decidability of the membership problem for this fragment. Combining algebraic and topological properties, we show how to extend Knast's Theorem to infinite words. As a byproduct, we give a new proof of Knast's Theorem for finite words. (This is joint work with Alexander Lauser.)
Paritosh Pandya (TIFR)
Unambiguity in Timed Regular Languages: Automata, Logics and Expressiveness
Abstract:
Generalizing Schutzenberger's Unmabiguous Langauges (UL) to timed setting, we define a notion of Timed Unambiguous Languages (TUL) and explore logics and automata for these languages. A subclass of the Two-way Deterministic Timed Automata (2DTA) of Alur and Henzinger called Partially-Ordered 2DTA (or po2DTA) defines TUL. We show that these automata are boolean closed and their non-emptiness is NP-Complete. We also introduce a deterministic freeze logic TL[X,Y] which is expressively complete for po2DTA and decidable with NP-complete complexity. Finally, we compare the expressive power of several timed temporal logics. MTL[U,S] is shown to be incomparable with the Unary freeze logic TPTL[F,P]. Fragments of MTL incorporating the notions of boundedness, unary modalities and non-punctuality are shown to be expressively incomparable with each other. On the other hand, TL[X,Y] properly lies between the bounded and unbounded Unary MITL (i.e. MITL[F,P]). The LTL EF games of Etessami and Wilke are extended to MTL EF games for proving expressiveness results.
This is joint work with Simoni Shah.
Benoit Razet (TIFR)
Tracing the decision procedure for regular expressions equality (Slides: PDF)
Abstract:
In this talk we will survey the various axiomatisations for regular expressions equality. Considering the very first complete axiomatisation due to Salomaa in 1966, we will present a program (we have recently developed) which takes as input two regular expressions and outputs the precise list of axioms in order to prove the equality of the two regular expressions. This is a joint work with Bodhayan Roy.
Sylvain Salvati (LaBRI, Bordeaux)
Towards an algebraic classification of recognizable sets of lambda-terms (Slides: PDF)
Abstract:
In this talk, we will first review the notion of recognizability on the lambda-calculus and the main results that it has brought. We will then present some on-going work on the algebraic classification of recognizable sets of lambda-terms. This will be done by introducing the notion of syntactic cartesian closed category of a language of lambda-terms and show that recognizable sets of lambda-terms are defined by syntactic cartesian closed categories that are locally finite. In particular we will show that in the cases of string languages or tree languages, these syntactic cartesian closed categories allow to retrieve the usual notions of syntactic monoid or syntactic algebras. Unfortunately, we have not been able yet to prove that every language of lambda-terms having a locally finite syntactic cartesian closed category is actually recognizable. Nevertheless, the study of certain classes of syntactic cartesian closed categories may yield to a generalization of Eilenberg's variety theorem for languages that have locally finite syntactic cartesian closed categories.
Stefan Schwoon (LSV, ENS Cachan)
Towards an efficient contextual unfolder (Slides: PDF)
Abstract:
S P Suresh (CMI)
A DEXPTIME-complete Dolev-Yao theory with distributive encryption (Slides: PDF)
Abstract:
The Dolev-Yao theory is an abstract modelling of intruder capabilities in the context of security protocols. A primary component of the theory is the message deduction capabilities of the intruder, which is usually given as a proof system. The problem of deciding when a given term can be derived from a given set of terms using the proof system, called the passive intruder deduction problem, is basic to any formal analysis of security protocols. This problem is decidable in PTIME for the basic Dolev-Yao theory and many simple extensions, and the algorithm relies on a property called locality of normal proofs.
In the context of modelling cryptographic tools like blind signatures and homomorphic encryption, the Dolev-Yao model is typically extended with an operator (called blind pairing) over which encryption is distributive. We consider one such theory which lacks any obvious locality property and show that its derivability problem is hard: in fact, it is DEXPTIME-complete. The result holds also under certain variants, like when blind pairing is associative.
The results are interesting because they constitute one of the few non-trivial lower bound results for the passive intruder deduction problem. The proofs are also interesting: the upper bound proofs involve some nifty proof normalizations and an alternating automata saturation construction, while the lower bounds involve reductions from the reachability problem for alternating pushdown systems.
Tayssir Touili (LIAFA, Paris 7)
On Model Checking Multi-threaded recursive programs
Abstract:
We consider the problem of model-checking multi-threaded programs with recursive procedure calls, result passing between recursive procedures, dynamic creation of parallel processes, and synchronisation between parallel threads. To represent such programs accurately, we define a model based on rewrite systems. We consider the reachability problem of this model. This problem being undecidable, we reduce it to the computation of abstractions of the sets of execution paths of the program, and we propose a generic technique that can compute different abstractions (of different precisions and different costs) of these sets.
Hrishikesh Karmarkar (IIT Bombay)
Determinization of ω-automata unified (Slides: PDF)
Abstract:
We describe a uniform construction for converting ω-automata with arbitrary acceptance conditions (based on the notion of infinity sets i.e. the set of states visited infinitely often in a run of the automaton) to equivalent deterministic parity automata (DPW). Given a non-deterministic automaton with n states, our construction gives a DPW with at most 2O(n2 log n) states and O(n2) parity indices. The corresponding bounds when the original automaton is deterministic are O(n!) and O(n), respectively. Our algorithm gives better asymptotic bounds on the number of states and parity indices vis-a-vis the best known technique when determinizing Rabin or Streett automata with Ω{(2n) acceptance pairs, where n > 1. We demonstrate this by describing a family of Streett (and Rabin) automata with 2n non-redundant acceptance pairs, for which the best known determinization technique gives a DPW with at least Ω(2(n3) states, while our construction constructs a DRW/DPW with 2O(n2log n) states. An easy corollary of our construction is that an ω-language with Rabin index k cannot be recognized by any ω-automaton (deterministic or non-deterministic) with fewer than O(√k) states.
Soumya Paul (IMSc)
Neighbourhood structures in games (Slides: PPTX, PDF)
Abstract:
We look at concurrent-move games where the players are arranged in neighbourhoods. The neighbourhood structure is given by a graph G, the neighbourhood graph, the vertices of the which correspond to the players. The cliques in G are the neighbourhoods and the edges in G correspond to the visibility structure of the players. The game proceeds in rounds where in each round t the players of every clique X of G play a strategic form game among each other. A player at a node v strategies based on what she can observe, i.e., the strategies and the outcomes in round t-1 of the players at vertices adjacent to v. We look at simple imitative strategies for the players and consider two kinds of neighbourhood structures.
Static Neighbourhoods: The players always stick to their neighbourhoods and hence the structure of G does not change in successive rounds.
Dynamic Neighbourhoods: Here the players are allowed to switch neighbourhoods between successive rounds. Hence the neighbourhood graph might change between rounds t and t+1.
We look at simple co-ordination games on these structures and analyse what kind of behavioural patterns and neighbourhood structures eventually arise. We then look at general neighbourhood games (where the players are not obliged to play imitative strategies but different players maybe of different types and also where the payoff structure may be arbitrary) and show a characterisation result.
This is joint work with R. Ramanujam.
Ramchandra Phawade (IMSc)
A Kleene functor for a subclass of net systems (Slides: PDF)
Abstract:
Based on the early work of Conway, authors such as Elgot, Bloom and Esik, Stefanescu, showed that Kleene's theorem can be seen as a functor between the symmetric monoidal categories of finite automata and of regular expressions, which use disjoint union and the sum operation as tensor operations. The functor corresponds to the well-known algorithm with polynomially many steps from automata to regular expressions (the expressions themselves can be of exponential size), and there is also a polynomial time algorithm in the reverse direction.
Meseguer and Montanari showed that Petri nets can be seen as forming a symmetric monoidal category, with parallel composition as the tensor.
We work in a very small and well-studied subclass: that of 1-bounded T-systems (also known as marked graphs). We show that there is a functor between category of 1-bounded T-systems and corresponding category of T-expressions, which we define. The algorithm corresponding to the functor is polynomial time, and so is the algorithm in the reverse direction.
M Praveen (IMSc)
Small Vertex Cover makes Petri Net Coverability and Boundedness Easier (Slides: PDF)
Abstract:
The coverability and boundedness problems for Petri nets are known to be Expspace-complete. In an attempt to understand which instances of these problems are harder than the others, we use the framework of parameterized complexity. Given a Petri net, we associate a graph with it. With the vertex cover number k of this graph and the maximum arc weight W as parameters, we show that coverability and boundedness are in ParaPspace. This means that these problems can be solved in space O(ef(k,W)poly(n)), where ef(k,W) is some fast growing function and poly(n) is some polynomial in the size of the input. We then extend the ParaPspace result to model checking a logic that can express some generalizations of coverability and boundedness.
B Srivathsan (LaBRI, Bordeaux)
A lazy reachability algorithm for timed automata (Slides: PDF)
Abstract:
K Vasanta Lakshmi (IISc)
Verification of Requirement Specifications Using Counter Automata (Slides: PDF)
Abstract:
Yaron Velner (Tel Aviv)
Church Synthesis Problem for Noisy Input (Slides: PDF)
Abstract: