Registration

Speaker: Prakash Saivasan

Title: Satisfiability of String Constraints with Sub-word Ordering 

Abstract:  In this talk, we will consider constraints over the domain of finite strings. Constraint system typically involve relational constraints and membership constraints. In our setting, we consider sub-word relation for relating the variables. We will study the satisfiability problem for such constraint systems. While the problem in full generality is undecidable, we will consider an acyclic fragment of it and show decidability. We show that the problem is uniformly NExptime-complete when regular or context free languages are involved in the membership constraints. We will further establish a close connection between this problem and reachability in certain kinds of lossy channel systems.  

SLIDES

Tea Break

Speaker: Kartik Nagar

Title: Certified Mergeable Replicated Data Types

Abstract: Replicated data types (RDTs) are data structures that permit concurrent modification of multiple, potentially geo-distributed replicas without coordination between them. RDTs are designed in such a way that conflicting operations are eventually deterministically reconciled ensuring that all replicas converge to the same state. Constructing correct RDTs remains a difficult endeavour due to the complexity of reasoning about independently evolving states of the replicas. With the focus on the correctness of RDTs (and rightly so), existing approaches to RDTs are less efficient compared to their sequential counterparts in terms of the time and space complexity of local operations. This is unfortunate since RDTs are often used in a local-first setting where the local operations far outweigh remote communication.

In this talk, I will present Peepul, a pragmatic approach to building and verifying efficient RDTs. To make reasoning about correctness easier, we cast RDTs in the mould of the distributed version control system, and equip it with a three-way merge function for reconciling conflicting versions. Further, we go beyond just verifying convergence, and provide a methodology to verify arbitrarily complex specifications. We develop a replication-aware simulation relation to relate RDT specifications to their efficient purely functional implementations. We implement Peepul as an F* library that discharges proof obligations to an SMT solver. The verified efficient RDTs are extracted as OCaml code and used in Irmin, a distributed database built on the principles of Git.

This talk is based on a joint work with Vimala S, Adharsh Kamath and KC Sivaramakrishnan, published in PLDI 2022.

SLIDES

Tea Break

Speaker: C. Aiswarya

Title:   Deciding Conjugacy of a Rational Relation 

Abstract:  The study of rational relations is fundamental to the study of formal languages and automata theory. A rational relation is conjugate if each pair of words in the relation is conjugate (or cyclic shifts of each other). The notion of conjugacy has been central in addressing many important algorithmic questions about rational relations. We address the problem of checking whether a rational relation is conjugate and show that it is decidable.

Towards our decision procedure, we establish a new result that is of independent interest to word combinatorics. We identify a necessary and sufficient condition for the set of pairs given by $(\alpha_0,\beta_0) G_1^* (\alpha_1,\beta_1) \cdots G_k^*(\alpha_k,\beta_k), k \geq 0$ to be conjugate, where $G_i$ is a (not necessarily rational) conjugate relation  and $\alpha_i, \beta_i$ are arbitrary words. This is similar to, and a nontrivial generalisation of,  a characterisation given by Lyndon and Sch\"utzenberger in 1962 for the conjugacy of a pair of words. 

Furthermore, our condition can be evaluated in polynomial time, yielding a PTIME procedure for deciding the conjugacy of a rational relation given as a sumfree expression. Since any arbitrary rational expression can be expressed as a sum of sumfree expressions (with an exponential blow-up), decidability of conjugacy of rational relations follows. 

If time permits, we will also explore some applications to in approximate comparisons between transducers, for instance computing the edit distance between two transducers. 

Based on joint work with Amaldev Manuel and Saina Sunny. 

SLIDES

Lunch

Speaker: Purbita Jana

Title: Geometric Logic: Generalizations and its Applications 

Abstract:  We will delve into the idea of geometric logic and its extensions. It is well known that the propositional fragment of geometric logic (also known as the logic of finite observations) is nothing but the logic of affirmative assertions. Recall that an assertion is affirmative if and only if the assertion is true precisely in the circumstances where it can be affirmed. Note that we need to do the job in finite time, a finite amount of work and based on what we can observe. If we wish to make the idea of the logic of affirmative assertions closer to real-life situations then discussing the validity (truth value) of affirmative assertions up to some extent is a better idea, instead of, whether affirmative assertions are valid (true) or not valid (false). To address this issue we need to concentrate on the notion of valuation function. Generalizations in this direction can be used to interpret scenarios where the truth values are not comparable. In our previous work, we have already shown how the extension of the 3-valued logic of finite observations can be seen as the stepping stone to propose the logic of ethics. We will discuss this in detail. Moreover, if time permits, we will discuss how this study enhances the results of M. J. Healy for the LAPART architecture. 

SLIDES

Tea Break

Speaker: Malvin Gattinger

Topic: Symbolic Model Checking Dynamic Epistemic Logic - theory, practice and perspectives

Abstract: Recent work in Epistemic Planning uses Dynamic Epistemic Logic to solve multi-agent planning problems. For this, it is often necessary to compute perspective shifts to let agents take into account the knowledge of others. These perspective shifts are usually defined on explicit Kripke models which may grow exponentially.

After introducing the general idea of symbolic model checking for DEL, this talk will discuss methods to compute these perspective shifts without explicit Kripke models. Concretely, we define perspective shifting on symbolic structures and succinct models. Time permitting, we will also show how symbolic 

perspective shifting is implemented in the SMCDEL implementation in Haskell.

Lastly, we will report on ongoing work where we compare the so-called symbolic and succinct models for DEL to each other. 

SLIDES

High Tea

Closing Discussion with Students