ICE-TCS Theory Day 2019

On Friday, 3 May, ICE-TCS hosted its 15th annual Theory Day. The event consisted of two 45-minute presentations by Ravi Boppana (Department of Mathematics, MIT) and Exequiel Rivas (Inria Paris - Rocquencourt, France), and three ten-minute presentations by ICE-TCS researchers highlighting some of the recent research directions pursued by members of the centre.

Ravi Boppana kicked off the Theory Day with a wonderfully paced talk on his work with Ron Holzman on Tomaszewski’s problem on randomly signed sums. The problem is as follows. Let $v_1$, $v_2$, ..., $v_n$ be real numbers whose squares add up to 1.  Consider the $2^n$ signed sums of the form $S=\sum \pm v_i$.  Can there be more signed sums whose value is greater than 1 then those whose value  is at most 1? Holzman and Kleitman (1992) proved that at least 3/8 of these sums satisfy $|S|\le 1$.  In his talk, Ravi showed us the main ideas Holzman and he used to improve the bound to 13/32.

Computational effects model the interaction of computer programs with their environment. In his talk, Exequiel Rivas taught us how monads can be used to capture computational effects (a research programme that started with Moggi's award-winning work), and then, discussed some attempts to incorporate merging operations in the monadic picture.

Two of the short talks were given by Henning A. Úlfarsson and Elli Anastasiadi. Henning described the work of his group on  a tool, called the CombSpecSearcher, that automates the methods used by combinatorialists to prove some of their theorems, The tool is able to prove results featured in dozens of research papers. Watch this space for updates on its development and for its successes!

Elli Anastasiadi, a PhD student who is already playing an important role for the centre, gave a clear seven-minute introduction to fine-grained complexity and to the notion of fine-grained reduction.

The 2019 Theory Day was well attended, at least by the standards of a TCS event in Iceland. If all goes well, we'll be back next year.

The Complexity of Identifying Characteristic Formulae

This post is reprinted from the Process Algebra Diary.

One of the classic results in concurrency theory is the Hennessy-Milner Theorem. This result states that

1. two bisimilar states in a labelled transition system satisfy exactly the same formulae in a multi-modal logic now called Hennessy-Milner logic, and 
2. two states in a labelled transition system that satisfy a mild finiteness constraint (called image finiteness)  and enjoy the same properties expressible in Hennessy-Milner logic are bisimilar.

See, for instance, Section 1.2 in these notes by Colin Stirling for an exposition of that result. A consequence of the Hennessy-Milner Theorem is that whenever two states p and q in a labelled transition system are not bisimilar, one can come up with a formula in Hennessy-Milner logic that p satisfies, but q does not. Moreover, for each state p in a finite, loop-free labelled transition systems, it is possible to construct a formula F(p) in Hennessy-Milner logic that completely characterizes p up to bisimilarity. This means that, for each state q, p is bisimilar to q if, and only if, q satisfies F(p). The formula F(p) is called a characteristic formula for p up to bisimilarity. One can obtain a similar result for states in finite labelled transition systems by extending Hennessy-Milner logic with greatest fixed points.


Characteristic formulae have a long history in concurrency theory. However, to be best of my knowledge, the complexity of determining whether a formula is characteristic had not been studied before Antonis Achilleos first addressed the problem in this conference paper. In that paper, Antonis focused on the complexity of the problem of determining whether a formula F is complete, in the sense that, for each formula G, it can derive either G or its negation.

Our recent preprint  The Complexity of Identifying Characteristic Formulae extends the results originally obtained by Antonis to a variety of modal logics, possibly including least and greatest fixed-point operators. In the paper, we show that completeness, characterization, and validity have the same complexity — with some exceptions for which there are, in general, no complete formulae. So, for most modal logics of interest, the problem is coNP-complete or PSPACE-complete, and becomes EXPTIME-complete for modal logics with fixed points. To prove our upper bounds, we present a nondeterministic procedure with an oracle for validity that combines tableaux and a test for bisimilarity, and determines whether a formula is complete.

I think that there is still a lot of work that can be done in studying this problem, with respect to a variety of other notions of equivalence considered in concurrency theory, so stay tuned for further updates. 

Two recent papers by the programming theory group at ICE-TCS

The following two papers by Tarmo Uustalu and his co-workers have recently been accepted for publication:

• H. Maarand, T. Uustalu. Certified normalization of generalized traces. Innov. in Syst. and Softw. Engin., A NASA Journal, Springer. 
• J. Espírito Santo, L. Pinto, T. Uustalu. Modal embeddings and calling paradigms. In H. Geuvers, ed., Proc. of 4th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund, June 2019), Leibniz Int. Proc. in Inf., Dagstuhl Publishing, Saarbrücken/Wadern. 

Congratulations to Tarmo and his collaborators!

Recent papers by the Algorithms Group at ICE-TCS

In keeping with its excellent track record over many years, the research group in algorithms at ICE-TCS has started 2019 with a bang. To wit, here is a list of papers by researchers at the centre in the field of algorithmics that have been recently accepted or published, in alphabetical order by author name:

• Rajiv Gandhi, Magnus M. Halldorsson, Christian Konrad, Guy Kortsarz, and Hoon Oh. Radio Aggregation Scheduling. Theoretical Computer Science, to appear.
• Magnus M. Halldorsson, Stephan Holzer, Evangelia Anna Markatou, Nancy Lynch. Leader Election in SINR Model with Arbitrary Power Control. Theoretical Computer Science, available online 23 Jan 2019.
• Magnus M. Halldorsson, Sven Koehler, Dror Rawitz. Distributed Approximation of k-Service Assignment. Distributed Computing 32(1):27--40, February 2019. 
• Magnus M. Halldorsson, Christian Konrad. Distributed Algorithms for Coloring Interval Graphs with Applications to Multicoloring Trees. Theoretical Computer Science, available online 14 Dec 2018.  
• Magnus M. Halldorsson, Tigran Tonoyan. Limitations of Current Wireless Scheduling Algorithms. Theoretical Computer Science, to appear.
• Magnus M. Halldorsson, Tigran Tonoyan. Wireless Link Capacity under Correlated Lognormal Shadowing. To appear in Proc. 17th International Symposium on Modeling and Optimization in Mobile, Ad Hoc and Wireless Networks (WiOpt 2019), June 2019. 
• Magnus M. Halldorsson, Yuexuan Wang and Dongxiao Yu. Leveraging Multiple Channels in Ad Hoc Networks. Distributed Computing, 32(2):159--172, April 2019.     
• Murilo S. de Lima, Mário C. San Felice, Orlando Lee. Group Parking Permit Problems. Discrete Applied Mathematics, to appear.  
• Murilo S. de Lima (translator), Paulo Feofiloff (original author). Graph Theory Exercises. This is a book you might find useful for your own courses in discrete mathematics and graph theory.

Congratulations to Magnús, Murilo and Tigran! Expect more in the coming months. 

Accepted journal paper on the theory of input-output conformance simulation

The paper Logical characterisations, rule formats and compositionality for input-output conformance simulation by Luca Aceto, Ignacio Fabregas, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir has been accepted for publication in the Journal of Logical and Algebraic Methods in Programming. The paper is an extended version of a conference paper that appeared in SOFSEM 2017. (See here for a longer author version of the conference paper.)

Input-output conformance simulation (iocos, for short) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans’ classic ioco relation, but has better worst-case complexity than ioco, which is PSPACE-complete, and supports stepwise refinement. The goal of the above-mentioned ICE-TCS paper is to develop the theory of iocos further by studying logical characterisations of that relation, rule formats for it and its compositionality. More specifically, that article presents Hennessy-Milner-like characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. The article also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points, and provides a precongruence rule format for iocos and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos in a compositional way for operations specified by rules in the precongruence rule format for iocos.

In a forthcoming post, I will describe the notion of characteristic formula and some of the results in a recent ICE-TCS preprint that studies the complexity of determining whether a formula expressed in a modal logic, possibly with fixed points, is characteristic for some finite LTS/Kripke structure.

Back to the future

In case anyone is interested in what ICE-TCS has been up since its inception on Friday, 29 April 2005, we have published a number of annual reports, we have a news archive going back to the birth of the centre, a list of all the guests we have hosted over the last 14 years and of the projects of ours that have received funding from competitive funding agencies. Moreover, some of the activities of the centre have been covered in posts by some of its members (see here and here, for two sister blogs, whose future entries related to ICE-TCS will be mirrored here too) and on the Bulletin of the EATCS,

Feel free to explore those resources and our, low-tech but content-rich web site.

ICE-TCS paper at POPL 2019, an A++ conference

The first post on the new ICE-TCS blog is really about something that isn't news at all, but we have to start from somewhere.

The article Adventures in monitorability: from branching to linear time and back again by Luca Aceto, Antonis Achilleos, Adrian Francalanza (University of Malta), Anna Ingólfsdóttir and Karoliina Lehtinen (University of Liverpool) was selected for the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), which was held, together with its co-located events, in Cascais, Portugal, in the period 13-19 January 2019. The annual Symposium on Principles of Programming Languages is the premier forum for the discussion of all aspects of programming languages and programming systems, and is widely regarded as an A++ conference. 

The above-mentioned ICE-TCS paper contributes to the study of runtime monitoring, an increasingly important technique for ensuring that computing systems behaves as they should when they execute, and reports on some of the research carried carried within the project TheoFoMon, supported by the Icelandic Research Fund. The POPL 2019 article establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive logic for system specification. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. We will discuss in more detail the research area to which this paper contributes and offer a bird's eye view of its contributions in a series of follow-up posts.