This session is a celebration of the scientific and intellectual legacy of Oded Maler (1957-2018). Oded Maler was a computer scientist who did groundbreaking work in timed and hybrid systems theory and also a pioneer in connecting computational thinking with biological modelling. Oded did his PhD thesis entitled Finite Automata: Infinite Behavior, Learnability and Decomposition, under the supervision of Amir Pnueli at the Weizmann Institute of Science. After his postdoc at IRISA (Rennes, France) he obtained in 1994 a research position at the CNRS (French National Center of Scientific Research) and was then appointed Directeur de Recherche. Oded was revered for his wide-ranging interests and passion for humanities and philosophy of science. His intrepid efforts in building bridges between biology and computer science consisted in showing that a network of interacting genes and proteins is thinkable as an information processing system that evolves in space and time according to fundamental laws of physics, and can thus be formally described in mathematical terms. His research has opened the door to the application of computational models, tools, and insights developed within the fields of timed and hybrid systems to systems biology.
Oded was known not only for his impactful research achievements in automata theory and learning, timed and hybrid systems and logics, runtime monitoring and cyber-physical systems, but also for his indomitable will engaged in joining force with the biologists to push forward the understanding of mechanisms of diseases, the creation of diagnostic tools, therapeutic monitoring and new treatments. A few years after being diagnosed with cancer, computer scientist and biology enthusiast Oded Maler died of cancer at the age of 61, leaving behind an ongoing "Plan Cancer" project and high aspirations for us to continue the research path he has paved.
We are deeply thankful to Thao Dang, Eugene Asarin, and Alexandre Donze for coming to HSB to speak about the life and achievements of Oded. Below are titles and abstracts of their talks.
Abstract:
Oded Maler was one of the founders of the workshop Hybrid Systems Biology. His contributions in this domain could be traced back to his young days as a curious and brave computer scientist trying to break into Control Sciences, a neighbouring land yet full of distinct customs and traditions. This ambitious venture fruitfully impacted the evolution of the two domains. His results enlarged the theoretical boundary of his Computer Science homeland by extending timed systems to hybrid systems, addressing the fundamental decidability and complexity questions, laying the foundations for formal verification and synthesis of hybrid systems. Furthermore, these results have major intellectual impacts on the control community who began to embrace formal methods.
Being constantly attentive to other disciplines, Oded continued his journey and was particularly interested in systems biology (among others, such as embedded system scheduling and implementation, analog and mixed-signal circuits). His major contribution is his adaptation and proliferation of temporal logics, algorithmic analysis, and more generally hybrid computational thinking to this domain.
In this presentation, I will talk only about some of Oded’s influential contributions in hybrid systems along this remarkable odyssey.
Abstract:
Oded Maler often characterized as “barbaric” some of his approaches to solving complex problems. By this, he meant the modern meaning, i.e., “unsophisticated”, for example when he suggested to compute bunch of simulations to approximate reachable sets of dynamical systems - at a time when the trend was to fill pages of fancy theorems in advanced computational geometry or functional analysis. However, it is fair to say that he was in effect a true Barbarian but in the antique sense: Ancient Greeks called “Barbarians” those who were not Greek themselves. As a matter of fact, Oded as a scientist knew no boundaries: he wandered freely between theoretical computer science and applied mathematics, control theory, logics, Physics and Biology, etc. Always with humility, humor, and avid curiosity about local customs and knowledge he would bring in his own extended scientific baggage with genuine intention and efforts to mix in and contribute to the fields he was exploring. Systems Biology was a natural target of these explorations. There he found problems related to hybrid dynamical systems, another cross-field he contributed to pioneer. Together with various collaborators including biologists, both from wet labs and theoreticians, and myself, we experimented with and improved techniques such as systematic simulation and the monitoring of signal temporal logic, an extension of a logic used in program verification adapted to continuous and real-world processes, to help in particular with the difficult problem of parameter uncertainty in the modeling of living systems. I will try to recount some results we obtained and the avenues of research that this work from Oded’s legacy helped create and remain open today.
Abstract:
At timed level of abstraction, system behaviors are considered as sequences of discrete events (from a finite alphabet) and real-valued time lapses between them; or as discrete-valued signals over continuous time. Initiated by works of Alur & Dill and aiming modeling and verification of real-time sequences, this approach became quite popular was successfully extended to other domains. As usual in verification, sets of timed behaviors were defined by (timed) automata, and by logical formulas.
In mid 90s, Oded Maler initiated a search for simpler, suitable for engineers, and still powerful formalism to describe sets of timed behaviors. After overcoming many technical obstacles, timed regular expressions were born, and their equivalence to timed automata proven. In follow-up works, alternative formalisms have been proposed by several researchers.
In 2010s, Oded Maler and his group came back to timed regular expressions, with a new optics of pattern-matching: given a (large) record of timed behavior of a system, and a timed regular expression describing patterns of interest (e.g. faulty sequences), detect all the occurrences of the pattern in the record. Most of this research is automata-free: pattern-matching algorithms work directly on timed behaviors. Efficient algorithms have been developed and implemented, allowing off-line and on-line pattern-matching, and using several formalisms for pattern specification, and applications to monitoring prospected.
In this talk I will present the timed view on system behaviors, and the two periods of timed regular expressions: theoretical study on expressiveness from 1990s and practice-oriented works on pattern-matching and monitoring from 2010s. No special knowledge is required from the audience. This will also be a memorial talk, on Oded’s philosophical, creative and personal style of choosing research topics, leading research, and supervising students and co-workers.