The Complexity of Identifying Characteristic Formulae

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. 

The ICE-TCS blog

After about 14 years, ICE-TCS has finally decided to have its own blog. In the past, I have covered ICE-TCS related news here and I will continue to do so. Those posts will also appear in the centre's blog.

Have a look at the new blog if you are interested in the work we do and in the events at our little centre in Reykjavik, Iceland.

ICSE 2019 ACM SIGSOFT Distinguished Paper Award to GSSI students

I am very pleased to inform you that Emilio Cruciani and Roberto Verdecchia, two third-year PhD students in CS at the GSSI,  and their coauthors Breno Miranda and Antonia Bertolino (member of the Scientific Committee of the PhD programme in CS at the GSSI) will receive an ICSE 2019 ACM SIGSOFT Distinguished Paper Award for their paper "Scalable Approaches for Test Suite Reduction". 

 

Distinguished Papers represent the very best contributions to the ICSE Technical Track, and are awarded to up to 10% of the papers. (ICSE is the premiere annual conference in the field of software engineering and is very competitive.) This is a remarkable achievement that reflects well on the authors, on CS@GSSI and on the institute as a whole. 

Congratulations to Antonella, Breno, Emilio and Roberto, not to mention the GSSI as a whole!

EATCS Award 2019 to Thomas Henzinger

The EATCS has just announced that Thomas Henzinger is the EATCS Award 2019 recipient for "fundamental contributions to the theory and practice of formal verification and synthesis of reactive, real-time, and hybrid computer systems, and to the application of formal methods to biological systems." Congratulations to  the award committee---consisting of Artur Czumaj, Marta Kwiatkowska and Christos Papadimitriou (chair)---for their great choice, to Tom for a very well deserved award and to the TCS community at large.

Of course, Tom Henzinger needs no introduction. However, let me use this post to provide a bird's eye view of his career and of some of his many contributions to TCS, which would be enough for a good number of very successful research careers. The text below is largely due to Jean-Francois Raskin.


Biographical sketch Thomas A. Henzinger is the President of IST Austria (Institute of Science and Technology Austria), which, under his leadership, has quickly become one of the most impactful research institutes in the world. Before joining IST as its first president, Tom was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98) and Professor (1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also the Director of the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-09).

Tom is an ISI highly cited researcher and his h-index is 103, according to Google Scholar. He is a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a member of the Austrian Academy of Sciences, a Fellow of the AAAS, a Fellow of the EATCS, a Fellow of the ACM, and a Fellow of the IEEE. He was the recipient of the Milner Award of the Royal Society in 2015, of the Wittgenstein Award of the Austrian Science Fund and was granted an ERC Advanced Investigator Grant in 2010. He received the SIGPLAN POPL Most Influential Paper Award (2014), Logic in Computer Science Test-of-Time Award (2012), ACM SIGSOFT Impact Paper Award (2011), and Best Paper awards at SIGSOFT FSE and CONCUR.

Main scientific achievements Tom's research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems.

Tom has made a large number of fundamental contributions to theoretical computer science. Here I will limit myself to mentioning a small number of research areas where he has been particularly prolific and influential.

• The theory of timed and hybrid systems. Tom has defined and studied the expressiveness and the algorithmic complexity of several real-time extensions of temporal logics. He is one of the most important contributors to the theory of hybrid automata and to algorithms for the analysis of suchmodels. His papers on the subject are among the most cited ones in the field of computer-aided verification. As an example, his paper “Symbolic model checking for real-time systems” received a LICS Test-of-Time Award in 2012. He has also studied the gap that exists between mathematical models of systems (e.g. hybrid automata) and their implementation on physical hardware. To bridge this gap, he developed models of physical platforms such as Giotto and E-machines, and he devised ways to relate their semantics with the one of the abstract mathematical models.
• Games for verification and control. Tom has introduced the logic ATL*, which extends LTL and CTL* with the ability to reason about strategies that can be played by coalitions of agents/components in models of multi-agent/component systems. He has contributed to the understanding of the potential of adopting concepts from game theory for modeling and reasoning about open systems. He has contributed to a large number of algorithmic advances for solving game-graph problems and to better understand their computational complexity.
• From Boolean models to quantitative models for verification and synthesis. Tom has recently investigated how to shift from Boolean models to quantitative models. This research proposes quantitative generalizations of the paradigms that had success in reactive modeling, such as compositionality, property-preserving abstraction, model checking and synthesis. With those models, we can specify and reason about quantitative aspects, such as resource consumption, or compare the performance of different design solutions in embedded systems. He has obtained a substantial funding from the European Research Council to proceed along this promising line of research.
• Foundations of software model checking. Tom has contributed substantially to the algorithms underlying the analysis of software systems by introducing the concept of lazy abstraction. Those ideas have been implemented in the highly influential tool Blast. This line of work was honoured with the Most Influential 2004 POPL Paper Award which he received in 2014.
• Computational modelling of biological systems. Tom and his coworkers have shown that computational models are well suited to model the dynamics of biological systems. This is part of a broader research program that has the objective to show that concepts introduced to formalize reactive systems are helpful to model and reason about biological systems.

Those important theoretical contributions have always been developed with relevant practical applications in mind. Consequently, Thomas Henzinger has not only worked on the foundations of our subject, but he also transferred his theoretical ideas into practice by developing tools and by suggesting methodologies that could be used in applying his theoretical results.

Tom is a research leader who has had a profound influence on his PhD students and post-docs. To wit, several of his former students are now well-recognized researchers that enrich the life of our research community and now lead successful research groups.

Addendum 12 April 2019: In case you are interested, you can find a short interview I had with Tom Henzinger a while back here.

Guarded recursion and unique fixed points: A pill of wisdom from a recent ICE-TCS seminar

Last Tuesday, Sergey Goncharov (FAU Erlangen-Nürnberg, Germany) delivered an ICE-TCS seminar entitled Guarded traced categories for recursion and iteration. In his talk, Sergey presented recent results, based on  joint work (in progress) with Lutz Schröder and Paul Blain Levy, on axiomatizing the theory of guarded fixed points with applications to process algebra in monad-based form, where the notion of guardedness originated. 

In the classic theory of process calculi without internal actions, an equation

X = P(X) 

is guarded if each occurrence of the variable X in the expression P(X) occurs within the scope of some prefixing operator. A classic result in the theory of, for instance, Milner's Calculus of Communicating Systems is that guarded equations have unique solutions modulo bisimilarity. For instance, the equation

X = a.X 

denotes the process rec X. a.X that executes action a indefinitely. If one interprets the above equation over the complete lattice of all languages of finite words over some alphabet, then its only solution is the empty language.

I freely admit that I was under the impression that guarded equations always had unique solutions, but I was wrong. There was a point in the talk at which Sergey showed that the above equation has more than one solution over other domains. Consider, for instance, the set of languages of infinite words over the singleton alphabet {a}. There are only two such languages, namely the empty language and {a^ω}, and both are solutions to the above equation. (This is not surprising, since a-prefixing is just the identity function over this family of languages.) The same holds true when we interpret that equation over the set of all languages of finite and infinite words over some alphabet.

This is probably not news to many, but I have learnt a lesson from attending the talk myself: Guardedness does not imply uniqueness of solutions.

To the young researchers of all ages out there: Go to talks and keep an open mind. You will learn a few bits of information that you might need in your future research projects or you might clarify some misconceptions you might have had, like I did last Tuesday.