My former colleague Philipp Rümmer co-organised a workshop on topics broadly concerned with applying logic to determine properties of various kinds of systems. I only managed to attend the morning session of the workshop, so the report below is very incomplete.
The invited talk was delivered by Radu Grosu. He covered a very broad and fascinating range of topics from philosophical ruminations about time and quantum mechanics, semantics of temporal logics to computerised analysis of music. The main point I took away was that time and frequency are well known dual concepts. This duality is the foundation of several techniques in physics and signal processing that exploit properties of the frequency domain to make conclusions about the time domain. The duality of time and frequency can also be used in the analysis of hybrid systems using temporal logic.
The idea of embedding frequency semantics into a temporal logic appealed to me a lot. I find that adding a modality or operator to a logic forces me to think about that operator very seriously and helps me truly understand and apply it. During the talk I found myself trying to think of standard hybrid systems and their properties in terms of the frequency domain and what it might mean to interpret a temporal logic over this domain. Moreover, I wonder if standard frequency domain techniques can be leveraged to obtain model checking algorithms for such a logic. I imagine that Radu and his collaborators have already answered some of these questions.
In addition to being thought provoking and having interesting mathematics, there were several applications that scored very high on my internal coolness meter. I can’t remember the details of the biological examples, except that they were there. Radu also had examples of a few bars of classical and blues music that could be succinctly described in such a logic.
Descriptions of the other talks can be found in the workshop proceedings.
Over lunch, I had the chance to meet Ashish Tiwari from SRI for the first time. He has done pioneering work in the intersection of decision procedures, program verification, abstract interpretation, hybrid systems and systems biology (to name only a few areas). I hope to cover some of his work in future posts.