tag:blogger.com,1999:blog-277056612022-09-24T07:59:09.991+00:00Process Algebra DiaryPapers I find interesting---mostly, but not solely, in Process Algebra---, and some fun stuff in Mathematics and Computer Science at large and on general issues related to research, teaching and academic life.Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.comBlogger733125tag:blogger.com,1999:blog-27705661.post-37996019823942567412022-09-19T16:58:00.002+00:002022-09-19T16:58:46.242+00:00Dean of the School of Technology at Reykjavik University: Call for applications<p>Reykjavik University is looking for a new dean of the School of Technology, which comprises the Department of Applied Engineering, the Department of Computer Science, and the Department of Engineering. </p><p>If you have a strong academic career, a vision of how our school can improve its standing and impact, and would enjoy living in Iceland, I encourage you to consider this opportunity! See the ad at the link below for more information: </p><p><a href="https://jobs.50skills.com/ru/en/15613">https://jobs.50skills.com/ru/en/15613</a> </p><p>Spread the news through your network and encourage excellent candidates to apply.</p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-55313942383468886872022-08-10T13:55:00.003+00:002022-08-10T13:55:39.204+00:00CONCUR through time: A data- and graph-mining analysis<p>The <a href="https://concur2022.mimuw.edu.pl/" target="_blank">33rd edition of the International Conference on Concurrency Theory (CONCUR</a>) will be held in Warsaw, Poland, in the period 16–19 September 2022. The first CONCUR conference dates back to 1990 and was one of the conferences organized as part of the two-year <a href="https://pure.tue.nl/ws/portalfiles/portal/4345371/589768.pdf" target="_blank">ESPRIT Basic Research Action 3006</a> with the same name. The CONCUR community has run the conference ever since and established the <a href="https://concurrency-theory.org/organizations/ifip" target="_blank">IFIP WG 1.8 “Concurrency Theory”</a> in 2005 under Technical Committee TC1 Foundations of Computer Science of IFIP1.</p><p>In light of the well-established nature of the CONCUR conference, and spurred by a <a href="https://slides.com/piluc/icalp-50?token=fl3BBJ8j" target="_blank">data-and graph-mining comparative analysis</a> carried out by Pierluigi Crescenzi and three of his students to celebrate the 50th anniversary of ICALP, Pierluigi and I undertook a similar study for the CONCUR conference using some, by now classic, tools from network science. Our goal was to try and understand the evolution of the CONCUR conference throughout its history, the ebb and flow in the popularity of some research areas in concurrency theory, and the centrality of CONCUR authors, as measured by several metrics from network science, amongst other topics. </p><p>Our article available <a href="http://www.icetcs.ru.is/luca/CONCUR.pdf" target="_blank">here</a> reports on our findings. We hope that members of the CONCUR community will enjoy reading it and playing with the web-based resources that accompany this piece. It goes without saying that the data analysis we present has to be taken with a huge pinch of salt and is only meant to provide an overview of the evolution of CONCUR and to be food for thought for the concurrency theory community. <br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-12168542549386844182022-08-09T12:17:00.012+00:002022-08-19T11:02:15.691+00:00Interview with Franck Cassez and Kim G. Larsen, CONCUR 2022 ToT Award Recipients<p class="MsoNormal">This post is devoted to an interview with <a href="https://homes.cs.aau.dk/~kgl/" target="_blank">Kim G. Larsen</a>, who received the <a href="https://concur2022.mimuw.edu.pl/tot-award/" target="_blank">CONCUR 2022 Test-of-Time Award</a> for the paper <a href="https://link.springer.com/content/pdf/10.1007/3-540-44618-4_12.pdf" target="_blank">The Impressive Power of Stopwatches</a> (available also <a href="https://www.researchgate.net/publication/220701029_The_Impressive_Power_of_Stopwatches" target="_blank">here</a>), which appeared at CONCUR 2000 and was co-authored with <a href="https://franck44.github.io/" target="_blank">Franck Cassez</a>. On behalf of the concurrency theory community, I thank Kim for taking the time to answer my questions. I trust that readers of this blog will enjoy reading Kim's answer as much as I did. <span class="im"></span></p><p class="MsoNormal"><b><span lang="EN-US">Luca</span></b><span lang="EN-US">: You receive the CONCUR ToT Award 2022 for your paper The Impressive Power of Stopwatches, which appeared at CONCUR 2000. </span>In that article, you showed that timed automata enriched with stopwatches and unobservable time delays have the same expressive power of linear hybrid automata. Could you briefly explain to our readers what timed automata with stopwatches are? Could you also tell us how you came to study the question addressed in your award-winning article? Which of the results in your paper did you find most surprising or challenging?</p><p class="MsoNormal"><b>Kim:</b> <span class="im"></span><span lang="EN-US">Well, in timed automata all clocks grow with rate 1 in all locations of the automata. Thus you can tell the amount of time that has elapsed since a particular clock was last reset, e.g. due to an external event of interest. A stopwatch is a real-valued variable similar to a regular clock. In contrast to a clock, a stopwatch will in certain locations grow with rate 1 and in other locations grow with rate 0, i.e. it is stopped. As such, a stopwatch gives you information about the accumulated time spent in a certain parts of the automata. </span></p><p></p><p class="MsoNormal"><span lang="EN-US"></span><span lang="EN-US">In modelling schedulability problems for real-time systems, the use of stopwatches is crucial in order to adequately capture preemption. I definitely believe that it was our shared interest in schedulability that brought us to study timed automata with stopwatches. We knew from earlier results by Alur et al. that properties such as reachability was undecidable. But what could we do about this? And how much expressive power would the addition of stopwatches provide?</span></p><p class="MsoNormal"><span lang="EN-US"></span><span lang="EN-US">In the paper we certainly put the most emphasis on the latter question, in that we showed that stopwatch automata and linear hybrid automata accept the same class of timed languages, and this was at least for me the most surprising and challenging result. However, focusing on impact, I think the approximate zone-based method that we apply in the paper has been extremely important from the point of view of having our verification tool <a href="https://uppaal.org/" target="_blank">UPPAAL</a> being taken-up at large by the embedded systems community. It has been really interesting to see how well the over-approximation method actually works.</span><span class="im"></span></p><span class="im"><p class="MsoNormal"><b><span lang="EN-US">Luca</span></b><span lang="EN-US">: In your article, you showed that linear hybrid automata and stopwatch automata accept the same class of timed languages. </span>Would this result still hold if all delays were observable? Do the two models have the same expressive power with respect to finer notions of equivalence such as timed bisimilarity, say? Did you, or any other colleague, study that problem, assuming that it is an interesting one?</p><p class="MsoNormal"><b>Kim:</b> <span class="im"></span><span lang="EN-US">These are definitely very interesting questions, and should be studied. As for finer notions of equivalences – e.g. timed bisimilarity – I believe that our translation could be shown to be correct up to some timed variant of chunk-by-chunk simulation introduced by Anders Gammelgaard in his <a href="https://tidsskrift.dk/daimipb/article/view/6611/5733" target="_blank">Licentiat Thesis</a> from Aarhus University in 1991. That could be a good starting point<b>.</b></span><span class="im"></span><span class="im"></span></p></span><span class="im"><p class="MsoNormal"><span lang="EN-US"><br /><b>Luca</b>: Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? </span>Which of your subsequent results on timed and hybrid automata do you like best? Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising?<br /></p><p class="MsoNormal"><b>Kim: </b> <span lang="EN-US">Looking up in <a href="https://dblp.org/pid/l/KimGuldstrandLarsen.html" target="_blank">DBLP,</a> I see that I have some 28 papers containing the word “scheduling”. For sure stopwatches will have been used in one way or another in these. One thing that we never really examined thoroughly is to investigate how well the approximate zone-based will worked when applied to the translation of linear hybrid automata through the translation to stopwatch automata. This would definitely be interesting to find out. </span></p></span> <span class="im"></span><p class="MsoNormal"><span lang="EN-US">This was the first joint publication between me and Franck. </span><span lang="EN-US">I enjoyed fully the collaboration on all the next 10 joint papers. Here the most significant ones are probably the <a href="https://doi.org/10.1007/11539452_9" target="_blank">paper at CONCUR 2005</a>, where we presented the symbolic on-the-fly algorithms for synthesis for timed games and the branch UPPAAL TIGA. And later in a European project GASICS with Jean-Francois Raskin, we used the TIGA in the synthesis of optimal and robust control of a hydraulic system.</span></p><p class="MsoNormal"><b>Franck:</b> Using the result in our paper, we can analyse scheduling problems where tasks can be stopped and restarted, using real-time model-checking and a tool like UPPAAL.</p><p class="MsoNormal"><br />To do so, we build a network of stopwatch automata modelling the set of tasks and a scheduling policy, and reduce schedulability to a safety verification problem: avoid reaching states where tasks do not meet their deadlines. Because we over-approximate the state space, our analysis may yield some false positives and may wrongly declare a set of tasks non-schedulable because the over-approximation is too coarse. </p><p class="MsoNormal">In the period 2003–2005, in cooperation with Francois Laroussinie we tried to identify some classes of stopwatch automata for which the over-approximation does not generate false positives. We never managed to find an interesting subclass. </p><p class="MsoNormal">This may look like a serious problem in terms of applicability of our result, but in practice, it does not matter too much. Most of the time, we are interested in the schedulability of a specific set of tasks (e.g. controlling a plant, a car, etc.) and for these instances, we can use our result: if we have false positives, we can refine the model tasks and scheduler and rule them out. Hopefully after a few iterations of refinement, we can prove that the set of tasks is schedulable.</p><p class="MsoNormal">The <span class="im">subsequent result on timed and hybrid automata of mine </span> that I probably like best is the one we obtained on solving optimal reachability in timed automata. <br />We had a <a href="https://www.labri.fr/perso/fleury/publications/BCFL-fsttcs04.pdf" target="_blank">paper at FSTTCS in 2004</a> presenting the theoretical results, and a <a href="https://doi.org/10.1016/j.entcs.2004.07.006" target="_blank">companion paper at GDV 2004</a> with an implementation using HyTech, a tool for analysing hybrid automata. <br /></p><p class="MsoNormal">I like these results because we ended up with a rather simple proof, after 3-4 years working on this hard problem. </p><span class="im"> <p class="MsoNormal"><b><span lang="EN-US">Luca</span></b><span lang="EN-US">: Could you tell us how you started your collaboration on the award-winning paper? I recall that Franck was a regular visitor to our department at Aalborg University for some time, but I can't recall how his collaboration with the Uppaal group started. </span></p><p class="MsoNormal"><span lang="EN-US"><b>Kim:</b> </span><span class="im"></span><b><span lang="EN-US"></span></b><span lang="EN-US">I am not quite sure I remember how and when I first met Franck. For some time we already worked substantially with French researchers, in particular from LSV Cachan (Francois Larroussinie and Patricia Bouyer). I have the feeling that there were quite some strong links between Nantes (were Franck was) and LSV on timed systems in those days. Also Nantes was the organizer of the PhD school MOVEP five times in the period 1994-2002, and I was lecturing there in one of the years, meeting Olivier Roux and Franck who were the organizers. Funny enough, this year we are organizing <a href="https://movep2022.cs.aau.dk/" target="_blank">MOVEP</a> in Aalborg. Anyway, at some point Franck became a regular visitor to Aalborg, often for long periods of time – playing on the Squash team of the city when he was not working.</span><span class="im"></span><span class="im"></span><span lang="EN-US"></span></p><p class="MsoNormal"><span lang="EN-US"><b>Franck:</b> As Kim mentioned, I was in Nantes at that time, but I was working with Francois Laroussinie who was in Cachan. Francois had spent some time in Aalborg working with Kim and his group and he helped organise a mini workshop with Kim in 1999, in Nantes. That’s when Kim invited me to spend some time in Aalborg, and I visited Aalborg University for the first time from October 1999 until December 1999. This is when we worked on the stopwatch automata paper. We wanted to use UPPAAL to verify systems beyond timed automata. </span></p><p class="MsoNormal"><span lang="EN-US">I visited Kim and his group almost every year from 1999 until 2007, when I moved to Australia. There were always lots of visitors at Aalborg University and I was very fortunate to be there and learn from the Masters. <br /><br />I always felt at home at Aalborg University, and loved all my visits there. The only downside was that I never managed to defeat Kim at badminton. I thought it was a gear issue, but Kim gave me his racket (I still have it) and the score did not change much.</span></p><p class="MsoNormal"><span lang="EN-US"><br /><b>Luca</b>: What are the research topics that you find most interesting right now? </span>Is there any specific problem in your current field of interest that you'd like to see solved?</p></span><span class="im"><p class="MsoNormal"><b>Kim:</b> <span class="im"></span><span lang="EN-US">Currently I am spending quite some time on marrying symbolic synthesis with reinforcement learning for Timed Markov Decision Processes in order to achieve optimal as well as safe strategies for Cyber-Physical Systems.</span><span class="im"></span><span class="im"></span><span lang="EN-US"></span></p><p class="MsoNormal"><span lang="EN-US"><br /><b>Luca</b>: Both Franck and you have a very strong track record in developing theoretical results and in applying them to real-life problems. </span>In my, admittedly biased, opinion, your work exemplifies Ben Schneiderman's Twin-Win Model (<a data-saferedirecturl="https://www.google.com/url?q=https://www.pnas.org/doi/pdf/10.1073/pnas.1802918115&source=gmail&ust=1660131834210000&usg=AOvVaw3C8MqXrhHOcBM8hIz-QekT" href="https://www.pnas.org/doi/pdf/10.1073/pnas.1802918115" target="_blank">https://www.pnas.org/doi/pdf/<wbr></wbr>10.1073/pnas.1802918115</a>), which propounds the pursuit of "the dual goals of breakthrough theories in published papers and validated solutions that are ready for widespread dissemination." Could you say a few words on your research philosophy? </p></span><span class="im"><p class="MsoNormal"><b>Kim:</b> <span class="im"></span><span lang="EN-US">I completely subscribe to this. Several early theoretically findings – as the paper on stopwatch automata – have been key in our sustainable transfer to industry.</span><span class="im"></span><span class="im"></span><span lang="EN-US"></span></p><p class="MsoNormal"><span lang="EN-US"><b>Franck:</b> Kim has been a mentor to me for a number of years now, and I certainly learned this approach/philosophy from him and his group. <br /> </span></p><p class="MsoNormal"><span lang="EN-US">We always started from a concrete problem, e.g. scheduling tasks/checking schedulability, and to validate the solutions, building a tool to demonstrate applicability. The next step was to improve the tool to solve larger and larger problems.</span></p><p class="MsoNormal"><span lang="EN-US"><br />UPPAAL is a fantastic example of this philosophy: the reachability problem for timed automata is PSPACE-complete. That would deter a number of people to try and build tools to solve this problem. But with smart abstractions, algorithms and data-structures, and constant improvement over a number of years, UPPAAL can analyse very large and complex systems. It is amazing to see how UPPAAL is used in several areas from traffic control to planning and to precisely guiding a needle for an injection. </span></p><p class="MsoNormal"><span lang="EN-US"><br /><b>Luca</b>: What advice would you give to a young researcher who is keen to start working on topics related to formal methods? </span></p></span><span class="im"> </span><p class="MsoNormal"><b><span lang="EN-US">Kim: </span></b><span lang="EN-US">Come to Aalborg, and participate in year's MOVEP.</span></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-47441189802996070802022-07-29T16:29:00.000+00:002022-07-29T16:29:08.800+00:00Davide Sangiorgi's Interview with James Leifer, CONCUR 2022 ToT Award Recipient <p>I am pleased to post <a href="http://www.cs.unibo.it/~sangio/" target="_blank">Davide Sangiorgi</a>'s interview with <a href="https://concur2022.mimuw.edu.pl/tot-award/" target="_blank">CONCUR 2022 Test-of-Time Award</a> recipient <a href="http://pauillac.inria.fr/~leifer/" target="_blank">James Leifer</a>, who will receive the award for the paper <br /><a href="https://link.springer.com/content/pdf/10.1007/3-540-44618-4_19.pdf" target="_blank">"Deriving Bisimulation Congruences for Reactive Systems</a>" co-authored with the late Robin Milner. <br /></p><p>Thanks to James for painting a rich picture of the scientific and social context within which the work on that paper was done and to Davide for conducting the interview. I trust that readers of this blog will enjoy reading it as much as I did. </p><div><b>Davide:</b> How did the work presented in your CONCUR ToT paper come about?</div><div><br /></div><div><b>James:</b> I was introduced to Robin Milner by my undergraduate advisor Bernard Sufrin around 1994. Thanks to that meeting, I started with Robin at Cambridge in 1995 as a fresh Ph.D. student. Robin had recently moved from Edinburgh and had a wonderful research group, including, at various times, Peter Sewell, Adriana Compagnoni, Benjamin Pierce, and Philippa Gardner. There were also many colleagues working or visiting Cambridge interested in process calculi: Davide Sangiorgi, Andy Gordon, Luca Cardelli, Martín Abadi,... It was an exciting atmosphere! I was particularly close to Peter Sewell, with whom I discussed the ideas here extensively and who was generous with his guidance.</div><div><br /></div><div>There was a trend in the community at the time of building complex process calculi (for encryption, Ambients, etc.) where the free syntax would be quotiented by a structural congruence to "stir the soup" and allow different parts of a tree to float together; reaction rules (unlabelled transitions) then would permit those agglomerated bits to react, to transform into something new.</div><div><br /></div><div>Robin wanted to come up with a generalised framework, which he called Action Calculi, for modelling this style of process calculi. His framework would describe graph-like "soups" of atoms linked together by arcs representing binding and sharing; moreover the atoms could contain subgraphs inside of them for freezing activity (as in prefixing in the pi-calculus), with the possibility of boundary crossing arcs (similarly to how nu-bound names in pi-calculus can be used in deeply nested subterms). </div><div><br /></div><div>Robin had an amazing talent for drawing beautiful graphs! He would "move" the nodes around on the chalkboard and reveal how a subgraph was in fact a reactum (the LHS of an unlabelled transition). In the initial phases of my Ph.D. I just tried to understand these graphs: they were so natural to draw on the blackboard! And yet, they were also so uncomfortable to use when written out in linear tree- and list-like syntax, with so many distinct concrete representations for the same graph.</div><div><br /></div><div>Putting aside the beauty of these graphs, what was the benefit of this framework? If one could manage to embed a process calculus in Action Calculi, using the graph structure and fancy binding and nesting to represent the quotiented syntax, what then? We dreamt about a proposition along the following lines: if you represent your syntax (quotiented by your structural congruence) in Action Calculi graphs, and you represent your reaction rules as Action Calculi graph rewrites, then we will give you a congruential bisimulation for free!</div><div><br /></div><div>Compared to CCS for example, many of the rich new process calculi lacked labelled transitions systems. In CCS, there was a clean, simple notion of labelled transitions and, moreover, bisimulation over those labelled transitions yielded a congruence: for all processes <i>P</i> and <i>Q</i>, and all process contexts<i> C[-]</i>, if <i>P ~ Q</i>, then <i>C[P] ~ C[Q]</i>. This is a key quality for a bisimulation to possess, since it allows modular reasoning about pieces of a process, something that's so much harder in a concurrent world than in a sequential one.</div><div><br /></div><div>Returning to Action Calculi, we set out to make good on the dream that everyone gets a congruential bisimulation for free! Our idea was to find a general method to derive labelled transitions systems from the unlabelled transitions and then to prove that bisimulation built from those labelled transitions would be a congruence.</div><div><br /></div><div>The idea was often discussed at that time that there was a duality whereby a process undergoing a labelled transition could be thought of as the environment providing a complementary context inducing the process to react. In the early labelled transition system in pi-calculus for example, I recall hearing that <i>P</i> undergoing the input labelled transition <i>xy</i> could be thought of as the environment outputting payload<i> y </i>on channel <i>x</i> to enable a tau transition with <i>P.</i></div><div><br /></div><div>So I tried to formalise this notion that labelled transitions are environmental contexts enabling reaction, i.e. defining <i>P ---C[-]---> P'</i> to mean <i>C[P] ------> P'</i> provided that <i>C[-]</i> was somehow "minimal", i.e. contained nothing superfluous beyond what was necessary to trigger the reaction. We wanted to get a rigorous definition of that intuitive idea. There was a long and difficult period (about 12 months) wandering through the weeds trying to define minimal contexts for Action Calculi graphs (in terms of minimal nodes and minimal arcs), but it was hugely complex, frustrating, and ugly and we seemed no closer to the original goal of achieving congruential bisimulation with these labelled transitions systems.</div><div><br /></div><div>Eventually I stepped back from Action Calculi and started to work on a more theoretical definition of "minimal context" and we took inspiration from category theory. Robin had always viewed Action Calculi graphs as categorical arrows between objects (where the objects represented interfaces for plugging together arcs). At the time, there was much discussion of category theory in the air (for game theory); I certainly didn't understand most of it but found it interesting and inspiring. </div><div><br /></div><div>If we imagine that processes and process-contexts are just categorical arrows (where the objects are arities) then context composition is arrow composition. Now, assuming we have a reaction rule <i>R ------> R'</i>, we can define labelled transitions <i>P ---C[-]---> P'</i> as follows: there exists a context <i>D</i> such that <i>C[P] = D[R] </i>and <i>P' = D[R']</i>. The first equality is a commuting diagram and Robin and I thought that we could formalise minimality by something like a categorical pushout! But that wasn't quite right as <i>C </i>and <i>D</i> are not <i>the minimum </i>pair (compared to all other candidates), but <i>a minimal</i> pair: there may be many incomparable minimal pairs all of which are witnesses of legitimate labelled transitions. There was again a long period of frustration eventually resolved when I reinvented "relative pushouts" (in place of pushouts). They are a simple notion in slice categories but I didn't know that until later...</div><div><br /></div><div>Having found a reasonable definition of "minimal", I worked excitedly on bisimulation, trying to get a proof of congruence: <i>P ~ Q</i> implies <i>E[P] ~ E[Q]</i>. For weeks, I was considering the labelled transitions of <i>E[P] ---F[-]---></i> and all the ways that could arise. The most interesting case is when a part of <i>P,</i> a part of <i>E</i>, and <i>F</i> all "conspire" together to generate a reaction. From that I was able to derive a labelled transition of <i>P</i> by manipulating relative pushouts, which by hypothesis yielded a labelled transition of <i>Q</i>, and then, via a sort of "pushout pasting", a labelled transition <i>E[Q] ---F[-]---></i>. It was a wonderful moment of elation when I pasted all the diagrams together on Robin's board and we realised that we had the congruence property for our synthesised labels!</div><div><br /></div><div>We looked back again at Action Calculi, using the notion of relative pushouts to guide us (instead of the arbitrary approach we had considered before) and we further looked at other kinds of process calculi syntax to see how relative pushouts could work there... Returning to the original motivation to make Action Calculi a universal framework with congruential bisimulation for free, I'm not convinced of its utility. But it was the challenge that led us to the journey of the relative pushout work, which I think is beautiful.</div><div><br /></div><div><b>Davide: </b>What influence did this work have in the rest of your career? How much of your subsequent work built on it?</div><div><b><br /></b></div><div><b>James:</b> It was thanks to this work that I visited INRIA Rocquencourt to discuss process calculi with Jean-Jacques Lévy and Georges Gonthier. They kindly invited me to spend a year as postdoc in 2001 after I finished my thesis with Robin, and I ended up staying in INRIA ever since. I didn't work on bisimulation again as a research topic, but stayed interested in concurrency and distribution for a long time, working with Peter Sewell et al on distributed language design with module migration and rebinding, and with Cédric Fournet et al on compiler design for automatically synthesising cryptographic protocols for high level sessions specifications.</div><div><br /></div><div><b>Davide: </b>Could you tell us about your interactions with Robin Milner? What was it like to work with him? What lessons did you learn from him?</div><div><br /></div><div><b>James: </b>I was tremendously inspired by Robin.</div><div><br /></div><div>He would stand at his huge blackboard, his large hands covered in chalk, his bicycle clips glinting on his trousers, and he would stalk up and down the blackboard --- thinking and moving. There was something theatrical and artistic about it: his thinking was done in physical movement and his drawings were dynamic as the representations of his ideas evolved across the board.</div><div><br /></div><div>I loved his drawings. They would start simple, a circle for a node, a box for a subgraph, etc. and then develop more and more detail corresponding to his intuition. (It reminded me of descriptions I had read of Richard Feynman drawing quantum interactions.)</div><div><br /></div><div>Sometimes I recall being frustrated because I couldn't read into his formulas everything that he wanted to convey (and we would then switch back to drawings) or I would be worried that there was an inconsistency creeping in or I just couldn't keep up, so the board sessions could be a roller coaster ride at times!</div><div><br /></div><div>Robin worked tremendously hard and consistently. He would write out and rewrite out his ideas, regularly circulating hand written documents. He would refine over and over his diagrams. Behind his achievements there was an impressive consistency of effort.</div><div><br /></div><div>He had a lot of confidence to carry on when the sledding was hard. He had such a strong intuition of what ought to be possible, that he was able to sustain years of effort to get there.</div><div><br /></div><div>He was generous with praise, with credit, with acknowledgement of others' ideas. He was generous in sharing his own ideas and seemed delighted when others would pick them up and carry them forward. I've always admired his openness and lack of jealousy in sharing ideas.</div><div><br /></div><div>In his personal life, he seemed to have real compatibility with Lucy (his wife), who also kept him grounded. I still laugh when I remember once working with him at his dining room table and Lucy announcing, "Robin, enough of the mathematics. It's time to mow the lawn!" </div><div><br /></div><div>I visited Oxford for Lucy's funeral and recall Robin putting a brave face on his future plans; I returned a few weeks later when Robin passed away himself. I miss him greatly. </div><div><br /></div><div><b>Davide: </b>What research topics are you most interested in right now? How do you see your work develop in the future?</div><div><br /></div><div><b>James:</b> I've been interested in a totally different area, namely healthcare, for many years. I'm fascinated by how patients, and information about them, flows through the complex human and machine interactions in hospital. When looking at how these flows work, and how they don't, it's possible to see where errors arise, where blockages happen, where there are informational and visual deficits that make the job of doctors and nurses difficult. I like to think visually in terms of graphs (incrementally adding detail) and physically moving through the space where the action happens --- all inspired by Robin!</div>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-62773158088406963862022-07-05T18:13:00.005+00:002022-07-06T21:35:56.458+00:00ICALP and the EATCS turn 50<p>These days, our colleagues at IRIF are hosting <a href="https://icalp2022.irif.fr/" target="_blank">ICALP 2022</a> in Paris. This is the 49th edition of the ICALP conference, which turns 50 since its first instalment was held in 1972. ICALP was the first conference of the, then newly founded, <a href="https://eatcs.org/" target="_blank">European Association for Theoretical Computer Science (EATCS)</a>.The rest is history and I let any readers this post might have draw their own conclusions on the role that the EATCS and ICALP have played in supporting the development of theoretical computer science. (Admittedly, my opinions on both the EATCS and ICALP are very biased.) </p><p>The <a href="https://icalp2022.irif.fr/?page_id=42" target="_blank">scientific programme of ICALP 2022</a> is mouthwatering as usual, thanks to the work done by the authors of submitted papers, Mikołaj Bojańczyk and David Woodruff (PC chairs), and their PCs. I encourage everyone to read the papers that are being presented at the conference.</p><p>The main purpose of this post, however, is to alert the readers of this blog that ICALP 2022 also hosts an <a href="https://icalp2022.irif.fr/?page_id=1111" target="_blank">exhibition to celebrate EATCS/ICALP at 50</a> and theoretical computer science at large. If you are in Paris, you can attend the exhibition in person. Otherwise, you can visit it virtually <a href="https://icalp2022.irif.fr/?page_id=1111" target="_blank">here</a>. (See also the posters in <a href="https://drive.google.com/file/d/1L7wLDYyDCNfSCvnNA8jWZiMb3BRLy14k/view" target="_blank">one PDF file</a>.)<br /></p><p>I had the honour to take part in the preparation of the material for that exhibition, which was led by Sandrine Cadet and Sylvain Schmitz. I learnt a lot from all the other colleagues in the committee for the exhibition. </p><p>As part of that work, I asked <a href="https://www.pilucrescenzi.it/" target="_blank">Pierluigi Crescenzi</a> whether he'd be willing to carry out a graph and data mining analysis of ICALP vis-a-vis other major conferences in theoretical computer science based on DBLP data. Pierluigi's work went well beyond the call of duty and is summarised in <a href="https://slides.com/piluc/icalp-50?token=fl3BBJ8j" target="_blank">this presentation</a>. I trust that you'll find the results of the analysis by Pierluigi and three of his students at the <a href="https://sites.google.com/gssi.it/csgssi" target="_blank">Gran Sasso Science Institute</a> very interesting. If you have any suggestions for expanding that analysis further, please write it in the comment section. </p><p>Let me close by wishing the EATCS and ICALP a happy 50th birthday, and a great scientific and social event to all the colleagues who are attending ICALP 2022. <br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-26751946666605473172022-06-21T20:53:00.002+00:002022-06-23T11:39:16.494+00:00Interview with Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar and Mariëlle Stoelinga, CONCUR 2022 ToT Award Recipients<p>In this instalment of the Process Algebra Diary, <a href="http://math.umons.ac.be/staff/Randour.Mickael/" target="_blank">Mickael Randour</a> and I joined forces to interview <a href="https://luca.dealfaro.com/" target="_blank">Luca de Alfaro</a>, <a href="http://wpage.unina.it/m.faella/" target="_blank">Marco Faella</a>, <a href="https://pub.ist.ac.at/~tah/" target="_blank">Thomas A. Henzinger</a>, <a href="https://people.mpi-sws.org/~rupak/" target="_blank">Rupak Majumdar</a> and <a href="https://wwwhome.ewi.utwente.nl/~marielle/" target="_blank">Mariëlle Stoelinga</a>, who are some of the recipients of the <a href="https://concur2022.mimuw.edu.pl/tot-award/" target="_blank">CONCUR 2022 Test-of-Time award</a>. We hope that you'll enjoy reading the very inspiring and insightful answers provided by the above-mentioned colleagues to our questions. <br /></p><p>Note: In what follows, "Luca A." refers to me, whereas "Luca" is Luca de Alfaro. <br /></p><p><b>Luca A. and Mickael:</b> You receive the CONCUR ToT Award 2022 for your paper "<a href="https://pub.ist.ac.at/~tah/Publications/the_element_of_surprise_in_timed_games.pdf)" target="_blank">The Element of Surprise in Timed Games</a>", which appeared at CONCUR 2003. In that article, you studied concurrent, two-player timed games. A key contribution of your paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise, as they are played “faster”, and the definition of natural concepts of winning conditions for the two players — ensuring that players can win only by playing according to a physically meaningful strategy. In our opinion, this is a great example of how novel concepts and definitions can advance a research field. Could you tell us more about the origin of your model?</p><p><br /><b>All: </b>Mariëlle and Marco were postdocs with Luca at UCSC in that period, Rupak was a student of Tom's, and we were all in close touch, meeting very often to work together. We all had worked much on games, and an extension to timed games was natural for us to consider. </p><p><br />In untimed games, players propose a move, and the moves jointly determine the next game state. In these games there is no notion of real-time. We wanted to study games in which players could decide not only the moves, but also the instant in time when to play them.</p><p><br />In timed automata, there is only one “player” (the automaton), which can take either a transition, or a time step. The natural generalization would be a game in which players could propose either a move, or a time step.</p><p><br />Yet, we were unsatisfied with this model. It seemed to us that it was different to say “Let me wait 14 seconds and reconvene. Then, let me play my King of Spades” or “Let me play my King of Spades in 14 seconds”. In the first, by stopping after 14 seconds, the player is providing a warning that the card might be played. In the second, there is no such warning. In other words, if players propose either a move or a time-step, they cannot take the adversary by surprise with a move at an unanticipated instant. We wanted a model that could capture this element of surprise.</p><p><br />To capture the element of surprise, we came up with a model in which players propose both a move and the delay with which it is played. After this natural insight, the difficulty was to find the appropriate winning condition, so that a player could not win by stopping time. </p><p><br /><b>Tom:</b> Besides the infinite state space (region construction etc.), a second issue that is specific to timed systems is the divergence of time. Technically, divergence is a built-in Büchi condition ("there are infinitely many clock ticks"), so all safety and reachability questions about timed systems are really co-Büchi and Büchi questions, respectively. This observation had been part of my work on timed systems since the early 1990s, but it has particularly subtle consequences for timed games, where no player (and no collaboration of players) should have the power to prevent time from diverging. This had to be kept in mind during the exploration of the modeling space.</p><p><br /><b>All:</b> We came up with many possible winning conditions, and for each we identified some undesirable property, except for the one that we published. This is in fact an aspect that did not receive enough attention in the paper; we presented the chosen winning condition, but we did not discuss in full detail why several other conditions that might have seemed plausible did not work.</p><p><br />In the process of analyzing the winning conditions, we came up with many interesting games, which form the basis of many results, such as the result on lack of determinazation, on the need for memory in reachability games (even when clock values are part of the state), and most famously as it gave the title to the paper, on the power of surprise.</p><p><br />After this fun ride came the hard work, where we had to figure out how to solve these games. We had worked at symbolic approaches to games before, and we followed the approach here, but there were many complex technical adaptations required. When we look at the paper in the distance of time, it has this combination of a natural game model, but also of a fairly sophisticated solution algorithm.</p><p><br /><b>Luca A. and Mickael: </b>Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? If so, which of your subsequent results on (timed) games do you like best? Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising?</p><p><br /><b>Luca:</b> Marco and I built Ticc, which was meant to be a tool for timed interface theories, based largely on the insights in this paper. The idea was to be able to check the compatibility of real-time systems, and automatically infer the requirements that enable two system components to work well together – to be compatible in time. We thought this would be useful for hardware or embedded systems, and especially for control systems, and in fact the application is important: there is now much successful work on the compositionality of StateFlow/Simulink models.</p><p><br />We used MTBDDs as the symbolic engine, and Marco and I invented a language for describing the components and we wrote by pair-programming some absolutely beautiful Ocaml code that compiled real-time component models into MTBDDs (perhaps the nicest code I have ever written). The problem was that we were too optimistic in our approach to state explosion, and we were never able to study any system of realistic size.</p><p><br />After this, I became interested in games more in an economic setting, and from there I veered into incentive systems, and from there to reputation systems and to a three-year period in which I applied reputation systems in practice in industry, thus losing somewhat touch with formal methods work.</p><p><b>Marco:</b> I’ve kept working on games since the award-winning paper, in one way or another. The closest I’ve come to the timed game setting has been with controller synthesis games for hybrid automata. In a series of papers, we had fun designing and implementing symbolic algorithms that manipulate polyhedra to compute the winning region of a linear hybrid game. The experience gained on timed games helped me recognize the many subtleties arising in games played in real time on a continuous state-space. <br /></p><p><b>Mariëlle:</b> I have been working on games for test case generation: One player represents the tester, which chooses inputs to test; the other player represents the System-under-Test, and chooses the outputs of the system. Strategy synthesis algorithms can then compute strategies for the tester that maximize all kinds of objectives, eg reaching certain states, test coverage etc. </p><p><br />A result that I really like is that we were able to show a very close correspondence between the existing testing frameworks and game theoretic frameworks: Specifications act as game arenas; test cases are exactly game strategies, and the conformance relation used in testing (namely ioco) coincides with game refinement (i.e. alternating refinement). </p><p><br /><b>Rupak:</b> In an interesting way, the first paper on games I read was the <a href="https://www-verimag.imag.fr/~sifakis/RECH/Synth-MalerPnueli.pdf" target="_blank">one by Maler, Pnueli and Sifakis (STACS 95)</a> that had both fixpoint algorithms and timed games (without “surprise”). So the problem of symbolic solutions to games and their applications in synthesis followed me throughout my career. I moved to finding controllers for games with more general (non-linear) dynamics, where we worked on abstraction techniques. We also realized some new ways to look at restricted classes of adversaries. I was always fortunate to have very good collaborators who kept my interest alive with new insights. Very recently, I have gotten interested in games from a more economic perspective, where players can try to signal each other or persuade each other about private information but it’s too early to tell where this will lead.</p><p><br /><b>Luca A. and Mickael:</b> What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?</p><p><br /><b>Mariëlle: </b>Throughout my academic life, I have been working on stochastic analysis --- with Luca and Marco, we worked on stochastic games a lot. First only on theory, but later also on industrial applications, esp in the railroad and high-tech domain. At some point in time, I realized that my work was actually centred around analysing failure probabilities and risk. That is how I moved into risk analysis; the official title of the title of the chair I hold is Risk Management for High Tech Systems. </p><p><br />The nice thing is: this sells <i>much</i> better than Formal Methods! Almost nobody knows what Formal Methods are, and if they know, people think “yes, those difficult people who urge us to specify everything mathematically”. For risk management, this is completely different: everybody understands that this is an important area. <br /><br /><b>Luca: </b>I am currently working on computational ecology, on ML for networks, and on fairness in data and ML. In computational ecology, we are working on the role of habitat and territory for species viability. We use ML techniques to write “differentiable algorithms”, where we can compute the effect of each input – such as the kind of vegetation in each square-kilometer of territory – on the output. If all goes well, this will enable us to efficiently compute which regions should be prioritized for protection and habitat conservation.</p><p><br />In networks, we have been able to show that reinforcement learning can yield tremendous throughput gains in wireless protocols, and we are now starting to work on routing and congestion control.</p><p><br />And in fairness and ML, we have worked on the automatic detection of anomalous data subgroups (something that can be useful in model diagnostics), and we are now working on the spontaneous inception of discriminatory behavior in agent systems.</p><p><br />While these do not really constitute a coherent research effort, I can certainly say that I am having a grand tour of CS – the kind of joy ride one can afford with tenure!</p><p><br /><b>Rupak: </b>I have veered between practical and theoretical problems. I am working on charting the decidability frontier for infinite-state model checking problems (most recently, for asynchronous programs and context-bounded reachability). I am also working on applying formal methods to the world of cyber-physical systems ---mostly games and synthesis. Finally, I have become very interested in applying formal methods to large scale industrial systems through a collaboration with Amazon Web Services. There is still a large gap between what is theoretically understood and what is practically applicable to these systems; and the problems are a mix of technical and social.</p><p><br /><b>Luca A. and Mickael:</b> You have a very strong track record in developing theoretical results and in applying them to real-life problems. In our, admittedly biased, opinion, your work exemplifies Ben Schneiderman's <a href="https://www.pnas.org/doi/pdf/10.1073/pnas.1802918115" target="_blank">Twin-Win Model</a>, which propounds the pursuit of "the dual goals of breakthrough theories in published papers and validated solutions that are ready for widespread dissemination." Could you say a few words on your research philosophy? How do you see the interplay between basic and applied research?</p><p><br /><b>Luca:</b> This is very kind for you to say, and a bit funny to hear, because certainly when I was young I had a particular talent for getting lost in useless theoretical problems. </p><p><br />I think two things played in my favor. One is that I am curious. The other is that I have a practical streak: I still love writing code and tinkering with “things”, from IoT to biology to web and more. This tinkering was at the basis of many of the works I did. My work on reputation systems started when I created a wiki on cooking; people were vandalizing it, and I started to think about game theory and incentives for collaboration, which led to my writing much of the code for Wikipedia analysis, and at Google, for Maps edits analysis. My work on networks started with me tinkering with simple reinforcement-learning schemes that might work, and writing the actual code. On the flip side, my curiosity too often had the better of me, so that I have been unable to pay the continuous and devoted attention to a single research field. I am not a specialist in any single thing I do or I have done. I am always learning the ropes of something I don’t quite know yet how to do.</p><p><br />My applied streak probably gave me some insight on which problems might be of more practical relevance, and my frequent field changes have allowed me to bring new perspectives to old problems. There were not many people using RL for wireless networks, there are not many who write ML and GPU code and also avidly read about conservation biology.<br /><br /><b>Rupak:</b> I must say that Tom and Luca were very strong influencers for me in my research: both in problem selection and in appreciating the joy of research. I remember one comment of Tom, paraphrased as “Life is short. We should write papers that get read.” I spent countless hours in Luca’s office and learnt a lot of things about research, coffee, the ideal way to make pasta, and so on.<br /></p><p><b>Marco:</b> It was an absolute privilege to be part of the group that wrote that paper (my 4th overall, according to DBLP). I’d like to thank my coauthors, and Luca in particular, for guiding me during those crucially formative years.</p><p><b>Mariëlle: </b>I fully agree! <br /></p><p><br /><b>Luca A. and Mickael:</b> Several of you have high-profile leadership roles at your institutions. What advice would you give to a colleague who is about to take up the role of department chair, director of a research centre, dean or president of a university? How can one build a strong research culture, stay research active and live to tell the tale?</p><p><br /><b>Luca:</b> My colleagues may have better advice; my productivity certainly decreased when I was department chair, and is lower even now that I am the vice-chair. <br />When I was young, I was ambitious enough to think that my scientific work would have the largest impact among the things I was doing. But I soon realized that some of the greatest impact was on others: on my collaborators, on the students I advised, who went on to build great careers and stayed friends, and on all the students I was teaching. This awareness serves to motivate and guide me in my administrative work. The CS department at UCSC is one of the ten largest in the number of students we graduate, and the time I spend on improving its organization and the quality of the education it delivers is surely very impactful. My advice to colleagues is to consider their service not as an impediment to research, but as one of the most impactful things they do.</p><p><br />My way of staying alive is to fence off some days that I only dedicate to research (aside from some unavoidable emergency), and also, to have collaborators that give me such joy in working together that they brighten and energize my whole day. </p><p><br /><b>Luca A. and Mickael:</b> Finally, what advice would you give to a young researcher who is keen to start working on topics related to concurrency theory today?<br /> </p><p><b>Luca: </b>Oh that sounds very interesting! And, may I show you this very interesting thing we are doing in Jax to model bird dispersal? We feed in this climate and vegetation data, and then we…</p><p><br />Just kidding. Just kidding. If I come to CONCUR I promise not to lead any of the concurrency yearlings astray. At least I will try.</p><p><br />My main advice would be this: work on principles that allow correct-by-design development. If you look at programming languages and software engineering, the progress in software productivity has not happened because people have become better at writing and debugging code written in machine language or C. It has happened because of the development of languages and software principles that make it easier to build large systems that are correct by construction.<br />We need the same kind of principles, (modeling) languages, and ideas to build correct concurrent systems. Verification alone is not enough. Work on design tools, ideas to guide design, and design languages.</p><p><br /><b>Tom:</b> In concurrency theory we define formalisms and study their properties. Most papers do the studying, not the defining: they take a formalism that was defined previously, by themselves or by someone else, and study a property of that formalism, usually to answer a question that is inspired by some practical motivation. To me, this omits the most fun part of the exercise, the {\it defining} part. The point I am trying to make is not that we need more formalisms, but that, if one wishes to study a specific question, it is best to study the question on the simplest possible formalism that exhibits exactly the features that make the question meaningful. To do this, one often has to define that formalism. In other words, the formalism should follow the question, not the other way around. This principle has served me well again and again and led to formalisms such as timed games, which try to capture the essence needed to study the power of timing in strategic games played on graphs. So my advice to a young researcher in concurrency theory is: choose your formalism wisely and don't be afraid to define it. <br /><br /><b>Rupak:</b> Problems have different measures. Some are practically justified (“Is this practically relevant in the near future?”) and some are justified by the foundations they build (“Does this avenue provide new insights and tools?”). Different communities place different values on the two. But both kinds of work are important and one should recognize that one set of values is not universally better than the other.<br /></p><p><b>Mariëlle:</b> As Michael Jordan puts it: <i>Just play. Have fun. Enjoy the game.</i></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-56782344824205671402022-05-30T15:15:00.000+00:002022-05-30T15:15:44.384+00:00Orna Kupferman's Interview with Christel Baier, Holger Hermanns and Joost-Pieter Katoen, CONCUR 2022 ToT Award Recipients <p><i><span class="im">I am delighted to post <a href="https://www.cs.huji.ac.il/~ornak/" target="_blank">Orna Kupferman</a>'s interview with <a href="https://concur2022.mimuw.edu.pl/tot-award/" target="_blank">CONCUR 2022 Test-of-Time Award</a> recipients <a href="https://wwwtcs.inf.tu-dresden.de/~baier/" target="_blank">Christel Baier</a>, <a href="https://depend.cs.uni-saarland.de/~hermanns/" target="_blank">Holger Hermanns</a> and<a href="https://www-i2.informatik.rwth-aachen.de/~katoen/" target="_blank"> Joost-Pieter Katoen</a>. </span></i></p><p><span class="im"><i><br />Thanks to Christel, Holger and Joost-Pieter for their answers (labelled BHK in what follows) and to Orna (Q below) for conducting the interview. Enjoy and watch this space for upcoming interviews with the other award recipients!</i> <br /></span></p><p><span class="im">Q: You receive the CONCUR Test-of-Time Award 2022 for your paper "<a href="https://link.springer.com/content/pdf/10.1007/3-540-48320-9_12.pdf" target="_blank">Approximate symbolic model checking of continuous-time Markov chains</a>," which appeared <br />at CONCUR 1998. In that article, you combine three different challenges: symbolic algorithms, real-time systems, and probabilistic systems. Could you briefly explain to our readers what the main challenge in such a combination is?<br /><br /></span>BHK: The main challenge is to provide a fixed-point characterization of time-bounded reachability probabilities: the probability to reach a given target state within a given deadline. Almost all works in the field up to 1999 treated discrete-time probabilistic models and focused on "just" reachability probabilities: what is the probability to eventually end up in a given target state? This can be characterized as a unique solution of a linear equation system. The question at stake was: how to incorporate a real-valued deadline <i>d</i>? The main insight was <br />to split the problem in staying a certain amount of time, <i>x</i> say, in the current state and using the remaining <i>d-x</i> time to reach the target from its successor state. This yields a <a href="https://en.wikipedia.org/wiki/Volterra_integral_equation" target="_blank">Volterra integral equation system</a>; indeed time-bounded reachability probabilities are unique solutions of such equation systems. In the CONCUR'99 paper we suggested to use symbolic data structures to do the numerical integration; later we found out that much more efficient techniques can be applied.<span class="im"><br /><br />Q: Could you tell us how you started your collaboration on the award-winning paper? In particular, as the paper combines three different challenges, is it the case that each of you has brought to the research different expertise?<br /><br /></span>BHK: Christel and Joost-Pieter were both in Birmingham, where a meeting of a <br />collaboration project between German and British research groups on stochastic systems and process algebra took place. There the first ideas of model checking continuous-time Markov chains arose, especially for time-bounded reachability: with stochastic process algebras there were means to model CTMCs in a compositional manner, but verification was lacking. Back in Germany, Holger suggested to include a steady-state operator, the counterpart of transient properties that can be expressed using timed reachability probabilities. We then also developed the symbolic data structure to support the verification of the entire logic.<span class="im"></span><span class="im"><br /><br />Q: Your contribution included a generalization of <a href="https://en.wikipedia.org/wiki/Binary_decision_diagram" target="_blank">BDDs (binary decision diagrams)</a> to <a href="https://www.cs.cmu.edu/~emc/papers/Contributions%20to%20Edited%20Volumes/Multi-Terminal%20Binary%20Decision%20Diagrams%20and%20Hybrid%20Decision%20Diagrams.pdf" target="_blank">MTDDs (multi-terminal decision diagrams)</a>, which allow both Boolean and real-valued variables. What do you think about the current state of symbolic algorithms, in particular the choice between SAT-based methods and methods that are based on decision diagrams?<br /><br /></span>BHK: BDD-based techniques entered probabilistic model checking in the mid 1990's for discrete-time models such as Markov chains. Our paper was one of the first, perhaps even the first, that proposed to use BDD structures for real-time stochastic processes. Nowadays, SAT, and in particular SMT-based techniques belong to the standard machinery in probabilistic model checking. SMT techniques are e.g., used in bisimulation minimization at the language level, counterexample generation, and parameter synthesis. This includes both linear as well as non-linear theories. BDD techniques are still used, mostly in combination with sparse representations, but it is fair to say that SMT is becoming more and more relevant.<span class="im"><br /><br />Q: What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?<br /><br /></span>BHK: This depends a bit on whom you ask! Christel's recent work is about cause-effect reasoning and notions of responsibility in the verification context. This ties into the research interest of Holger who looks at the foundations of perspicuous software systems. This research is rooted in the observation that the explosion of opportunities for software-driven innovations comes with an implosion of human opportunities and capabilities to understand and control these innovations. Joost-Pieter focuses on pushing the borders of automation in weakest-precondition reasoning of probabilistic programs. This involves loop invariant synthesis, probabilistic termination proofs, the development of deductive verifiers, and so forth. Challenges are to come up with good techniques for synthesizing quantitative loop invariants, or even complete probabilistic programs.<span class="im"><br /><br />Q: What advice would you give to a young researcher who is keen to start working on topics related to symbolic algorithms, real-time systems, and probabilistic systems?<br /><br /></span>BHK: Try to keep it smart and simple.</p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-12902686607439136232022-05-06T15:01:00.003+00:002022-05-06T15:01:31.758+00:00HALG 2022: Call for participationI am posting this call for participation on behalf of<strong> </strong>Keren Censor-Hillel, PC chair for HALG 2022. I expect that many colleagues from the Track A community will attend that event<span style="color: #0000ee;"><u> </u>and enjoy its mouth-watering scientific programme.<u> </u></span><strong></strong><div style="text-align: left;"><p><strong> </strong></p><p style="text-align: center;"><strong>7th Highlights of Algorithms conference (HALG 2022)<br /></strong>The London School of Economics and Political Science, June 1-3, 2022<br /><a href="https://www.lse.ac.uk/HALG-2022" rel="noreferrer noopener" target="_blank">https://www.lse.ac.uk/HALG-2022</a></p> <p><br />The Highlights of Algorithms conference is a forum for presenting the highlights of recent developments in algorithms and for discussing potential further advances in this area. The conference will provide a broad picture of the latest research in algorithms through a series of invited talks, as well as the possibility for all researchers and students to present their recent results through a series of short talks and poster presentations. Attending the Highlights of Algorithms conference will also be an opportunity for networking and meeting leading researchers in algorithms.</p> <p>For local information, visa information, or information about registration, please contact Tugkan Batu <a href="mailto:t.batu@lse.ac.uk" rel="noreferrer noopener" target="_blank">t.batu@lse.ac.uk</a>.—<br /> </p><p><b>PROGRAM </b></p> <p>A detailed schedule and a list of all accepted short contributions is available at <a href="https://www.lse.ac.uk/HALG-2022/programme/Programme" rel="noreferrer noopener" target="_blank">https://www.lse.ac.uk/HALG-2022/programme/Programme</a><br /><br /><strong>REGISTRATION</strong></p> <p><a href="https://www.lse.ac.uk/HALG-2022/registration/Registration" rel="nofollow">https://www.lse.ac.uk/HALG-2022/registration/Registration</a></p> <p><strong></strong></p> <p style="margin-left: 40px; text-align: left;"><strong>Early registration (by 20th May 2022)</strong></p><div style="margin-left: 40px; text-align: left;"> </div><p style="margin-left: 40px; text-align: left;">Students: £100<br class="" />Non-students: £150</p><div style="margin-left: 40px; text-align: left;"> </div><p style="margin-left: 40px; text-align: left;"><strong>Late registration (from 21st May 2022)</strong><br class="" />Students: £175<br class="" />Non-students: £225</p> <p>Registration includes the lunches provided, coffee breaks, and the conference reception.</p> <p>There are some funds from conference sponsors to subsidise student registration fees. Students can apply for a fee waiver by sending an email to Enfale Farooq (<a href="mailto:e.farooq@lse.ac.uk" rel="noreferrer noopener" target="_blank">e.farooq@lse.ac.uk</a>) by <strong>15th May 2022</strong>. Those students presenting a contributed talk will be given priority in allocation of these funds. The applicants will be notified of the outcome by 17th May 2022.<br /></p> <p><strong>INVITED SPEAKERS</strong></p> <p style="margin-left: 40px; text-align: left;">Survey speakers:</p><div style="margin-left: 40px; text-align: left;"> </div><p style="margin-left: 40px; text-align: left;">Amir Abboud (Weizmann Institute of Science) <br />Julia Chuzhoy (Toyota Technological Institute at Chicago)<br />Martin Grohe (RWTH Aachen University)<br />Anna Karlin (University of Washington)<br />Richard Peng (Georgia Institute of Technology)<br />Thatchaphol Saranurak (University of Michigan)</p><div style="margin-left: 40px; text-align: left;"> </div><p style="margin-left: 40px; text-align: left;">Invited talks:<br class="" /><strong><br class="" /></strong>Peyman Afshani (Aarhus University) <br class="" />Soheil Behnezhad (Stanford University) <br class="" />Sayan Bhattacharya (University of Warwick)<br class="" />Guy Blelloch (Carnegie Mellon University)<br class="" />Greg Bodwin (University of Michigan)<br class="" />Mahsa Eftekhari (University of California, Davis)<br class="" />John Kallaugher (Sandia National Laboratories)<br class="" />William Kuszmaul (Massachusetts Institute of Technology)<br class="" />Jason Li (Carnegie Mellon University)<br class="" />Joseph Mitchell (SUNY, Stony Brook)<br class="" />Shay Moran (Technion)<br class="" />Merav Parter (Weizmann Institute of Science)<br class="" />Aviad Rubinstein (Stanford University)<br class="" />Rahul Savani (University of Liverpool)<br class="" />Mehtaab Sawhney (Massachusetts Institute of Technology)<br class="" />Jakub Tetek (University of Copenhagen)<br class="" />Vera Traub (ETH Zurich)<br class="" />Jan Vondrak (Stanford University)<br class="" />Yelena Yuditsky (Université Libre de Bruxelles) </p></div><p></p><p></p><p></p><p></p><p></p><p></p><p></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-5270253147410398802022-03-12T12:24:00.001+00:002022-03-12T15:57:13.247+00:00FOCS 2021 Test-of-Time Award winners (and one deserving paper that missed out)<p>As members of the TCS community will most likely know, FOCS established<a href="https://focs2021.cs.colorado.edu/test-of-time-awards/" target="_blank"> Test-of-Time Awards from its 2021 edition</a> to celebrate contributions published at that conference 30, 20 and 10 years before. The first list of selected winners is, as one might have expected, stellar: <br /></p><ul style="text-align: left;"><li>Uriel Feige, Shafi Goldwasser, László Lovász, Shmuel Safra, Mario Szegedy:<br />Approximating Clique is Almost NP-Complete.<br />FOCS 1991</li><li>David Zuckerman:<br />Simulating BPP Using a General Weak Random Source.<br />FOCS 1991</li><li>Serge A. Plotkin, David B. Shmoys, Éva Tardos:<br />Fast Approximation Algorithms for Fractional Packing and Covering Problems.<br />FOCS 1991</li><li>Ran Canetti:<br />Universally Composable Security: A New Paradigm for Cryptographic Protocols.<br />FOCS 2001</li><li>Boaz Barak:<br />How to Go Beyond the Black-Box Simulation Barrier.<br />FOCS 2001</li><li>Amit Chakrabarti, Yaoyun Shi, Anthony Wirth, Andrew Chi-Chih Yao:<br />Informational Complexity and the Direct Sum Problem for Simultaneous Message Complexity.<br />FOCS 2001</li><li>Zvika Brakerski, Vinod Vaikuntanathan:<br />Efficient Fully Homomorphic Encryption from (Standard) LWE.<br />FOCS 2011</li></ul><p>FWIW, I offer my belated congratulations to all the award recipients, whose work has had, and continues to have, a profound influence on the "Volume A" TCS community. </p><p>Apart from celebrating their achievement, the purpose of this post is to highlight a paper from FOCS 1991 that missed out on the Test-of-Time Award, but that, IMHO, would have fully deserved it. </p><p>I am fully aware that the number of deserving papers/scientists is typically larger, if not much larger, than the number of available awards. Awards are a scarce resource! My goal with this post is simply to remind our community (and especially its younger members) of a seminal contribution that they might want to read or re-read. <br /></p><p>The paper in question is "<a href="https://www.cs.cornell.edu/courses/cs6860/2019sp/Handouts/EmersonJutla91.pdf" target="_blank">Tree automata, mu-calculus and determinacy</a>" by <a href="https://www.cs.utexas.edu/~emerson/" target="_blank">Allen Emerson</a> and <a href="https://researcher.watson.ibm.com/researcher/view.php?person=us-csjutla" target="_blank">Charanjit S. Jutla</a>, which appeared at FOCS 1991. (Emerson shared the 2007 A.M. Turing Award for the invention of model checking and Jutla went on to doing path-breaking work in cryptography.) That paper is absolutely fundamental for the mu-calculus, but also for automata theory, and verification in general. It introduced many ideas and results that became the basis for extensive research. </p><p>As a first contribution, the article introduced <a href="https://en.wikipedia.org/wiki/Parity_game" target="_blank">parity games</a> and proved their fundamental properties. The parity condition was a missing link in automata theory on infinite objects. It made the whole theory much simpler than that proposed in earlier work. Technically, the parity condition is both universal and positional. Universal means that tree automata with parity conditions are as expressive as those with Rabin or Muller conditions. Positional means that in the acceptance game if a player has a winning strategy then she has one depending only on the current position and not on the history of the play so far. This is a huge technical advance for all automata-theoretic constructions and for the analysis of infinite-duration games. It allows one, for instance, to avoid the complicated arguments of Gurevich and Harlington in <a href="https://doi.org/10.1145/800070.802177" target="_blank">their seminal STOC 1982 article</a>, which were already a huge simplification of <a href="https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/S0002-9947-1969-0246760-1.pdf" target="_blank">Rabin's original argument from 1969</a> proving the decidability of the <a href="https://en.wikipedia.org/wiki/Monadic_second-order_logic#Decidability_and_complexity_of_satisfiability" target="_blank">monadic second-order theory of the infinite binary tree</a> and much more. In passing, let me remark that Rabin has gone on record saying that "I consider this to be the most difficult research I have ever done." See <a href="https://cacm.acm.org/magazines/2010/2/69370-an-interview-with-michael-rabin/fulltext" target="_blank">this interview</a> in CACM. </p><p>The second main contribution of that paper is the discovery of the relation between parity games and the mu-calculus. The authors show how a mu-calculus model-checking problem can be reduced to solving a parity game, and conversely, how the set of winning positions in a parity game can be described by a mu-calculus formula. This result is the birth of the "model-checking via games" approach. It also shows that establishing a winner in parity games is contained both in NP and in co-NP. As a corollary, the model-checking problem is as complex as solving games. It is still not known if the problem is in PTIME. A <a href="https://doi.org/10.1145/3055399.3055409" target="_blank">recent advance from STOC'17</a> gives a quasi-polynomial-time algorithm. (See <a href="https://blog.computationalcomplexity.org/2017/03/parity-games-in-quasipolynomial-time.html" target="_blank">this blog post</a> for a discussion of that result, which received the STOC 2017 best paper award and was immediately followed up by a flurry of related papers.) </p><p>Finally, the paper also shows how to prove Rabin's complementation lemma, which is the most difficult step in his celebrated aforementioned decidability result, with the help of parity conditions. The proof is radically simpler than previous approaches. The paper puts this contribution most prominently, but actually the conceptual and technical contributions presented later in the paper turned out to be most important for the community. </p><p>Overall, the above-mentioned paper by Emerson and Jutla is a truly seminal contribution that has stood the test of time, has sown the seeds for much research over the last thirty years (as partly witnessed by the over 1,130 citations it has received so far) and is still stimulating advances at the cutting edge of theoretical computer science that bridge the Volume A-Volume B divide. </p><p>I encourage everyone to read it!</p><p><b>Acknowledgement:</b> I have learnt much of the content of this post from Igor Walukiewicz. The responsibility for any infelicity is mine alone. <br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-55299414643043347112022-03-06T15:26:00.000+00:002022-03-06T15:26:02.261+00:00HALG 2022: Call For Submissions of Short Contributed Presentations<p> <i>On behalf of <a href="https://ckeren.net.technion.ac.il/" target="_blank">Keren Censor-Hillel</a>, PC chair for HALG 2022, I am happy to post the call for </i><i>submissions of short contributed presentations for that event. I encourage all members of the algorithms community to submit their contributed presentations. HALG has rapidly become a meeting point for that community in a relaxed workshop-style setting.</i> </p><p style="text-align: center;"><b>The 7th Highlights of Algorithms conference (HALG 2022) </b></p><p style="text-align: center;"><b>London, June 1-3, 2022 </b></p><p style="text-align: center;"><a href="https://www.lse.ac.uk/">https://www.lse.ac.uk/</a></p><p>HALG-2022 The Highlights of Algorithms conference is a forum for presenting the highlights of recent developments in algorithms and for discussing potential further advances in this area. The conference will provide a broad picture of the latest research in algorithms through a series of invited talks, as well as the possibility for all researchers and students to present their recent results through a series of short talks and poster presentations. Attending the Highlights of Algorithms conference will also be an opportunity for networking and meeting leading researchers in algorithms. </p><p>Call For Submissions of Short Contributed Presentations: The HALG 2022 conference seeks submissions for contributed presentations. Each presentation is expected to consist of a poster and a short talk (serving as an invitation to the poster). There will be no conference proceedings, hence presenting work already published at a different venue or journal (or to be submitted there) is welcome. </p><p>If you would like to present your results at HALG 2022, please submit their details: the abstract, the paper and the speaker of the talk via EasyChair: <a href="https://easychair.org/conferences/?conf=halg2022">https://easychair.org/conferences/?conf=halg2022</a> </p><p>The abstract should include (when relevant) information where the results have been published/accepted (e.g., conference), and where they are publicly available (e.g., arXiv). All submissions will be reviewed by the program committee, giving priority to work accepted or published in 2021 or later. </p><p>Submissions deadline: March 27, 2022. </p><p>Acceptance/rejection notifications will be sent in early April. </p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-65215612633442892332022-03-04T15:35:00.000+00:002022-03-04T15:35:00.795+00:00Combinatorial Exploration: An algorithmic framework to automate the proof of results in combinatorics<p>Are you interested in combinatorial mathematics? If so, I am happy to welcome you to the future! </p><p>I am proud to share with you a new, <a href="https://arxiv.org/abs/2202.07715" target="_blank">99-page preprint</a> by three colleagues from my department (<a href="https://permutatriangle.github.io/authors/bean.html" target="_blank">Christian Bean</a>, <a href="https://permutatriangle.github.io/authors/nadeau.html" target="_blank">Émile Nadeau </a>and <a href="https://permutatriangle.github.io/authors/ulfarsson.html" target="_blank">Henning Ulfarsson</a>) and three of their collaborators (<a href="http://www.cs.otago.ac.nz/staffpriv/malbert/index.php" target="_blank">Michael Albert</a>, <a href="https://akc.is/" target="_blank">Anders Claesson</a> and <a href="http://jaypantone.com/" target="_blank">Jay Pantone</a>) that is the result of years of work that led to the birth of Combinatorial Exploration. <i>Combinatorial Exploration</i> is an algorithmic framework that can prove results that so far have required the ingenuity of human combinatorialists. More specifically, it can study, at the press of a button, the structure of combinatorial objects and derive their counting sequences and generating functions. The applicability and power of Combinatorial Exploration are witnessed by the applications to the domain of permutation patterns given in the paper. My colleagues use it to re-derive <i>hundreds</i> of results in the literature in a uniform manner and prove many new ones. See the <a href="https://permpal.com/" target="_blank">Permutation Pattern Avoidance Library (PermPAL)</a> and Section 2.4 of the article for a more comprehensive list of notable results. The paper also gives three additional proofs-of-concept, showing examples of how Combinatorial Exploration can prove results in the domains of alternating sign matrices, polyominoes, and set partitions. Last, but by no means least, the github repository at <a href="https://github.com/PermutaTriangle/comb_spec_searcher">https://github.com/PermutaTriangle/comb_spec_searcher</a> contains the open-source python framework for Combinatorial Exploration, and the one at <a href="https://github.com/PermutaTriangle/Tilings">https://github.com/PermutaTriangle/Tilings</a> contains the code needed to apply it to the field of permutation patterns. </p><p> "Det er svært at spå, især om fremtiden", as Niels Bohr and Piet Hein famously said. However, let me stick my neck out and predict that this work will have substantial impact and will be the basis for exciting future work. </p><p> Congratulations to my colleagues! With my department chair hat on, I am very proud to see work of this quality stem from my department and humbled by what my colleagues have achieved already. As an interested observer, I am very excited to see what their algorithms will be able to prove in the future. For the moment, let's all enjoy what they have done already. <br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-42707243354017159942021-12-15T08:46:00.001+00:002021-12-15T08:47:27.343+00:00Call for Invited Talk Nominations: 7th Highlights of Algorithms conference (HALG 2022)<p> <i>On behalf of <a href="https://ckeren.net.technion.ac.il/" target="_blank">Keren Censor-Hillel</a>, PC chair for HALG 2022, I am happy to post the call for invited talk nominations for that event. I encourage all members of the algorithms community to submit their nominations. HALG has rapidly become a meeting point for that community in a relaxed workshop-style setting.</i> </p><p style="text-align: center;"><b>Call for Invited Talk Nominations<br /> <br />7th Highlights of Algorithms conference (HALG 2022)<br /> <br />LSE London, June 1-3, 2022</b><br /></p><p><br />The HALG 2022 conference seeks high-quality nominations for invited talks that will highlight recent advances in algorithmic research appearing in a paper in 2021 or later.<br /> <br />To nominate, please email <a href="mailto:halg2022nominations@gmail.com">halg2022nominations@gmail.com</a> the following information in <i>plaintext only</i>:</p><ul style="text-align: left;"><li>Basic details: title of paper, authors, conference/arxiv links, suggested speaker.</li><li>Brief justification: Focus on the benefits to the audience, e.g., quality of results, importance/relevance of topic, clarity of talk, speaker’s presentation skills.<br /></li></ul><p><br />Nominations will be reviewed by the Program Committee to select speakers that will be invited to the conference.<br />Nomination deadline: January 14, 2022 <br /> <br />Please go to <a href="https://highlightsofalgorithms.org/">https://highlightsofalgorithms.org/</a> for general information on HALG and for information about previous HALG meetings.<br /> <br />Keren Censor-Hillel<br />PC chair for HALG 2022</p><p><br /></p><p><br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-30188141096174843332021-12-14T16:29:00.001+00:002021-12-14T16:29:15.217+00:00Faculty positions in Computer Science at Reykjavik University<p> The <a href="https://en.ru.is/st/dcs/" target="_blank">Department of Computer Science at Reykjavik University</a> invites applications for full-time, permanent faculty positions at any rank in the fields of Software Engineering, and Design and Development of Computer Games. Outstanding candidates in other areas of Computer Science are encouraged to apply as well. </p><p>We are looking for energetic, highly qualified academics with a proven international research record and excellent potential in their field of study. The primary evaluation criterion is scientific quality. We particularly welcome applications from researchers who have a strong network of research collaborators, can strengthen internal collaborations within the department, have the proclivity to improve their academic environment and its culture, and generally have potential to flourish in our environment. </p><p>Apart from developing their research career, the successful applicants will play a full part in the teaching and administrative activities of the department, teaching courses and supervising students at both graduate and undergraduate level. Applicants with a demonstrated history of excellence in teaching are preferred. Salary and rank are commensurate with experience. Among other benefits, Reykjavik University offers its research staff the option to take research semesters (sabbaticals) after three years of satisfactory teaching and research activity. The positions are open until filled, with intended starting date in August 2022. Later starting dates can be negotiated. </p><p>The deadline for applications is January 30, 2022. The review of the applications will begin in late January 2022, and will continue until the positions are filled.</p><p>See <a href="https://jobs.50skills.com/ru/en/10749" target="_blank">here</a> for full details and information on how to apply. <br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-70809469538672184142021-12-14T10:23:00.003+00:002021-12-14T10:23:25.096+00:00Near-Optimal Distributed Degree+1 Colouring<p>If you are interested in graph colouring, and specifically in distributed algorithms for that classic problem, I strongly recommend the <a href="https://arxiv.org/abs/2112.00604" target="_blank">recent paper</a> posted by Magnús M. Halldórsson, Fabian Kuhn, Alexandre Nolin and Tigran Tonoyan. (For the record, three of the authors work, or have worked, in my department at Reykjavik University, so I am biased.) </p><p>The above-mentioned paper addresses the problem of finding a proper colouring of a graph when each node <i>v</i> has a palette of degree(<i>v</i>)+1 colours at its disposal. The paper resolves an open problem in distributed colouring and simplifies known results in doing so. As a byproduct of their results, the authors obtain improved streaming and sub-linear time algorithms. See the paper for much more information on the context for this result and the technical details. </p><p>Congratulations to the authors!</p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-877101981056796682021-12-04T12:59:00.003+00:002021-12-05T13:35:16.132+00:00TheoretiCS: A new open-access journal in Theoretical Computer Science<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/a/AVvXsEjf7-wAXJmH9SiOAhxTj4m6svlchJtMYZVkNnWSoaPMvaVSAq3Xn8x902jjH_K7CEvubT8Rj09SwcNiKvpy0iVgtLuYyWk-fFvk7O4yoTyqumEJqRMVpJGM5ONAQMibKk6SKFPXaEtWQA09kSzd0RW8Yke8qd-RZiR-b5FI4JwvkPEU2ENrLw=s320" style="display: block; padding: 1em 0px; text-align: center;"><img alt="" border="0" data-original-height="133" data-original-width="320" src="https://blogger.googleusercontent.com/img/a/AVvXsEjf7-wAXJmH9SiOAhxTj4m6svlchJtMYZVkNnWSoaPMvaVSAq3Xn8x902jjH_K7CEvubT8Rj09SwcNiKvpy0iVgtLuYyWk-fFvk7O4yoTyqumEJqRMVpJGM5ONAQMibKk6SKFPXaEtWQA09kSzd0RW8Yke8qd-RZiR-b5FI4JwvkPEU2ENrLw=s320" width="320" /></a></div><p> I am delighted to share with all the readers of this blog the news of the launch of <a href="https://theoretics-journal.org" target="_blank">TheoretiCS</a>, a new, top-quality, open-access journal dedicated to the whole of Theoretical Computer Science. The journey leading to the establishment of this new journal has been long and the fact that this path eventually reached its destination is due to the sterling efforts and foresight of a number of people within our community. The seeds of TheoretiCS were sown within the Council of the European Association for Theoretical Computer Science during my two terms as president of that association. At that time, <a href="https://www.cwi.nl/people/jos-baeten" target="_blank">Jos Baeten</a> and <a href="https://www.fi.muni.cz/usr/kucera/">Antonin Kucera</a> worked hard to try and set up an open-access journal of the association. That journal never saw the light of day, but the process that eventually led to TheoretiCS was afoot. After some time, <a href="https://ls1-www.cs.tu-dortmund.de/en/kontakt-thomas-schwentick" target="_blank">Thomas Schwentick</a> took the baton in the relay race and took decisive steps in turning the establishment of this new journal into a true community effort. It is fair to say that the launch of this journal has involved an unprecedented level of cooperation amongst <a href="https://theoretics.episciences.org/page/advisory-board" target="_blank">representatives of leading conferences from across the entire Theoretical Computer Science community</a>. I am immensely grateful to everyone who participated in that work for the effort they put into making TheoretiCS a reality and apologise for not mentioning all the colleagues who contributed explicitly in this post. You can find more information on TheoretiCS in the text below, which I received from Jos Baeten, founding member-at-large of the Advisory Board of the Theoretics Foundation. </p><p>So, what can you do to support this new journal? There are at least two things that each of us can do and that I believe are important. </p><ol style="text-align: left;"><li>Help TheoretiCS reach its quality objectives by submitting your best work to it and by encouraging your colleagues to do so too. TheoretiCS aims at publishing articles of a very high quality, and at becoming a reference journal on par with the leading journals in the area. To be accepted, a paper must make a significant contribution of lasting value to a relevant area of TCS, and its presentation must be of high quality. This is elaborated upon in the guiding principles spelled out below. I let you reach your own conclusions about the quality and the breadth of the <a href="https://theoretics.episciences.org/page/editorial-board" target="_blank">editorial board of TheoretiCS</a>, which is stellar IMHO. <br /></li><li>Spread the news of the launch of TheoretiCS within your networks. Despite its many years of existence and the role it plays within our community, I still meet colleagues (even in Theoretical Computer Science) who do not know that <a href="https://www.dagstuhl.de/en/publications/lipics" target="_blank">LIPIcs</a> exists and who claim that publishing conference proceedings with commercial publishers is a sign of scientific quality. </li></ol><p>If you happen to be in a position to do so, you can support the <a href="https://theoretics.episciences.org/page/theoretics-foundation" target="_blank">TheoretiCS foundation</a>, which is a German not-for-profit organization, by making a donation. </p><p></p><p>I look forward to seeing the developments of TheoretiCS. Even though predicting the future is difficult, I have no doubt that the journal will become a coveted outlet, with the help of the community it aims to serve. Welcome to TheoretiCS and good luck!</p><p></p><p><br />=== Additional information about the journal ===<br /><br />--- Guiding principles and objectives ---<br /><br />- We believe that our field (and science in general) needs more 'virtuous' open-access journals, a whole eco-system of them, with various levels of specialization and of selectivity. We also believe that, along with the structuring role played by conferences in theoretical computer science, we collectively need to re-develop the practice of journal publications.<br /><br />- The scope of TheoretiCS is the whole of Theoretical Computer Science, understood in an inclusive meaning (concretely: including, but not restricted to, the Theory of Computing and the Theory of Programming; or equivalently, the so-called TCS-A and TCS-B, reminiscent of Jan van Leeuwen's Handbook of Theoretical Computer Science).<br /><br />- Our aim is to rapidly become a reference journal and to contribute to the unity of the Theoretical Computer Science global community. In particular, we will seek to publish only papers that make a very significant contribution to their respective fields, that strive to be accessible to a wider audience within theoretical computer science, and that are, generally, of a quality on par with the very best journals in the field.<br /><br />- TheoretiCS adheres to the principles of 'virtuous' open-access: there is no charge to read the journal, nor to publish in it. The copyright of the papers remains with the authors, under a Creative Commons license.<br /><br /><br />--- Editorial Board ---<br /><br />The inaugural Editors-in-Chief are Javier Esparza (TU München) and Uri Zwick (Tel Aviv U.). The entire Editorial Board can be seen at <a href="https://theoretics-journal.org">https://theoretics-journal.org</a> (see below as well).<br /><br /><br />--- Organization and a bit of history ---<br /><br />The project built on groundwork laid in the Council of the EATCS, and started in 2019 and underwent a long gestation. From the start, we wanted to have a thorough discussion with a wide representation of the community, on how to best implement the guiding principles sketched above. It was deemed essential to make sure that all fields of theoretical computer science would feel at home in this journal, and that it would be recognized as a valid venue for publication all over the world.<br /><br />This resulted in the creation of an Advisory Board, composed of representatives of most of the main conferences in the field (currently APPROX, CCC, COLT, CONCUR, CSL, FOCS, FoSSaCS, FSCD, FSTTCS, ICALP, ICDT, ITCS, LICS, MFCS, PODC, SoCG, SODA, STACS, STOC, TCC) and of so-called members-at-large. The composition of this Advisory Board, which may still evolve, can be consulted at <a href="https://theoretics-journal.org">https://theoretics-journal.org</a>.<br /><br /><br />--- Logistics and answers to some natural questions ---<br /><br />- The journal is published by the TheoretiCS Foundation, a non-profit foundation established under German law. <br /><br />- TheoretiCS is based on the platform episciences.org, in the spirit of a so-called overlay journal.<br /><br />- The Advisory Board, together with the Editors-in-Chief and the Managing Editors, devolved much of their efforts to designing and implementing an efficient 2-phase review system: efficient in terms of the added-value it brings to the published papers and their authors, and of the time it takes. Yet, as this review system relies in an essential fashion on the work and expertise of colleagues (like in all classical reputable journals), we cannot guarantee a fixed duration for the evaluation of the papers submitted to TheoretiCS.<br /><br />- Being charge-free for authors and readers does not mean that there is no cost to publishing a journal. These costs are supported for the foreseeable future by academic institutions (at the moment, CNRS and Inria, in France; others may join).<br /><br />- The journal will have an ISSN, and each paper will have a DOI. There will be no print edition.<br /><br /><br />--- Editorial Board ---<br /><br />Editors-in-Chief<br /><br /> Javier Esparza (Technische Universität München, Munich)<br /> Uri Zwick (Tel Aviv University, Tel Aviv)<br /><br />Managing Editors<br /><br /> Antoine Amarilli (Institut polytechnique de Paris, Télécom Paris)<br /> Nathanaël Fijalkow (CNRS, Bordeaux, and The Alan Turing Institute of Data Science, London)<br /><br />Editors<br /><br /> Martin Abadi, Google, USA<br /> Andris Ambainis, U. of Latvia<br /> Albert Atserias, UPC, Barcelona<br /> Haris Aziz, UNSW, Sydney<br /> David Basin, ETH Zürich<br /> Patricia Bouyer, CNRS, Paris-Saclay<br /> Nicolò Cesa-Bianchi, Università di Milano<br /> Anuj Dawar, Cambridge University<br /> Luc Devroye, McGill University, Montreal<br /> Jacob Fox, Stanford University<br /> Mohsen Ghaffari, ETH Zürich<br /> Georg Gottlob, Oxford University<br /> Anupam Gupta, Carnegie-Mellon University<br /> Venkatesan Guruswami, Carnegie-Mellon University<br /> Johan Håstad, KTH, Stockholm<br /> Ravi Kannan, Microsoft Research India, Bengaluru<br /> Anna Karlin, University of Washington, Seattle<br /> Ken-ichi Kawarabayashi, National Institute of Informatics, Tokyo<br /> Valerie King, University of Victoria<br /> Robert Kleinberg, Cornell University<br /> Naoki Kobayashi, University of Tokyo<br /> Elias Koutsoupias, Oxford University<br /> Xavier Leroy, Collège de France, Paris<br /> Katrina Ligett, Hebrew University, Jerusalem<br /> Rupak Majumdar, MPI-SWS, Kaiserslautern<br /> Joseph Mitchell, State University of New York at Stony Brook<br /> Mehryar Mohri, Google and New York University<br /> David Mount, University of Maryland<br /> Anca Muscholl, Université de Bordeaux<br /> Danupon Nanongkai, University of Copenhagen<br /> Moni Naor, Weizmann Institute, Rehovot<br /> Catuscia Palamidessi, Inria, Palaiseau<br /> Michał Pilipczuk, University of Warsaw<br /> Jean-Francois Raskin, Université Libre de Bruxelles<br /> Peter Sanders, KIT, Karlsruhe<br /> Davide Sangiorgi, Università di Bologna<br /> Nitin Saxena, IIT Kanpur<br /> Alistair Sinclair, UC Berkeley<br /> Ola Svensson, EPF Lausanne<br /> Gregory Valiant, Stanford University<br /> Stephanie Weirich, University of Pennsylvania<br /> Virginia V. Williams, Massachusetts Institute of Technology<br /> James Worrell, Oxford University<br /> Mihalis Yannakakis, Columbia University, New York<br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-64948122344595051562021-11-24T22:50:00.005+00:002021-11-25T09:25:13.176+00:00Inria Innovation Prize 2021 to Mateescu, Garavel, Lang and Serwe<p>I just learnt that <a href="https://convecs.inria.fr/people/Radu.Mateescu/">Radu Mateescu</a>, <a href="http://convecs.inria.fr/people/Hubert.Garavel/">Hubert Garavel</a>, <a href="http://convecs.inria.fr/people/Frederic.Lang/">Frédéric Lang</a> and <a href="http://convecs.inria.fr/people/Wendelin.Serwe/">Wendelin Serwe</a> from the <a href="http://convecs.inria.fr/">Construction of Verified Concurrent Systems</a> (Convecs) project team at INRIA Grenoble – Rhône-Alpes Centre have been recently awarded the <a href="https://www.inria.fr/en/convecs-team-safety-modeling-distributed-parallel-systems" target="_blank">Inria Innovation Prize – Académie des sciences – Dassault Systèmes</a>. Their work contributes to the development of the <a href="https://cadp.inria.fr/" target="_blank">CADP toolbox</a> for modelling and verifying parallel and distributed systems. The aim of that project is to automatically detect design flaws in highly complex systems. </p><p>Readers of this blog will be as delighted as I am by this news. <a href="https://en.wikipedia.org/wiki/Construction_and_Analysis_of_Distributed_Processes" target="_blank">CADP</a> is one of the tools from the concurrency community that has the longest history, dating back to its early releases in 1989. It has been used to good effect in a variety of applications, is still under continuous development and makes excellent use in practice of classic tools from concurrency theory. By way of example, let me mention the recent successes by the Convecs team in dealing with difficult challenges posed by <a href="http://ls5-www.cs.tu-dortmund.de/cms/de/mitarbeiter/prof/Bernhard_Steffen.html" target="_blank">Bernhard Steffen</a> and his team on the evaluation of CTL and LTL formulae on large products of automata. (See, for instance, the news items <a href="http://cadp.inria.fr/news12.html" target="_blank">here</a> and <a href="http://cadp.inria.fr/news13.html#section-3" target="_blank">here</a>.) Traditional model checkers fail on those challenges because the state space of the product automata is too large for them. However, a wise use of bisimulations and congruence results allows CADP to solve many of those challenges. Interested readers might also wish to peruse the slides at </p><ul style="text-align: left;"><li><a href="http://cadp.inria.fr/ftp/presentations/Mazzanti-RERS-18.pdf">http://cadp.inria.fr/ftp/presentations/Mazzanti-RERS-18.pdf</a> </li><li><a href="http://cadp.inria.fr/ftp/presentations/Lang-RERS-19.pdf">http://cadp.inria.fr/ftp/presentations/Lang-RERS-19.pdf</a> and</li><li><a href="http://cadp.inria.fr/ftp/presentations/Lang-RERS-20.pdf">http://cadp.inria.fr/ftp/presentations/Lang-RERS-20.pdf</a>. </li></ul>Congratulations to the whole CADP team and to the concurrency community for this award!Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-55898240324201813902021-09-16T12:23:00.003+00:002021-09-16T12:25:58.741+00:00PhD scholarship in Data Science for sustainability at Reykjavik University<p style="text-align: center;"><b>Department of Computer Science, Reykjavik University </b></p><p style="text-align: center;"><b>PhD scholarship in Data Science for sustainability by predicting food consumption to reduce food waste </b></p><p>The Department of Computer Science at Reykjavík University is looking for a PhD student to build, apply and evaluate a global model that predicts future food consumption by geographic area. The goal of the project is twofold: Reduce food waste in restaurants and grocery stores by using global machine learning algorithms. Understand food consumption trends in restaurants and grocery stores by analyzing the global model’s input data and their results. The ideal candidate should possess data science expertise, be passionate about sustainability and enthusiastic about research. The project is a collaboration with <a href="https://greenbytes.is" target="_blank">GreenBytes</a> and will be carried out in Reykjavik, Iceland. </p><p>See <a href="https://jobs.50skills.com/ru/en/10068">https://jobs.50skills.com/ru/en/10068</a> for full details and for information on how to apply.</p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-76779862341532910672021-08-28T12:27:00.005+00:002021-08-31T09:08:09.730+00:00Interview with CONCUR 2021 ToT Award Recipients: David Janin and Igor Walukiewicz<p>This is the fourth and last instalment of the series of interviews with the 2021 CONCUR Test-of-Time Award recipients, which I have conducted with Nathalie Bertrand and Nobuko Yoshida's great help. (See <a href="https://processalgebra.blogspot.com/2021/06/interview-with-concur-2021-tot-award.html" target="_blank">here</a>, <a href="https://processalgebra.blogspot.com/2021/08/interview-with-concur-2021-tot-award.html" target="_blank">here</a> and <a href="https://processalgebra.blogspot.com/2021/08/interview-with-concur-2021-tot-award_23.html" target="_blank">there</a> for the previous ones.) In it, I interviewed <a href="https://www.labri.fr/perso/janin/" target="_blank">David Jani</a>n and <a href="https://www.labri.fr/perso/igw/" target="_blank">Igor Walukiewicz</a>. </p><p>I thank David and Igor for their very stimulating answers to my questions and for painting such a rich picture of the context for their award-winning work and of the subsequent developments related to it. Enjoy!<b></b></p><p>Note: The interview has been slightly edited for clarity and to correct some small typos. Thanks to <a href="http://www-sop.inria.fr/members/Ilaria.Castellani/" target="_blank">Ilaria Castellani</a> for pointing out several typos that had escaped my attention. <b><br /></b></p><p><b>Luca:</b> You receive the CONCUR ToT Award 2021 for your paper <a href="https://doi.org/10.1007/3-540-61604-7_60" target="_blank">On the Expressive Completeness of the Propositional mu-Calculus with respect to Monadic Second Order Logic</a>, which appeared at CONCUR 1996. In that article, you showed what I consider to be a fundamental result, namely that the <a href="https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus" target="_blank">mu-calculus</a> and the bisimulation-invariant fragment of <a href="https://en.wikipedia.org/wiki/Monadic_second-order_logic" target="_blank">monadic second-order logic (MSOL)</a> have the same expressiveness over transition systems. Could you tell us how you came to study that question and why do you think that such a natural problem hadn't been answered before your paper? </p><p><b>David and Igor:</b>At that time we were interested in automata characterizations of the expressive power of MSOL and the mu-calculus. In 1988 <a href="https://www.mimuw.edu.pl/~niwinski/" target="_blank">Damian Niwinski</a> has shown that over binary trees the mu-calculus and MSOL are expressively equivalent. When it appeared, the result was quite surprising, even unexpected. The two logics are not equivalent on unranked trees where the number of children of a node is not fixed. In consequence, the logics are not equivalent over the class of all transition systems. </p><p>In 1983 van Benthem showed that modal logic is equivalent to the bisimulation-invariant fragment of first-order logic. When we have learned about this result we<br />have realized that our automata models can be used to prove a similar statement<br />for the mu-calculus. <br /><br />The method of van Benthem could not be applied to MSOL, the automata based<br />method looks like the only way to prove the result. <br /><br /><b>Luca:</b> I am interested in how research collaborations start, as I like to tell "research-life stories" to PhD students and young researchers. Could you tell us how you started your collaboration?<br /><br /><b>David:</b> I came to meet Igor when he was visiting Bordeaux in fall 93, presenting his first completeness result on a proof system for the mu-calculus (LICS 93). I was myself starting a PhD considering modal logic for specifying (various forms of) nondeterminism in connection with (power)domain theory (FST&TCS 93).<br /><br />We eventually met again in Auvergnes (center of France) for the Logic Colloquium in summer 94. There, spending time in the park nearby the conference venue or walking around the volcanoes, we elaborated a notion of nondeterministic automata for the modal mu-calculus. This result can be seen as extending the notion of "disjunctive" normal form from propositional logic to the modal mu-calculus. I remember that Igor later used this result for his second completeness result for <a href="http://www.cs.cornell.edu/~kozen/" target="_blank">Kozen</a>’s proposed proof system for the mu-calculus (LICS 95). Thanks to Igor, this was for me the occasion to learn in depth the link between mu-calculus and tree automata.<br /><br />Incidentally, <a href="https://staff.science.uva.nl/j.vanbenthem/" target="_blank">Johan van Benthem</a> was also attending this Logic Colloquium and we both attend his lecture about the bisimulation-invariant fragment of FO. Although we did not yet realize we could generalize his result to MSO, this surely increased our own understanding of logic.<br /><br />Our first result (Automata for the mu-calculus) was presented at MFCS in 95 in Prague, where Igor and I met again. It could have been there, or a little later, that we eventually postulated our bisimulation-invariance result. However, proof arguments were only found later while exchanging emails. It was a bit amazing for me that we could discuss that way across Europe: email started to be heavily used only in the late 80's. In my head, Poland was far, far away from France.<br /><br />Yet our collaboration was eventually in the line of an ongoing collaboration<br />between Warsaw and Bordeaux, involving researcher like Arnold (my supervisor)<br />and Niwinski (Igor's mentor), both major specialists in the area of automata and<br />logics. Somehow, as a followup, together with Aachen (<a href="https://logic.rwth-aachen.de/People/Graedel/" target="_blank">Grädel</a> and <a href="https://www.lics.rwth-aachen.de/cms/LICS/Der-Lehrstuhl/Team/Dozierende/~ocwi/Wolfgang-Thomas/lidx/1/" target="_blank">Thomas</a>) and<br />many other sites, the GAMES European network was later created, and, almost at<br />the same time, Igor came to Bordeaux as a CNRS researcher.<br /><br /><b>Luca:</b> As you mentioned earlier, van Bentham has <a href="https://pure.uva.nl/ws/files/3800551/1170_12194y.pdf" target="_blank">shown</a> that modal logic has the same expressive power as the bisimulation-invariant fragment of first-order logic. In some sense, one may consider your main result as the extension of van Bentham's theorem to a setting with fixed-points. Could you briefly describe at a high level the challenges that fixed-points created in your work? To your mind, what was the main technical achievement or technique in your paper?<br /><br /><b>David and Igor:</b> Sure our result is similar to van Benthem's, and, as mentioned<br />above, his own presentation in 93 was very inspiring. However, his proof relies<br />on compactness of first-order logic and cannot be adapted to monadic<br />second-order logic. In our proof, we have used automata-theoretic techniques. <br /><br />In our previous works we had developed automata models for MSOL and the<br />mu-calculus on unranked trees. Every transition system is bisimulation invariant<br />to a tree obtained by the unfolding of the transition system. Crucially for our<br />result, it is also equivalent to a tree where every subtree is duplicated<br />infinitely many times. A short pumping argument shows that on such trees the two automata models are equivalent. <br /><br /><b>Luca:</b> Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? Is there any result obtained by other researchers that builds on your work and that you like in particular?<br /><br /><b>David and Igor: </b>Around that time Marco Hollenberg and Giovana D'Agostino used our automata-theoretic methods to show the uniform interpolation property for the mu-calculus. <br /><br />In collaboration with Giacomo Lenzi (postdoc in Bordeaux from Pisa), David<br />considered the bisimulation-invariant fragment of various levels of the monadic<br />quantifier alternation hierarchy. It turns out that monadic Sigma_1 corresponds to reachability properties and monadic Sigma_2 corresponds to Büchi properties, respectively the first and second levels of the mu-calculus hierarchy. <br /><br />It could be the case that all mu-calculus can be translated into monadic<br />Sigma_3 formulas -- this is true when restricting to deterministic transition<br />systems. However, with nondeterminism, such a result seems difficult to achieve. <br /><br />Incidentally, Giacomo and David also proved that adding limited counting capacity<br />to modalities yields a fixed-point calculus equivalent to the unraveling invariant<br />fragment of MSO (LICS 2001). <br /><br />In 1999, in collaboration with Erich Grädel, Igor has used similar techniques to define and study guarded fixed-point logic. Subsequently, several other fixed-point logics of this kind were proposed with the most expressive one probably being guarded negation logic with fixed points of Bárány, ten Cate, and Segoufin from 2015. These works all use automata-theoretic methods to some extent. <br /><br /><b>Luca:</b> Your paper was written while Igor was at BRICS at the University of Aarhus. Igor, what was it like to be at BRICS@Aarhus at that time? What role do<br />you think centres like BRICS played and can play in the development of theoretical computer science? Do you think that your stay at BRICS had a<br />positive impact on your future career?<br /><br /><b>Igor:</b> My stay at BRICS had definitively a beneficial impact on me. At that time BRICS was one of the most active centers world wide in theoretical computer science. Being able to see and talk to so many different people, being exposed<br />to so many different ideas, was very enriching. BRICS was a meeting place <br />allowing scientists to have a better and larger vision of our field. BRICS contributed to the development of many people involved, as well as to the excellence of Aarhus, and even Denmark as a whole, in our field.<br /><br /><b>Luca:</b> I have been brought up in the concurrency-theory tradition and I feel that bisimulation-invariant properties are the interesting ones over transition systems. Do you think that we actually "need" logics that allow one to specify properties of transition systems that are not bisimulation invariant?<br /><br /><b>David:</b> That was the idea indeed and the mu-calculus is the good logic for that. From a mathematical perspective, bisimulation is a fairly natural definition. In some sense, bisimulation equivalence is a greatest co-congruence.<br /><br />However, I always suspected that bisimulation is too fine grained as an equivalence for concurrency. When modeling realistic systems, nondeterminism arises either as controllable (angelic) or uncontrollable (demonic) choice. In this case, the right equivalence to be considered is simulation equivalence.<br /><br />The funny thing is that David Park, who "invented" bisimulation, was actually studying equivalence of J.R. Büchi's deterministic string automata where, because of determinism, bisimulation turns out to be equivalent to simulation equivalence. It is only after Matthew Hennessy and Robin Milner's work in concurrency that bisimulation was applied to nondeterministic behaviors.<br /><br /><b>Igor:</b> In the context of XML and semistructured data, bisimulation is not relevant. One of the prominent queries in XPATH is whether a value appears twice -- that is clearly not a bisimulation-invariant property. So while XPATH looks very close to PDL or the mu-calculus, many techniques and questions are very different. The other context that comes to mind is controller synthesis, where we ask for a<br />transition system of a specific shape, for example, with self-loops on certain actions. Such self loops represent invisibility of the action to the controller. <br /><br /><b>Luca:</b> What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?<br /><br /><b>David: </b>In Logic for Computer Science, there have always been two kinds of approaches: model theory that eventually led to model checking and proof theory that eventually led to typed programming languages.<br /><br />Twenty years later, aiming at designing and implementing real concurrent systems, especially for interactive arts, I realized that the latter approach was<br />(at least for me) a lot more effective. Building concurrent systems by synchronizing arbitrary sub-systems sounded for me like unstructured programming; it was essentially unmaintainable. Monads and linear types, among<br />many other approaches in typed functional programming, surely offered interesting<br />alternatives to process calculi approaches.<br /><br /><b>Igor:</b> In the context of the paper we discuss here, I am surprised by developments around the model-checking problem for the mu-calculus. After some years of relative calm, Calude, Jain, Khoussainov, Li and Stephan have made an important breakthrough in 2017. Yet, despite big activity after this result, the research on the problem seems to have hit one more barrier. Another old prominent problem is decidability of the alternation hierarchy for the mu-calculus. The problem is: given a formula and a number of alternations between the least and the greatest fixed-points, decide if there is an equivalent formula with this number of alternations. Even when the number of alternations is fixed we do not know the answer. Among others, Thomas Colcombet and Christof Loeding have done very interesting work on this subject.<br /><br /><b>Luca:</b> What advice would you give to a young researcher who is keen to start working on topics related to automata theory and logic in computer science? <br /><br /><b>David:</b> From the distance, our result sounds to me as a combination of both technique and imagination. Technique for mastering known results and imagination for finding original open problems, especially between research fields that are not (yet) known to be deeply related. As a matter of fact, I felt lucky finding such a fresh open problem that was (probably) a lot easier to solve than many other well-known hard problems.<br /><br />Technique comes from hard work. It is obviously essential but somehow easy to teach and evaluate in academia. Imagination comes from curiosity. It is still essential but a lot more difficult to teach. So young researchers must develop by themselves their own imagination and curiosity.<br /><br />In the automata-theory branch of logic in computer science, the remaining open<br />problems seem fairly hard, so I believe that it is the imagination of young researchers that will make the difference for setting up new interesting directions of research, especially those who are ready to look aside, towards other areas of<br />logic in computer science and, because it can be a considerable source of<br />motivation, funny applications.<br /><br /><b>Igor:</b> Naturally, the field is much broader these days than it was 25 years ago. It is<br />crucial to master some techniques. For this, working on variations of already solved problems is a good method. Yet, I think it is important to escape<br />the cycle of constant modifications of existing problems and their solutions. <br />I would suggest that, at some moment, one should find an important open<br />problem that one is passionate about and should spend a considerable effort on<br />it. I admit that this is a matter of a taste, personality, and having a sufficiently<br />comfortable situation to afford such a risk. Another good option is to look at frontiers with other areas: distributed computing, semantics, control theory, security. <br /><br /></p><br />Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-38317682191003049092021-08-23T09:44:00.000+00:002021-08-23T09:44:16.190+00:00Interview with CONCUR 2021 ToT Award Recipients: Ahmed Bouajjani and Javier Esparza<p><i>I am delighted to post <a href="http://people.rennes.inria.fr/Nathalie.Bertrand/" target="_blank">Nathalie Bertrand</a>'s splendid interview with <a href="https://qonfest2021.lacl.fr/test-of-time.php" target="_blank">CONCUR 2021 Test-of-Time Award</a> recipients <a href="https://www.irif.fr/~abou/" target="_blank">Ahmed Bouajjani</a> and <a href="https://www7.in.tum.de/~esparza/" target="_blank">Javier Esparza</a>. (Ahmed and Javier receive the award for a paper their co-authored with the late <a href="https://hsb2019.fit.vutbr.cz/oded_maler.php" target="_blank">Oded Maler</a>.)<br /><br />Thanks to Ahmed and Javier for their answers and to Nathalie for conducting such an interesting interview, which is rich in information on the technical context for, and impact of, their work as well as on their research collaborations over the years. I now leave the floor to Nathalie and her interviewees. Enjoy! </i><br /></p><p>This post is devoted to the interview I was honored to conduct with Ahmed Bouajjani and Javier Esparza for <a href="https://doi.org/10.1007/3-540-63141-0_10" target="_blank">their paper</a> with Oded Maler on reachability in pushdown automata.<br /><br /><b>Nathalie: </b>You receive the CONCUR ToT Award 2021 for your paper with Oded Maler <a href="https://doi.org/10.1007/3-540-63141-0_10" target="_blank">Reachability Analysis of Pushdown Automata: Application to Model-Checking</a>, which appeared at CONCUR 1997. In that article, you develop symbolic techniques to represent and manipulate sets of configurations of pushdown automata, or even of the broader class of alternating pushdown systems. The data structure you define to represent potentially infinite sets of configurations is coined alternating multi-automata, and you provide algorithms to compute the<br />set of predecessors (pre*) of a given set of configurations. Could you briefly explain to our readers what alternating multi-automata are?<br /><br /><b>Ahmed:</b> The paper is based on two ideas. The first one is to use finite automata as a data structure to represent infinite sets of configurations of the pushdown automaton. We called them <i>multi-automata</i> because they have multiple initial states, one per control state of the pushdown automaton, but there is nothing deep there. The second idea is that this representation is closed under the operation of computing predecessors, immediate or not. So, given a multi-automaton representing a set of configurations, we can compute another multi-automaton representing all their predecessors. If you compute first the immediate predecessors, then their immediate predecessors, and so on, you don't converge, because your automata grow bigger and bigger. The surprising fact is that you can compute <i>all</i> predecessors in one go by just adding transitions to the original<br />automaton, without adding any new states. This guarantees termination. Later we called this process ``saturation''.<br /><br />Once you can compute predecessors, it is not too difficult to obtain a model-checking algorithm for LTL model checking. But for branching-time logics you must also be able to compute intersections of sets of configurations. That's where alternation kicks in, we use it to represent intersections without having to add new states.<br /><br /><b>Nathalie:</b> Could you also tell us how you came to study the question addressed in your award-winning article? Which of the results in your paper did you find most surprising or challenging?<br /><br /><b>Javier:</b> In the late 80s and early 90s many people were working on symbolic model-checking, the idea of using data structures to compactly represent sets of configurations. BBDs for finite-state model-checking were a hot topic, and for quite a few years dominated CAV. BDDs can be seen as acyclic automata, and so it was natural to investigate general finite automata as data structure for infinite-state systems. Pierre Wolper and his group also did very good work on that.<br /><br />About your second question, when I joined the team Ahmed and Oded had already been working on the topic for a while, and they had already developed the saturation algorithm. When they showed it to me I was blown away, it was so beautiful. A big surprise.<br /><br /><b>Nathalie:</b> In contrast to most previous work, your approach applied to model checking of pushdown systems treats in a uniform way linear-time and branching time logics. Did you apply this objective in other contributions?<br /><br /><b>Javier:</b> I didn't. The reason is that I was interested in concurrency, and when you bring together concurrency and procedures even tiny fragments of branching-time logics become undecidable. So I kind of stuck to the linear-time case. Did you work on branching-time, Ahmed?<br /><br /><b>Ahmed:</b> Somehow yes (although it is not precisely about linear vs. branching time properties), in the context of Regular Model Checking, a uniform framework for symbolic analysis of infinite-state systems using automata-based data structures. There, we worked on two versions, one based on word automata for systems where configurations can be encoded as words or vectors of words, such as stacks, queues, etc., and another one based on tree automata for configurations of a larger class of systems like heap manipulating programs, parametrized systems with tree-like architectures, etc. The techniques we developed for both cases are based on the same principles.<br /><br /><b>Nathalie:</b> As it is often the case, the paper leaves some open questions. For instance, I believe, the precise complexity of verification of pushdown systems against CTL specifications is PSPACE-hard and in EXPTIME. Did you or others close this gap since? Did your techniques help to establish the precise complexity?<br /><br /><b>Ahmed:</b> In our paper we showed that model checking the alternating modal<br />mu-calculus is EXPTIME-hard. CTL is less expressive, and it was the most popular logic in the verification community at the time, so it was natural to ask if it had lower complexity. <br /><br /><b>Javier:</b> Yes, as a first step in the paper we showed that a fragment of CTL, called EF, had PSPACE complexity. But I made a mistake in the proof, which was later found by Igor Walukiewicz. Igor cracked the problem in a paper at FSTTCS'00. It turns out that EF is indeed PSPACE-complete (so at least we got the result right!), and full CTL is EXPTIME-complete. I wish Igor had used our technique, but he<br />didn't, he applied the ideas of his beautiful CAV'96 paper on parity pushdown games.<br /><br /><b>Nathalie:</b> It is often interesting to understand how research collaborations start as it can be inspiring to PhD students or colleagues. Could you tell us how you started your collaboration on the award-winning paper? Did you continue working together (on a similar topic or on something totally different) after 1997?<br /><br /><b>Ahmed:</b> Javier and I first met in Liege for CAV 95. French universities have this program that allows us to bring foreign colleagues to France for a month as invited professors, and I invited Javier to Grenoble in 96.<br /><br /><b>Javier:</b> It was great fun; Verimag was a fantastic place to do verification, we both liked cinema, Ahmed knew all restaurants, and the Alps were beautiful. Ahmed invited me again to Grenoble in 97. This time I came with my wife, and we again had a great time.<br /><br />When I arrived in Grenoble in 96 Ahmed and Oded had already written most of the work that went into the paper. My contribution was not big, I only extended the result to the alternation-free mu-calculus, which was easy, and proved a matching lower bound. I think that my main contribution came <b>after</b> this paper. Ahmed and Oded were too modest, they thought the result was not so important, but I found it not only beautiful, I thought it'd be great implement the LTL part,<br />and build a model checker for programs with procedures. We could do that thanks to Stefan Schwoon, who started his PhD in Munich around this time--he is now at Paris-Saclay---and was as good a theoretician as a tool builder. Around 2000 he implemented a symbolic version of the algorithms in MOPED, which was quite successful.<br /><br /><b>Ahmed:</b> In 99 I moved to LIAFA in Paris, and I remember your kids were born.<br /><br /><b>Javier:</b> Yes, you sent my wife beautiful flowers!<br /><br /><b>Ahmed:</b> But we kept in touch, and we wrote a paper together in POPL'03 with my PhD student Tayssir Touili, now professor in Paris. We extended the ideas of the CONCUR paper to programs with both procedures and concurrency. Other papers came, the last in 2008.<br /><br /><b>Javier:</b> And Ahmed is visiting Munich next year, pandemic permitting, so I hope there'll be more.<br /><br /><b>Nathalie:</b> How would you say this award-winning paper influenced your later work? Did any of your subsequent research build explicitly on it?<br /><br /><b>Ahmed:</b> This paper was the first of many I have co-authored on verification of infinite-state systems using automata. All of them use various automata classes to represent sets of configurations, and compute reachable configurations by iterative application of automata operations. We call these procedures accelerations; instead of computing a fixed point of a function by repeated iteration, you "jump" to the fixed point after finitely many steps, or at least converge faster. Accelerations were implicitly present in the CONCUR'97 paper. They have been also used by many other authors, for example Bernard Boigelot and Pierre Wolper.<br /><br />My first paper on accelerations was with Peter Habermehl, my PhD student at the time and now at IRIF. We worked on the verification of systems communicating through queues, using finite automata with Presburger constraints as data structure. Then came several works on communicating systems with my student Aurore Annichini and Parosh Abdulla and Bengt Jonsson from Uppsala. As a natural continuation, with the Uppsala group and my student Tayssir Touili we developed the framework of Regular Model Checking. And then, with Peter Habermehl, Tomas Vojnar and Adam Rogalewicz from TU Brno, we extended Regular Model Checking to Abstract Regular Model Checking, which proved<br />suitable and quite effective for the analysis of heap manipulating programs.<br /><br />We also applied the CONCUR'97 results to the analysis of concurrent programs. The first work was a POPL'03 paper with Javier, Tayssir, and me on an abstraction framework. Two years later, Shaz Qadeer and Jakob Rehof proposed bounded-context switch analysis for bug detection. That paper created a line of research, and we contributed to it in many ways, together with Shaz, Mohamed Faouzi Atig, who was my student then, and is now Professor at Uppsala, and others.<br /><br /><b>Javier:</b> The CONCUR'97 paper was very important for my career. As I said before, it directly led to MOPED, and later to jMOPED, a version of MOPED for Java programs developed by Stefan Schwoon and Dejvuth Suwimonteerabuth. Then, Tony Kucera, Richard Mayr, and I asked ourselves if it was possible to extend probabilistic verification to pushdown systems, and wrote some papers on the topic, the first in LICS'04. This was just the right moment, because at the same time Kousha Etessami and Mihalis Yannakakis started to write brilliant papers on recursive Markov chains, an equivalent model. The POPL'03 paper with Ahmed and Tayssir also came, and it triggered my work on Newtonian program analysis with two very talented PhD students, Stefan Kiefer, now in Oxford, and Michael Luttenberger, now my colleague at TUM. So the CONCUR'97 paper was at the root of a large part of my work of the next 15 years.<br /><br /><b>Nathalie: </b>Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising?<br /><br /><b>Javier:</b> After implementing MOPED, Stefan worked with Tom Reps on an extension to weighted pushdown automata, the Weighted Pushdown Library. Tom and Somesh Jha also found beautiful applications to security. This was great work. I was also very impressed by the work of Luke Ong and his student Matthew Hague. In 97 Ahmed and I tried to apply the saturation method to the full mu-calculus but failed, we thought it couldn't be done. But first Thierry Cachat gave a saturation algorithm for Büchi pushdown games, then Luke, Matthew cracked the mu-calculus problem, and then they even extended it to<br />higher-order pushdown automata, together with Arnaud Carayol, Olivier Serre, and others. That was really surprising.<br /><br /><b>Ahmed:</b> I agree. I'd also mention Qadeer and Rehof's TACAS'05 paper. They built on our results to prove that context-bounded analysis of concurrent programs is decidable. They initiated a whole line of research.<br /><br /><b>Nathalie:</b> What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?<br /><br /><b>Javier:</b> Ten years ago I've had said the complexity of the reachability problem for Petri nets and of solving parity games, but now the first one is solved and the second almost solved! Now I don't have a specific problem, but in the last years I've been working on parameterized systems with an arbitrary number of agents, and many aspects of the theory are still very unsatisfactory. Automatically proving a mutual exclusion algorithm correct for a few processes was already routine 20 years ago, but proving it for an arbitrary number is still very much an open problem.<br /><br /><b>Ahmed:</b> I think that invariant and procedure summary synthesis will remain hard and challenging problems that we need to investigate with new approaches and techniques. It is hard to discover the right level of abstraction at which the invariant must be expressed, which parts of the state are involved and how they are related. Of course the problem is unsolvable in general but finding good methodologies on how to tackle it depending on the class of programs is an important issue. I think that the recent emergence of data-driven approaches is<br />promising. The problem is to develop well principled methods combining data-driven techniques and formal analysis that are efficient and that offer well understood guarantees.<br /><br /><b>Nathalie:</b> Would you have an anecdote or a tip from a well-established researcher to share to PhD students and young researchers?<br /><br /><b>Javier:</b> Getting this award reminded me of the conference dinner at CAV 12 in St. Petersburg. I ended up at a table with some young people I didn't know. The acoustics was pretty bad. When the CAV Award was being announced, somebody at the table asked "What's going on?", and somebody else answered "Not much, some senior guys getting some award". Never take yourself very seriously ...<br /><br /><b>Nathalie:</b> Oded Maler passed away almost 3 years ago. Do you have any memory of him to share with our readers?<br /><br /><b>Ahmed:</b> Oded was very amused by the number of citations. He used to say "Look at all the damage we've done."<br /><br /><b>Javier:</b> Yes, Oded had a wonderful sense of humor, very dry and deadpan. When I arrived in Grenoble it took me a few days to learn how to handle it! I miss it very much.<br /><br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-70463892729418362202021-08-11T09:38:00.001+00:002021-08-11T09:38:26.770+00:00The First: A Movie <p>I had the great pleasure to watch <a href="https://pantar.com/" target="_blank">Ali Hossaini</a> and <a href="http://www.lucavigano.com/" target="_blank">Luca Viganò</a>'s short movie "<a href="https://www.nationalgallery.org.uk/national-gallery-x/the-ai-gallery" target="_blank">The First</a>" that has been released by National Gallery X. "The First" is a coproduction of <a href="https://www.tas.ac.uk/" target="_blank">UKRI TAS Hub</a>, <a href="https://rusi.org/" target="_blank">RUSI </a>and <a href="https://www.nationalgallery.org.uk/national-gallery-x" target="_blank">National Gallery X</a>. It was produced as a keynote for <a href="https://www.tas.ac.uk/bigeventscpt/trusting-machines/" target="_blank">Trusting Machines?</a>, a conference on how to develop trustworthy AI. </p><p>For the little that it may be worth, I strongly recommend the movie. Do watch also the <a href="https://vimeo.com/577412746" target="_blank">conversation</a> between National Gallery X co-director Ali Hossaini and Luca Viganò, possibly before enjoying a second viewing of the movie. You can also read the paper "<a href="https://arxiv.org/pdf/1807.06078.pdf" target="_blank">Gnirut: The Trouble With Being Born Human In An Autonomous World</a>" mentioned in that conversation. </p><p>I fully subscribe to Luca Viganò's vision of using artistic tools to explain computer science concepts to the public, whose members will have to make use of the technological artifacts based on those concepts. Indeed, we live in a world in which technologists will increasingly have to be great humanists. IMHO, we are lucky to have people like Luca Viganò, who is also a playwright, paving the way in connecting "<a href="https://en.wikipedia.org/wiki/The_Two_Cultures" target="_blank">The Two Cultures</a>". (In case any of you is interested, I recommend Luca Viganò's <a href="https://us02web.zoom.us/rec/play/3uNdz1F0g1JCAir0C10Y3_jVs7k6fJgrIwr5RomnzBJGTjqBMOYv6SJgD2jINwMTuBvx-CSsHclof5Vn.29XNpJA7FKbfL5dG?autoplay=true&startTime=1614787555000" target="_blank">GSSI+ICE-TCS webinar</a>.)</p><p> </p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-5510032070268167682021-08-06T21:36:00.002+00:002021-08-06T21:37:04.030+00:00Interview with CONCUR 2021 ToT Award Recipients: Uwe Nestmann and Benjamin Pierce<p>I am pleased to re-post <a href="https://www.imperial.ac.uk/people/n.yoshida" target="_blank">Nobuko Yoshida</a>'s splendid <a href="http://mrg.doc.ic.ac.uk/concur-tot/ " target="_blank">interview</a> with CONCUR 2021 Test-of-Time Award recipients <a href="https://www.mtv.tu-berlin.de/nestmann/" target="_blank">Uwe Nestmann</a> and <a href="https://www.cis.upenn.edu/~bcpierce/" target="_blank">Benjamin Pierce</a>. I thoroughly enjoyed reading it and learnt much from the many pearls of wisdom that pepper the interview. </p><p>Thanks to Benjamin and Uwe for their answers and to Nobuko for conducting such an inspiring interview. Enjoy!<br /></p><p><br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-49132880962088543392021-06-24T08:16:00.000+00:002021-06-24T08:16:15.896+00:00The detectEr runtime-verification tool for Erlang programs<p>Thanks to the huge amount of excellent work done by <a href="https://duncanatt.github.io/" target="_blank">Duncan Paul Attard</a> and <a href="http://staff.um.edu.mt/afra1/" target="_blank">Adrian Francalanza</a>, we now have a tutorial on detectEr that some of you might want to check out. See <a href="https://duncanatt.github.io/detecter/index.html">this web page</a> for all the material, tool download and links to the videos of the tutorial Duncan delivered at the <a href="https://www.discotec.org/2021/tutorials" target="_blank">DisCoTec 2021 Tutorial Day</a>. </p><p>detectEr is a runtime verification tool for asynchronous component systems that run on the <a href="https://blog.erlang.org/a-brief-BEAM-primer/" target="_blank">Erlang Virtual Machine</a>. It also supports monitoring systems that can execute outside of the EVM, so long as these can produce traces that are formatted in a way that is parsable by detectEr. The tool itself is developed in <a href="https://www.erlang.org/" target="_blank">Erlang</a>, and is the product of five years of theoretical and practical development. (Erlang is a programming language used to build massively scalable soft real-time systems with requirements on high availability.) </p> <p>Enjoy!</p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-16648748220183207312021-06-18T16:37:00.001+00:002021-06-20T11:16:42.575+00:00Interview with CONCUR 2021 ToT Award recipients, Part 1: Rajeev Alur, Thomas Henzinger, Orna Kupferman and Moshe Vardi<p>Last year, the CONCUR conference series inaugurated its Test-of-Time Award, whose purpose is to recognise important achievements in Concurrency Theory that were published at the CONCUR conference and have stood the test of time. This year, the following <a href="https://qonfest2021.lacl.fr/test-of-time.php" target="_blank">four papers</a> were chosen to receive the CONCUR Test-of-Time Awards for the periods 1994–1997 and 1996–1999 by a jury consisting of Rob van Glabbeek (chair), Luca de Alfaro, Nathalie Bertrand, Catuscia Palamidessi, and Nobuko Yoshida: </p><ul style="text-align: left;"><li> David Janin and Igor Walukiewicz. <a href="http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=F31F028FFA1E754B87E7378032EAD6E7?doi=10.1.1.35.9156&rep=rep1&type=pdf" target="_blank">On the Expressive Completeness of the Propositional mu-Calculus with respect to Monadic Second Order Logic</a>. </li><li>Uwe Nestmann and Benjamin C. Pierce. <a href="http://www.cis.upenn.edu/~bcpierce/papers/choice.ps" target="_blank">Decoding Choice Encodings</a>.</li><li>Ahmed Bouajjani, Javier Esparza, and the late Oded Maler. <a href="http://www-verimag.imag.fr/~maler/Papers/pda.pdf" target="_blank">Reachability Analysis of Pushdown Automata: Application to Model-checking</a>.</li><li>Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. <a href="https://doi.org/10.1007/BFb0055622" target="_blank">Alternating Refinement Relations</a>. <br /></li></ul><p>Last year, I interviewed the <a href="http://concur2020.forsyte.at/test-of-time.html" target="_blank">CONCUR 2020 Test-of-Time Award recipients</a> and was asked by Javier Esparza (chair of the CONCUR SC) and Ilaria Castellani (outgoing chair of the IFIP WG 1.8 on Concurrency Theory) to do the same with the current batch of awardees. (In passing, let me thank <a href="http://people.rennes.inria.fr/Nathalie.Bertrand/" target="_blank">Nathalie Bertrand</a> and <a href="https://www.imperial.ac.uk/people/n.yoshida" target="_blank">Nobuko Yoshida</a> for their kind help with the interviews!)<br /></p><p>This post is devoted to the interview I conducted via email with <a href="https://www.cis.upenn.edu/~alur/" target="_blank">Rajeev Alur</a>, <a href="http://pub.ist.ac.at/~tah/" target="_blank">Thomas A. Henzinger</a>, <a href="https://www.cs.huji.ac.il/~ornak/" target="_blank">Orna Kupferman</a> and <a href="https://www.cs.rice.edu/~vardi/" target="_blank">Moshe Y. Vardi</a>. Reading the answers I received from that dream team of colleagues was like a masterclass for me and I trust that their thoughts on their award-winning paper will be of interest to many of the readers of this blog. Enjoy!<br /></p><p><b>Luca:</b> You receive the CONCUR ToT Award 2021 for your paper <a href="https://doi.org/10.1007/BFb0055622" target="_blank">Alternating Refinement Relations</a>, which appeared at CONCUR 1998. In that article, you gave what I consider to be a fundamental contribution, namely the introduction of refinement relations for alternating transition systems. Could you briefly explain to our readers what alternating transition systems are? Could you also tell us how you came to study the question addressed in your award-winning article and why you focused on simulation- and trace-based refinement relations? Which of the results in your paper did you find most surprising or challenging? </p><p><b>Answer:</b> When we model a system by a graph, our model abstracts away some details of the system. In particular, even when systems are deterministic, states in the model may have several successors. The nondeterminism introduced in the model often corresponds to different actions taken by the system when it responds to different inputs from its environment. Indeed, a transition in a graph that models a composite system corresponds to a step of the system that may involve some components. Alternating transition systems (ATSs) enable us to model composite systems in more detail. In an ATS, each transition corresponds to a possible move in a game between the components, which are called agents. In each move of the game, all agents choose actions, and the successor state is deterministically determined by all actions. Consequently, ATSs can distinguish between collaborative and adversarial relationships among components in a composite system. For example, the environment is typically viewed adversarially, meaning that a component may be required to meet its specification no matter how the environment behaves. </p><p>In an earlier <a href="https://www.cis.upenn.edu/~alur/Jacm02.pdf" target="_blank">paper</a>, some of us introduced ATSs and Alternating Temporal Logics, which can specify properties of agents in a composite system. The CONCUR 1998 paper provided refinement relations between ATSs which correspond to alternating temporal logics. Refinement is a central issue in a formal approach to the design and analysis of reactive systems. The relation “I refines S '' intuitively means that system S has more behaviors than system I. It is useful to think about S being a specification and I an implementation. Now, if we consider a composite implementation I||E and specification S||E and we want to check that the component I refines the component S, then the traditional refinement preorders are inappropriate, as they allow I to achieve refinement of I||E with respect to S||E by constraining its environment E. Alternating refinement relations are defined with respect to ATSs that model the interaction among the underlying components, and they enable us to check, for example, that component I has fewer behaviors than component S no matter how component E behaves. They are called “alternating” because refinement may restrict implementation actions but must not restrict environment actions. In other words, refinement may admit fewer system actions but, at the same time, more environment actions. </p><p>It was nice to see how theoretical properties of preorders in the traditional setting are carried over to the game setting, and so are the results known then about the computational price of moving to a game setting. First, the efficiency of the local preorder of simulation with respect to the global preorder of trace containment is maintained. As in the traditional setting, alternating simulation can be checked in polynomial time, whereas alternating trace-containment is much more complex. Second, the branching vs. linear characterizations of the two preorders is preserved: alternating simulation implies alternating trace containment, and the logical characterization of simulation and trace-containment by CTL and LTL, respectively, is carried over to their alternating temporal logics counterparts. The doubly-exponential complexity of alternating trace containment, as opposed to the PSPACE complexity of trace containment, is nicely related to the doubly-exponential complexity of LTL synthesis, as opposed to its PSPACE model-checking complexity,</p><p> <b>Luca:</b> In your paper, you give logical characterisations of your alternating refinement relations in terms of fragments of alternating temporal logic. Logical characterisations of refinement relations are classic results in our field and I find them very satisfying. Since I teach a number of those results in my courses, I'd be interested in hearing how you would motivate their interest and usefulness to a student or a colleague. What would your "sales pitch" be? </p><p><b>Answer:</b> There is extensive research on the expressive power of different formalisms. Logical characterization of refinement relations tells us something about the distinguishing power of formalisms. For example, while the temporal logic CTL* is more expressive than the temporal logic CTL, the two logics have the same distinguishing power: if you have two systems and can distinguish between them with a CTL* formula (that is, your formula is satisfied only in one of the systems), then you should be able to distinguish between the two systems also with a CTL formula. Moreover, while CTL is not more expressive than LTL, we know that CTL is “more distinguishing” than LTL. These results have to do with the logical characterizations of trace containment and simulation. The distinguishing power of a specification formalism is useful when we compare systems, in particular an implementation and its abstraction: if we know that the properties we care about are specified in some formalism L, and our system refines the abstraction according to a refinement relation in which the satisfaction of specifications in L is preserved, then we can perform verification on the abstraction.</p><p> <b>Luca:</b> I am interested in how research collaborations start, as I like to tell "research-life stories" to PhD students and young researchers of all ages. Could you tell us how you started your collaboration on the award-winning paper? </p><p><b>Answer:</b>Subsets of us were already collaborating on other topics related to reactive models and model checking, and all of us shared a common belief that the field was in need to move from the limited setting of closed systems to a more general setting of open systems, that is, systems that interact with an environment. Open systems occur not only when the environment is fully or partly unknown, but also when a closed system is decomposed into multiple components, each of them representing an open system. To build “openness” into models and specifications as first-class citizens quickly leads to the game-theoretic (or “alternating”) setting. It was this realization and the joint wish to provide a principled and systematic foundation for the modeling and verification of open systems which naturally led to this collaboration.</p><p> <b>Luca:</b> Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? Which of your subsequent results on alternating transition systems and their refinement relations do you like best? Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising? </p><p><b>Answer: </b>Various subsets of us pursued multiple research directions that developed the game-theoretic setting for modeling and verification further, and much remains to be done. Here are two examples. First, the game-theoretic setting and the alternating nature of inputs and outputs are now generally accepted as providing the proper semantic foundation for interface and contract formalisms for component-based design. Second, studying strategic behavior in multi-player games quickly leads to the importance of probabilistic behavior, say in the form of randomized decisions and strategies, of equilibria, when players have non-complementary objectives, and of auctions, when players need to spend resources for decisions. All of these are still very active topics of research in computer-aided verification, and they also form a bridge to the algorithmic game theory community. </p><p><b>Luca:</b> One can view your work as a bridge between concurrency theory and multi-agent systems. What impact do you think that your work has had on the multi-agent-system community? And what has our community learnt from the work done in the field of multi-agent systems? To your mind, what are the main differences and points of contact in the work done within those communities? </p><p><b>Answer:</b> Modeling interaction in multi-agent systems is of natural interest to planning problems studied in the AI community. In 2002, the <a href="http://www.ifaamas.org/index.html" target="_blank">International Foundation for Autonomous Agents and Multiagent Systems</a> (IFAAMAS) was formed and the annual <a href="https://aamas2021.soton.ac.uk/" target="_blank">International Conference on Autonomous Agents and Multiagent Systems</a> (AAMAS) was launched. The models, logics, and algorithms developed in the concurrency and formal methods communities have had a strong influence on research presented at AAMAS conferences over the past twenty years. Coincidentally, this year our <a href="https://www.cis.upenn.edu/~alur/Jacm02.pdf" target="_blank">paper on Alternating-Time Temporal Logic</a> was chosen for the <a href="http://www.ifaamas.org/award-influential.html#:~:text=IFAAMAS%3A%20Awards%3A%20Influential%20Paper&text=The%20Influential%20Paper%20Award%20seeks,lasting%20contributions%20to%20the%20field." target="_blank">IFAAMAS Influential Paper Award</a>. </p> <b>Luca:</b> What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved? <p><b>Answer:</b>Research on formal verification and synthesis, including our paper, assumes that the model of the system is known. Reinforcement learning has emerged as a promising approach to the design of policies in scenarios where the model is not known and has to be learned by agents by exploration. This leads to an opportunity for research at the intersection of reactive synthesis and reinforcement learning. A potentially promising direction is to consider reinforcement learning for systems with multiple agents with both cooperative and adversarial interactions. </p><p>The realization that reactive systems have to satisfy their specifications in all environments has led to extensive research relating formal methods with game theory. Our paper added alternation to refinement relations. The transition from one to multiple players has been studied in computer science in several other contexts. For the basic problem of reachability in graphs, it amounts to moving from reachability to alternating reachability. We recently studied this shift in other fundamental graph problems, like the generation of weighted spanning trees, flows in networks, vertex covers, and more. In all these extensions, we consider a game between two players that take turns in jointly generating the outcome. One player aims at maximizing the value of the outcome (e.g., maximize the weight of the spanning tree, the amount of flow that travels in the network, or the size of the vertex cover), whereas the second aims at minimizing the value. It is interesting to see how some fundamental properties of graph algorithms are lost in the alternating setting. For example, following a greedy strategy is not beneficial in alternating spanning trees, optimal strategies in alternating flow networks may use fractional flows, and while the vertex-cover problem is NP-complete, an optimal strategy for the maximizer player can be found in polynomial time. Many more questions in this setting are still open. </p><p><b>Luca:</b> What advice would you give to a young researcher who is keen to start working on topics related to alternating transition systems and logics? </p><b>Answer:</b> One important piece of advice to young researchers is to question the orthodoxy. Sometimes it is necessary to learn everything that is known about a topic but then take a step back, look at the bigger picture, reexamine some of the fundamental assumptions behind the established ways of thinking, change the models that everyone has been using, and go beyond the incremental improvement of previous results. This is particularly true in formal methods, where no single model or approach fits everything. And young researchers stand a much better chance of having a really fresh new thought than those who have been at it for many years. Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-90522955081629811092021-06-01T21:42:00.001+00:002021-06-01T21:42:32.457+00:00Frank P. Ramsey on research and publication rates<p>Spurred by the excellent 1978 radio programme <a href="https://sms.cam.ac.uk/media/20145" target="_blank">'Better than the Stars'</a> by <a href="https://en.wikipedia.org/wiki/Hugh_Mellor" target="_blank">D. H. Mellor</a> about <a href="https://plato.stanford.edu/entries/ramsey/" target="_blank">Frank Ramsey</a> and by the <a href="https://traffic.libsyn.com/secure/philosophybites/Cheryl_Misak_on_Frank_Ramsey_and_Ludwig_Wittgenstein.mp3" target="_blank">Philosophy Bites interview with Cheryl Misak on Frank Ramsey and Ludwig Wittgenstein</a>, I started reading <a href="https://www.cherylmisak.com/" target="_blank">Cheryl Misak</a>'s <a href="https://global.oup.com/academic/product/frank-ramsey-9780198755357?cc=is&lang=en&" target="_blank">biography of Frank Ramsey</a>. (FWIW, I strongly recommend the radio programme, the podcast and the book.)<br /></p><p>The following quote from pages 169-170 of Cheryl Misak's book describes Ramsey's views on publications and research, as stated in a letter to his father Arthur:<br /></p><div style="margin-left: 40px; text-align: left;">Arthur tried a different tack, suggesting that Frank was going to be in trouble for wasting all this time on analysis, rather than on his career. On 24 September, in what seems to be his last letter home before he left Vienna, Frank wrote: </div><blockquote style="margin-left: 80px; text-align: left;">I don’t see how there can be any such inquisition into my conduct in Vienna as you suppose seem to want to guard against.... No one can suppose that you can’t research for six months without having a paper ready by the end. If everyone wrote a paper every six months the amount of trivial literature would swell beyond all bounds. Given time I shall produce a good paper. But if I hurry it will be ill written and unintelligible and unconvincing. <br /></blockquote><blockquote style="margin-left: 80px; text-align: left;">It seems to me perfectly proper to spend a scholarship being analysed, as it is likely to make me cleverer in the future, and discoveries of importance are made by remarkable people not by remarkable diligence. </blockquote><div style="margin-left: 40px; text-align: left;"> While it may not be persuasive that psychoanalysis makes one cleverer, Frank was prescient that the numbers of journal articles would eventually swell and he was right that diligence isn't enough to produce discoveries of importance.</div><div style="margin-left: 40px; text-align: left;"> </div><div style="text-align: left;">Of course, academia has changed since those times and I do value "remarkable diligence". However, I will try to remember Ramsey's words next time someone proposes to make academic hirings and promotions conditional to having a certain number of papers or citations or whatever per year on average. <br /></div>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com0tag:blogger.com,1999:blog-27705661.post-88053905531924855482021-05-26T19:04:00.000+00:002021-05-26T19:04:00.117+00:00Course on Ethics and Accountability in Computer Science<p>About one year ago, I became aware of the course "Ethics and Accountability in Computer Science" designed and taught by <a href="https://riceacademy.rice.edu/junior-fellows/dr-rodrigo-ferreira" target="_blank">Rodrigo Ferreira</a> and <a href="https://www.cs.rice.edu/~vardi/" target="_blank">Moshe Y. Vardi</a> at Rice University. The goals and high-level structure of the course, as well as its context, are described in an informative and thoughtful <a href="https://www.cs.rice.edu/~vardi/papers/sigcse21.pdf" target="_blank">paper</a> by Moshe and Rodrigo that appears in the <a href="https://dl.acm.org/doi/proceedings/10.1145/3408877" target="_blank">Proceedings of the 52nd ACM Technical Symposium on Computer Science Education (SIGCSE ’21)</a>, which I strongly recommend. You can also read a <a href="https://www.pdcnet.org/tej/content/tej_2021_0999_3_31_87" target="_blank">journal paper</a> reporting on one of their course assignments, which was designed to make students focus on practising <a href="https://medium.com/@the_jennitaur/how-to-do-nothing-57e100f59bbb" target="_blank">"deep attention"</a> in the sense of artist and academic <a href="https://www.jennyodell.com/" target="_blank">Jenny Odell</a>.</p><p>I was smitten by the underlying tenet for their course, namely that "social justice is the single most important issue confronting computer science students today." That tenet is also very much in line with a reflection on the impact that digital technology has on social justice that the <a href="https://www.gssi.it/institute/organization" target="_blank">Scientific Advisory Board of the Gran Sasso Science Institute</a> asked the Computer Science group at that institute to undertake. Therefore, after having invited Rodrigo to deliver a <a href="http://www.google.com/url?q=http%3A%2F%2Ficetcs.ru.is%2Fwebinars%2Fdeep_ethics.mp4&sa=D&sntz=1&usg=AFQjCNH9ux4zX7PThxWzwoNa_yyZNa-ILA" target="_blank">webinar on the course</a> at the <a href="https://sites.google.com/gssi.it/csgssi/seminars-and-events/joint-ice-tcs-csgssi-virtual-seminar" target="_blank">ICE-TCS+GSSI webinar series</a>, I decided that, as an experiment, I would offer a version of the Rice University course to master students in computer science, language technology and software engineering at Reykjavik University during our spring semester 2021. </p><p>Mine was a foolhardy decision for a variety of reasons. However, I have always believed that computer scientists should strive to be the 21st century Renaissance men and women, and bridge the gap between C. P. Snow's <a href="https://en.wikipedia.org/wiki/The_Two_Cultures" target="_blank">"two cultures"</a>. Indeed, to quote <a href="https://ptolemy.berkeley.edu/~eal/" target="_blank">Edward A. Lee</a> freely, to my mind technologists ought to be amongst the greatest humanists of our age. Despite my other commitments, offering a version of the Ferreira-Vardi course at Reykjavik University felt like the right thing to do at this time. </p><p>I taught the course over twelve weeks to a varied group of eight students, in cooperation with <a href="http://claudiopedica.com/" target="_blank">Claudio Pedica</a>. Thanks to the constant support I received from Rodrigo Ferreira, I lived to tell the tale and I hope that I managed to do some justice to the truly excellent course that Moshe and Rodrigo put together. Having a dream team of students with a variety of cultural backgrounds made the course extremely interesting and a learning experience for me. I had to refresh my memory of the philosophy I studied at high school in Italy in a previous life, learn some modern moral philosophy I had not met at school (such as the work by <a href="https://plato.stanford.edu/entries/anscombe/" target="_blank">Elisabeth Anscombe</a> and <a href="https://plato.stanford.edu/entries/philippa-foot/" target="_blank">Philippa Foot</a>, amongst others), read a substantial amount of new material (some of it fresh off the press as the course was unfolding) and broaden my horizons. I could not have asked for a better intellectual experience and the students in the course, from Denmark, France, Germany, Iceland and the Netherlands taught me well, kept me on my toes and stimulated me to keep reading material related to ethics even now that the course is over. <br /></p><p>Teaching the course reinforced my belief that a course on ethics and on the impact that our field has on social justice should be required for all students in computer science. If you plan to run such a course, I strongly recommend that you consider the Ferreira-Vardi course as a blueprint. <br /></p><p><br /></p><p><br /></p><p><br /></p>Luca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.com2