Tuesday, July 02, 2019

PhD position at TU Wirn: Formal methods applied to the specification and monitoring of large-scale, spatially-distributed, stochastic systems

Interesting PhD position at TU Wien with Ezio Bartocci and Laura Nenzi. Spread the news! 

The Institute of Computer Engineering at the Technische Universität Wien (TU Wien) is seeking a candidate for a research assistant position (PhD student, 4 years). The position is available from September (a starting date until Fall 2019 is intended) and the successful candidate will be a PhD student of the LogiCS Doctoral Program and she/he will be supervised by Prof. Ezio Bartocci <http://www.eziobartocci.com/> and co-supervised by Dr. Laura Nenzi <https://lauranenzi.github.io/>
The successful applicant will carry out his/her PhD in the research area of formal methods applied to the specification and monitoring of large-scale, spatially-distributed, stochastic systems.
The position in funded by the ÖAW and the FWF <https://m.fwf.ac.at/en/research-funding/personnel-costs/> for the recently acquired YIRG grant: “High-dimensional statistical learning: new methods to advance economic and sustainability policies”, an interdisciplinary project to be led for the TU part by PhD Laura Nenzi.
TASK DESCRIPTION (leader Laura Nenzi):
Formal methods provide precise formal specification languages that can be easily interpreted by humans and verification algorithms that can check in an automatic way the value of satisfaction of interesting properties. One of the main problems of such techniques is the curse of dimensionality. A possibility to treat the problem is to use approximate methods such as statistical model checking. However, even these methodologies can be unfeasible for very-large-scale stochastic systems. A new research line consists of exploiting machine learning techniques and Bayesian inference to identify relevant data and decrease the computational cost, permitting the application of such powerful formal analysis on very complex systems. An important aspect that will be covered in the study is the spatial configuration of such systems, a key feature in several real case studies that are considering in the project. The methodology will be principally applied to tackle questions related to sustainable urban mobility and thus responsible consumption.
Please apply your application following the instructions in the DK LogiCS admission portal. https://logic-cs.at/phd/admission/ <https://logic-cs.at/phd/admission/>, by indicating in the application form: Prof. Ezio Bartocci and Dr. Laura Nenzi as supervisors. While it is not necessary to have the Master degree at the moment of the application, it is instead mandatory to complete it before starting the PhD.
For further information and inquiries about this post please contact Laura Nenzi, e-mail: laura.nenzi@gmail.com .

Thursday, June 20, 2019

Postdoc position at the GSSI in algorithms for modern networks, formal methods for reactive systems and model-based software engineering

Postdoctoral position financed by the GSSI

Scientific profile: The successful candidate will have a strong research record in one or more of the research areas within the Computer Science group at the GSSI, namely algorithms for modern networks, formal methods for reactive systems and model-based software engineering. We welcome applications in any of those areas.

The position is for two years (renewable for a third year, if this is mutually agreeable) and the salary is 36,000€ per year before taxes.

How to apply: The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/.
Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines.

Postdoctoral position at the GSSI within the project “ALGADIMAR: Algorithms, Games, and Digital Markets”

The Computer Science group at the Gran Sasso Science Institute (GSSI, http://cs.gssi.it) --- an international PhD school and centre for advanced studies located in L’Aquila, Italy --- has one available postdoctoral position  in the context of the PRIN projects  “ALGADIMAR: Algorithms, Games, and Digital Markets” (Gianlorenzo D’Angelo, PI at GSSI), funded by the Italian Ministry for University and Research.

The position is briefly described below. It is for two years and the salary is 36,000€ per year before taxes. The position is renewable for a third year, if this is mutually agreeable.

How to apply: The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/ or write an email to Gianlorenzo D’Angelo.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines. Preference will be given to applicants who have previous research experience on topics related to the theme of the project.

Postdoctoral position within the project “ALGADIMAR: Algorithms, Games, and Digital Markets”, supervised by Gianlorenzo D’Angelo

Brief description of the project: Digital markets form an increasingly important component of the global economy. The Internet has enabled new markets with previously unknown features (e-commerce, web-based advertisement, viral marketing, sharing economy, real-time trading), and algorithms play a central role in many decision processes involved in these markets. For example, algorithms run electronic auctions, adjust prices dynamically, trade stocks, harvest big data to decide market strategies and to provide recommendations to customers. The focus of the proposal ALGADIMAR is on the development of new methods and tools in research areas that are critical to the understanding of digital markets: algorithmic game theory, market and mechanism design, machine learning, algorithmic data analysis, optimization in strategic settings. We plan to apply these methods so as to solve fundamental algorithmic problems motivated by Internet advertisement, sharing economy, mechanism design for social good, security games. While our research is focused on foundational work —with rigorous design and analysis of algorithms, mechanisms and games— it will also include empirical validation on large-scale datasets from real-world applications.

Main activities: The research activity will be on one or more of the following topics: design and analysis of algorithms; algorithms and data structures for big data; approximation algorithms; combinatorial optimization; algorithms for graphs and networks; autonomous agents and mobile computing; distributed algorithms; algorithmic game theory, algorithmic aspects of internet and social networks.

Wednesday, June 19, 2019

Postdoctoral positions at the GSSI on modelling and verification for cyber-physical and smart systems

The Computer Science group at the Gran Sasso Science Institute (GSSI, an international PhD school and centre for advanced studies located in L’Aquila, Italy) has two available postdoctoral positions on topics related to modelling and verification for cyber-physical and smart systems. The positions are in the context of two PRIN projects funded by the Italian Ministry for University and Research, namely "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty (SEDUCE)" (Catia Trubiani, PI at the GSSI) and "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" (Luca Aceto, PI at the GSSI). Each position is for two years and the salary is 36,000€ per year before taxes. The positions are renewable for a third year if this is mutually agreeable.

The positions are briefly described below. We foresee a close collaboration between the members of the teams working on the two projects. The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/ or write an email to the PIs of the respective projects.

Note that the Computer Science group at the GSSI also has a further position financed by the institute, which can be filled in any of the research themes within the group. See http://cs.gssi.it for more information.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines. Preference will be given to applicants who have previous research experience on topics related to the themes of the project.

Postdoctoral position within the project "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty", supervised by Catia Trubiani: https://cs.gssi.it/catia.trubiani.

Brief description of the project: Emerging scenarios such as autonomous vehicles and the Internet-of-Things require large-scale cyber-physical systems (CPS), i.e., computing devices that interact with the physical world. To cope with their complexity, model-based design has long been advocated as a prominent approach for their rigorous development. However, the state of the art does not adequately account for two major issues: space, to capture the distribution of CPS devices as well as their mobility; and uncertainty, e.g., to reflect lack of knowledge about the environment, the accuracy of the model, or errors occurring in the real world. Our goal is to develop modelling and analysis techniques for CPS where space and uncertainty are first-class citizens. We envisage a component-based framework where digital and physical components have locality and mobility features, and where uncertainty is captured by means of probabilistically distributed activities to describe their dynamics. We devise a system to specify spatio-temporal CPS requirements, turning them into probabilistic spatio-temporal logical specifications that will be at the basis of efficient algorithms for the analysis, verification, and synthesis. We will apply our techniques to real case studies on smart buildings and crowd-navigating robots.

Main activities: The successful candidate will develop a component-based modelling language for the specification of cyber physical systems, where digital components (i.e., the computational devices), need to co-exist with physical components (i.e., the dynamical models of the physical world). Each component will feature an appropriate location and mobility model. Uncertainty will be specified with either probabilistically distributed activities, or nondeterministically, leading to reasoning that will take into account worst- and best-case scenarios under any possible value of such uncertain actions. The modelling framework will allow the specification of spatio-temporal requirements, which establish the behavioural guarantees to be satisfied by the CPS under analysis. The postdoctoral researcher will work with Catia Trubiani at the GSSI, and she/he will also collaborate with the project partners at IMT Lucca (Mirco Tribastone, coordinator of the project), University of Trieste (Luca Bortolussi and Stefano Seriani), and University of Camerino (Francesco Tiezzi).

Postdoctoral position within the project "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" supervised by Luca Aceto: http://www.gssi.it/people/professors/lectures-computer-science/item/225-aceto-luca.

Brief description of the project: The goal of the project is the development and the application of a novel methodology for the specification, implementation and validation of trustworthy smart systems based on formal methods. We envisage system development in three steps by first providing and analysing system models to find design errors, then moving from models to executable code by translation into domain-specific programming languages and, finally, monitoring runtime execution to detect anomalous behaviours and to support systems in taking context-dependent decisions autonomously. Scientifically, the research will yield new, fundamental insights on the general properties of large scale, physically located, smart systems, leading to an end-to-end, principled approach to their design, implementation and deployment. The developed software tools and the work on the case studies will show the effectiveness of our proposed approach in three practical scenarios at different application scales.

Main activities: The successful candidate will develop runtime-monitoring and software-model-checking techniques for “smart systems”, that is, systems that take context-dependent decisions autonomously. The research activities will involve developing frameworks that can deal with the distributed nature of smart systems and will build on existing work on specification-based monitoring and software model checking of cyber-physical systems. The postdoctoral researcher will also devise techniques to use information derived from the runtime analysis to guide the software-model-checking effort and to refine the models of the runtime environment used in model checking. The postdoctoral researcher will work with Luca Aceto, Omar Inverso, Ludovico Iovino and Emilio Tuosto at the GSSI. He/she will also collaborate with the project partners at IMT Lucca, CNR Pisa, University of Camerino, University of Pisa and University of Udine. Moreover, he/she will also interact with the concurrency group at ICE-TCS (http://icetcs.ru.is/), Reykjavik University, led by Luca Aceto and Anna Ingólfsdóttir.

Sunday, May 26, 2019

An interview with Jamie Gabbay and Andrew Pitts, 2019 Alonzo Church Award recipients

The 2019 Alonzo Church Award committee consisting of Thomas Eiter, Javier Esparza, Radha Jagadeesan, Catuscia Palamidessi, and Natarajan Shankar, have selected Murdoch J. Gabbay and Andrew M. Pitts for the 2019 Alonzo Church Award, for introducing the theory of nominal representations, a powerful and elegant mathematical model for computing with data involving atomic names. In particular, the nomination for the Alonzo Church Award singled out the following two papers:
For the conference version of the first article, Andy and Jamie will also be receiving the Test-of-Time Award from LICS 1999.

The award recipients kindly agreed to answer some questions of mine via email. You can find the transcript of the interview below. My questions are labelled with LA, Andy's answers with AP and Jamie's with JG. I hope that you'll enjoy reading their insights and the story of their award-receiving work as much as I did myself.

LA: You are receiving the 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation as well as the Test-of-Time Award from LICS 1999 for your invention of nominal techniques to provide a semantic understanding of abstract syntax with binding.   Could you briefly describe the history of the ideas that led you to use the permutation model of set theory with atoms due to Fraenkel and Mostowski to represent name abstraction and fresh name generation? What were the main inspirations and motivations for your work? In your opinion, how did nominal techniques advance the state of the art at that time?

AP: I have had a long-standing interest in the mathematical semantics of programming language features that restrict resources to a specific scope, or hide information from a program's environment; think local mutable state in languages like OCaml, or channel-name restriction in the pi-calculus. When Ian Stark was doing his PhD with me in the 90s we tried to understand a simple instance: the observable properties of higher-order functions combined with dynamically generated atomic names that can be tested for equality, but don't have any other attribute -- we called this the "nu-calculus". Ian gave a denotational semantics for the nu-calculus using Moggi's monad for modelling dynamic allocation. That monad is defined on the category of pullback-preserving functors from the category of injective functions between finite ordinals to the category of sets. This functor category was well-known to me from topos theory, where it is called Schanuel's topos and hosts the generic model of a geometric theory of an infinite decidable set. A few years later, when Jamie joined me as a PhD student in 1998, I suggested we look at the Schanuel topos as a setting for initial algebra semantics of syntax involving binding operations, modulo alpha-equivalence. I think Jamie prefers set theory over category theory, so he pushed us to use another known equivalent presentation of the Schanuel topos, in terms of continuous actions of the group of permutations of the set N of natural numbers (topologized as a subspace of the product of countably many copies of N). In this form there is an obvious connection with the cumulative hierarchy of sets (with atoms) that are hereditarily finitely supported with respect to the action of permuting atoms. This universe of sets was devised by Fraenkel and Mostowski in the first part of the twentieth century to model ZFA set theory without axioms of choice. Whether one emphasises set theory or category theory, the move to making permutations of names, rather than injections between sets of names, the primary concept was very fruitful. For example, it certainly makes higher-order constructions (functions and powersets) in the topos/set-theory easier to describe and use. We ended up with a generic construction for name-abstraction modulo alpha-equivalence compatible with classical higher-order logic or set theory, so long as one abstains from unrestricted use of choice.

JG: At the time it wasn't an idea to consider names as elements of a distinctive datatype of names, with properties just like other datatypes such as the natural numbers Nat. If we want to add 1 to 1, we take 1:Nat and invoke the "plus" function, which is a specific thing associated to Nat; so why not abstract a in x by assuming a:Atm (where Atm is a distinct thing in our mathematical universe) and x:X and invoking a function "abstract", which is a thing associated to Atm? We unfolded the implications of this idea in set theory and rediscovered FM sets. I was inspired by the way I saw mathematics built up in ZF set theory as an undergraduate, starting from a simple basis and building up the cumulative hierarchy. When I saw the chance to do this for a universe with names, I jumped at the chance. It turns out FM sets are not required. Nominal techniques can be built in ZFA set theory, which contains more functions and permits unrestricted choice.

LA: Over the last fifteen years, nominal techniques have become a fundamental tool for modelling locality in computation, underlying research presented in over a hundred papers, new programming languages and models of computation. They have applications to the syntax and semantics of programming languages, to logics for machine-assisted reasoning about programming-language semantics and to the automatic verification of specifications in process calculi. Variations on nominal sets are used in automata theory over infinite alphabets, with applications to querying XML and databases, and also feature in work on models of Homotopy Type Theory. When did it dawn on you that you had succeeded in finding a very good model for name abstraction and fresh name generation, and one that would have a lot of impact? Did you imagine that your model would generate such a large amount of follow-up work, leading to a whole body of work on nominal computation theory?

AP: No, to begin with I was very focussed on getting better techniques for computing and reasoning about syntax with bound names. But that only represents a part of the current broad landscape of nominal techniques, the part that mainly depends on the mathematical notion of "finite support" (a way of expressing, via name-permutation, that an object only involves finitely many names). Independently of us, some people realised that a related notion of finiteness, "orbit-finiteness" (which expresses that an object is finite modulo symmetries) is crucial for many applications of nominal techniques. I am referring to the work of Montanari and Pistore on pi-calculus and HD automata using named sets (yet another equivalent of the Schanuel topos) and the work on automata theory over infinite alphabets (and much else besides) using "sets with atoms" by the Warsaw group (Bojanczyk, Klin, Lasota, Torunczyk,...). The latter is particularly significant because it considers groups of symmetry for atoms other than the full permutation group (in which the only property of an atom preserved under symmetry is its identity).

JG: Yes, I did. Nobody could anticipate the specific applications but I knew we were on to something, which is why I stayed on to build the field after the PhD. The amount of structure was just too striking. This showed early: e.g. in the equivariance properties, and the commutation of nominal atoms-abstraction with function-spaces. When I sent the proof of this property to Andrew, at first he didn't believe it! I had a sense that there was something deep going on and I still do.

LA: What is the result of yours on nominal techniques you are most proud of? And what are your favourite results amongst those achieved by others on nominal computation?

AP: Not so much a specific result, but rather a logical concept, the freshness quantifier (which we wrote using an upside down "N" -- N stands for "New"). In informal practice when reasoning about syntax involving binders, one often chooses some fresh name for the bound variable, but then has to revise that choice in view of later ones; but fortunately any fresh name does as well as some particular one. This distinctive "some/any" property occurs all over the place when computing and reasoning about languages with binders and the freshness quantifier formalises it, in terms of the freshness ("not in the support of") relation and conventional quantifiers. For the second part of your question I would choose two things. One is the work by Jamie with Fernandez and Mackie on nominalrewriting systems, which won the PPDP Most Influential Paper 10-year Award in 2014. The second is the characterisation of orbit-finite sets with atoms in terms of "set-builder expressions"---see Klin et al, "Locally Finite Constraint Satisfaction Problems", Proc. LICS 2015); it's a nice application of the classical model theory of homogeneous structures with interesting applications for languages that compute with finite structures.

JG: Thanks for asking. Aside from the initial papers, my work on nominal rewriting with Fernandez has probably had most impact. However, I am rather fond of the thread of research going from Nominal Algebra, through the axiomatisation of substitution and first-order logic and the characterisation of quantification as a limit in nominal sets, and on to Stone duality. It's a mathematical foundation built from a nominal perspective of naming and quantification and I hope that as the state of the art in nominal techniques advances and broadens, it might prove useful. Andrew's book has been helpful in marking out nominal techniques as a field. I also agree with Andrew that orbit-finiteness and the applications of this idea to transition systems and automata, is important. I like the automata work for another concrete reason: nominal techniques were discovered in the context of names and binding in syntax, which has bequeathed a misconception that nominal techniques are only about this. The Warsaw school of nominal techniques gives an independent illustration of the other applications of these ideas.

LA: Twenty years have passed since your LICS 1999 paper and the literature on variations on nominal techniques now contains over a hundred papers. Do you expect any further development related to the theory and application of nominal techniques in the coming years? What advice would you give to a PhD student who is interested in working on topics related to nominal computation today?

AP: For the purpose of answering your question, let's agree to divide LICS topics into Programming Languages and Semantics (PLS) versus Logic and Algorithms (LAS). (So long as we don't think of it as a dichotomy!) Then it seems to me that applications of nominal techniques to LAS are currently in the ascendant and show no sign of slowing down. My own interests are with PLS and there is still work to be done there. In particular, I would like better support for using nominal techniques within the mainstream interactive theorem proving systems: we have the Nominal Package of Urban and Berghofer for classical higher-order logic within Isabelle (which lead to Urban and Tasson winning the CADE Skolem Award in 2015), but nothing analogous for systems based on dependent type theory, such as Agda, Coq and Lean. Recent work of Swan (arXiv:1702.01556) gives us a better understanding of how to develop nominal sets within constructive logic; but I have yet to see a dependent type theory that both corresponds to some form of constructive nominal logic under Curry-Howard and is sufficiently simple that it appeals to users of systems lke Coq who want to mechanise programming language meta-theory in a nameful style. Really, I would like the utility of the FreshML programming language that Jamie, Mark Shinwell and I proposed in 2003 (and which Mark implemented as a patch of OCaml) restricted to total functional programming in the style of Agda; but I don't quite know how to achieve that.

JG: Yes. We are far from understanding nominal techniques and the field has a lot of life and will continue to surprise. I've always believed that. A key sticking-point right now is implementations. I wrote a paper about this recently, on equivariance and the foundations of nominal techniques. One point in the paper is a sketch for a next-generation nominal theorem-prover (based on ZFA + equivariance). I'd like to see this carried out, so if anybody reading this is interested then please be in touch. I'd also like to see nominal techniques implemented as a package in a language like Haskell, ML, or even Python! If we can get this stuff into the working programmer's toolbox, in a way that just works and does not require special configuration, then that would be helpful. I suspect that nominal techniques as currently presented in the maths papers, might not fit into a programming language at the moment. The theory is too strong and may need weakened first. We need a subset of nominal techniques weak enough to squeeze into an existing language, yet expressive enough for interesting applications. Some general advice, specifically for the PhD student. If you have an idea which most people around you don't understand, consider this may be a gap in the collective imagination. There can be peer pressure when faced by incomprehension to blame yourself, back down, and think about something else. By all means do this, but only if you yourself judge it right to do so.

LA: Is there any general research-related lesson you have learnt in the process of working on nominal techniques?

AP: On the one hand, don't lose sight of what application your theory is supposed to be good for; but on the other hand, let beauty and simplicity be your guide.

JG: Yes:
  • Proving stuff is 30% of the work; convincing people is 70%. 
  • It's the basic ideas that are hard, not the complicated theorems.
  • Competence and imagination are orthogonal. 
  • It's doesn't have to be complex to be clever. 
  • Elegant + applicable is a potent combination. 
  • Seek out good listeners. Give up quickly on bad ones. Try to be a good listener. 
  • Other people have a lot to teach you, but it might not be the things you expected. 
  • Writing papers is fun.  
LA: Thanks to both of you for your willingness to answer my questions and congratulations for the awards you will be receiving this summer!

Sunday, May 12, 2019

ICE-TCS Theory Day 2019

This post also appears on the ICE-TCS blog.

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 , , ..., be real numbers whose squares add up to 1.  Consider the signed sums of the form .  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 .  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.

Thursday, April 18, 2019

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. 

Saturday, April 13, 2019

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!

Thursday, April 11, 2019

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.

Thursday, April 04, 2019

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.

Thursday, March 14, 2019

Seven PhD positions in CS at the GSSI

This call for PhD positions might be of interest to some of your students or you. Please distribute it as you see fit. 

The GSSI - Gran Sasso Science Institute offers seven PhD fellowships in Computer Science for the academic year 2019/20. One of those positions is earmarked for the development of efficient techniques and tools for the analysis of large genomic data and is supported by the genomic-research start-up Dante Labs srl. The official language for all PhD courses is English.

The fellowships are awarded for 4 years and their yearly amount is € 16.159,91 gross. All PhD students have free accommodation at the GSSI facilities and use of the canteen.

The application must be submitted through the online form available here by 18 June 2019 at 6 pm (Italian time zone). 

 The GSSI-Gran Sasso Science Institute is an international PhD school and a center for research and higher education in the areas of Physics, Mathematics, Computer Science and Social Sciences. Founded in 2012 in L’Aquila (Italy) as Center for Advanced Studies of the National Institute for Nuclear Physics (INFN) and then established in March 2016 as a School of Advanced Studies providing post-graduate education. Through a day-to-day collaboration and interaction, researchers and students have the opportunity to build a sound knowledge of the research methods and to experiment contamination of interests, innovative approaches and multicultural exchanges in all the GSSI activities. In addressing the complexity of today’s world, GSSI is committed to removing all barriers between its areas of study and research. The dissemination of scientific results towards society and the promotion of cultural events for generic public, citizens and schools are among GSSI goals.

See here for further details. 

Fully-funded four-year PhD scholarships at IMT Lucca

IMT School for Advanced Studies Lucca invites applications for PhD
positions in the Systems Science program, and specifically for its Computer
Science and Systems Engineering

We carry out foundational, applied, and interdisciplinary research on the
modeling and analysis of systems, broadly construed. The SYSMA
<http://sysma.imtlucca.it/> research unit welcomes applications from
candidates in Computer Science with an interest in any of the following

- cloud computing;

- computational methods for the analysis of cyber-physical systems;

- cybersecurity;

- modeling and verification of concurrent, distributed, and self-adaptive

- program analysis;

- smart contracts and blockchain technology;

- software performance evaluation.

A non-exhaustive list of suggested PhD topics is available here
<https://sysma.imtlucca.it/phd/phd-projects/>. Prospective candidates are
warmly encouraged to get in touch with members
<https://sysma.imtlucca.it/people/> of the SYSMA unit for informal

The scholarship is for 4 years and consists of grant amounting to € 15,300
gross/year, in addition to free accommodation and board at the IMT Campus
<https://www.imtlucca.it/en/campus/overview>. PhD candidates have the
possibility to defend their thesis from the beginning of the fourth year of
the program, but no earlier as per Italian legislation.

The initial start date of the PhD program is 1 November 2019. The working
language at IMT is English.

Application deadline is 23 April 2019. Note that candidates who have not
obtained their undergraduate degree by the deadline can still apply, and
can be admitted if they graduate no later than 31 October 2019.

Applications must be submitted through the online form at:


Tuesday, March 05, 2019

SIROCCO 2019 - Second Call for Papers

Michele Flammini, PC co-chair of this year's SIROCCO conference, asked me to post the second CFP for that event. Submit your paper and win a trip to the Abruzzo region this summer! (In case you need them, here are ten reasons why you should. In my biased opinion, there are many more.)

SIROCCO 2019 - Second Call for Papers
26th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2019)
July 1-4, 2019, L’Aquila, Italy
OVERVIEW. SIROCCO is devoted to the study of the interplay between structural knowledge, communication, and computing in decentralized systems of multiple communicating entities. Special emphasis is given to innovative approaches leading to better understanding of the relationship between computing and communication. SIROCCO has a tradition of interesting and productive scientific meetings in a relaxed and pleasant atmosphere, attracting leading researchers in a variety of fields in which communication and knowledge play a significant role. This year, SIROCCO will be held in L’Aquila, a beautiful historical city in the mountain side, 100km away from Rome.
SCOPE. Original papers are solicited from all areas of study of local structural knowledge, global communication, and computational complexities. Among the typical areas are distributed computing, communication networks, game theory, parallel computing, social networks, mobile computing (including autonomous robots), peer to peer systems, communication complexity, fault tolerant graphs, and probability in networks. Keeping up with the tradition of SIROCCO, new areas are always welcome.
SUBMISSIONS. Papers are to be submitted electronically through EasyChair at the following link: https://easychair.org/conferences/?conf=sirocco2019.
Authors are invited to submit their work in one of the two acceptable formats: regular papers and brief announcements. First, abstracts should be registered and later the full papers are due. A regular submission must report on original research and must contain results that have not previously appeared, and have not been concurrently submitted to a journal or a conference with published proceedings. It must be no longer than 12 single-column pages on letter-size paper using at least 11-point font, including tables and references. Up to 4 additional pages of figures may be included with the submission. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. Full Proofs omitted for lack of space should appear in an appendix.
A submission for a brief announcement must be no longer than 3 single-column pages on letter-size paper using at least 11-point font. The title of a submission for a brief announcement must begin with “Brief announcement:”. Such submissions may describe work in progress or work presented elsewhere. A submission that is not selected for regular presentation may be invited for a brief announcement.
PUBLICATION. Regular papers and brief announcements will be included in the conference proceedings that will be published by Springer. Regular papers receive up to 15 pages, brief announcements receive up to 2 LNCS-style pages.
BEST STUDENT PAPER AWARD. A prize will be given to the best student regular paper. A paper is eligible if at least one author is a full-time student at the time of submission, and the contribution of the student is significant. This must be noted on the cover page. The program committee may decline to give the award or may split it.
Susanne Albers, TU München, Germany
Pierre Fraigniaud, CNRS and University Paris Diderot, France
Stefano Leonardi, Sapienza University of Rome, Italy
Merav Parter, Weizmann Institute of Science, Israel
SIROCCO 2019 will also feature a talk by Paola Flocchini, University of Ottawa, Canada – Recipient of the 2019 Prize for Innovation in Distributed Computing
KEY DATES (all in 2019)
Abstract registration: April 1
Full paper submission: April 7
SIROCCO notification: May 17
Proceedings version: TBD
Early registration: June 1
Dan Alistarh, IST Austria, Austria
James Aspnes, Yale University, USA
Alkida Balliu, Aalto University, Finland
Vittorio Bilò, University of Salento, Italy
Lelia Blin, Sorbonne University, France
Ioannis Caragiannis, University of Patras, Greece
Keren Censor-Hillel, Technion, Israel (co-chair)
Michele Flammini, GSSI & University of L’Aquila, Italy (co-chair)
Luisa Gargano, University of Salerno, Italy
Chryssis Georgiou, University of Cyprus, Cyprus
Magnús Halldórsson, Reykjavik University, Iceland
Tomasz Jurdzinski, University of Wroclaw, Poland
Fabian Kuhn, University of Freiburg, Germany
Toshimitsu Masuzawa, Osaka University, Japan
Alessia Milani, University of Bordeaux, France
Ivan Rapaport, Universidad de Chile, Chile
Dror Rawitz, Bar-Ilan University, Israel
Mordechai Shalom, Tel-Hai College, Israel
Jennifer Welch, Texas A&M University, USA
Prudence W.H. Wong, University of Liverpool, UK
Yukiko Yamauchi, Kyushu University, Japan
Guido Proietti, University of L'Aquila, Italy (chair)
Gianlorenzo D’Angelo, GSSI, Italy
Mattia D’Emidio, University of L'Aquila, Italy
Michele Flammini, GSSI & University of L'Aquila, Italy
Luciano Gualà, University of Rome Tor Vergata, Italy
Ludovico Iovino, GSSI, Italy
Cosimo Vinci, University of L'Aquila, Italy
Shantanu Das, Aix-Marseille University, France
Rastislav Kralovic, Comenius University, Slovakia
Zvi Lotker, Ben Gurion University, Israel
Boaz Patt-Shamir, Tel Aviv University, Israel
Andrzej Pelc, University of Québec, Canada
Nicola Santoro, Carleton University, Canada
Sebastien Tixeuil, University Paris 6, France
Jukka Suomela, Aalto University, Finland