Invited Speaker: Rance Cleaveland
Rance Cleaveland is Professor of Computer Science at the University of Maryland in College Park, w here he also serves as Associate Dean of Research for the College of Computing, Mathematical and Natural Sciences. He has published widely in the areas of software verification and validation, formal methods, model checking, software specification formalisms, and verification tools. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University, and M.S. and Ph.D. degrees from Cornell University. He is a Fellow of the IEEE and recently finished a four-year stint as Division Director of Computing and Communication Foundations at the US National Science Foundation.
Query-Checking for Finite Linear-time Temporal Logic
This talk addresses the following problem: given a finite set of observations of system behavior, each observation itself being a finite sequence of system states, and a query consisting of a Finite Linear-Time Temporal Logic (LTL) formula with missing sub-formulas, compute missing the missing sub-formulas that make the formula true for all observations. This so-called query-checking problem has many applications in the analysis of time-series data, including server logs and financial trend data, as well as generally in system comprehension and system-specification mining. The presentation first introduces Finite LTL, which is the well-known LTL logic of Pnueli interpreted over finite, rather than infinite, state sequences. It will then show how automata may be constructed from such formulas that recognize exactly the sequences making the formula true, and how these automata may be adapted to Finite LTL queries in which sub-formulas are missing. A procedure is then described that uses the automaton representation of such a query to solve for the missing sub-formulas for a given a set of finite state sequences. Preliminary experimental results of a prototype implementation are also given. This work is joint with Sam Huang.
Invited Speaker: Giuseppe De Giacomo
Giuseppe De Giacomo is currently a Professor of Computer Science at the Department of Computer Science of the University of Oxford. For several years he has been a professor at the Department of Computer, Control and Management Engineering of the University of Roma "La Sapienza". His research activity has concerned theoretical, methodological, and practical aspects in different areas of AI and CS, most prominently Knowledge Representation, Reasoning about Actions, Generalized Planning, Autonomous Agents, Service Composition, Business Process Modeling, and Data Management and Integration. He is AAAI Fellow, ACM Fellow, and EurAI Fellow. He has got an ERC Advanced Grant for the project WhiteMech: White-box Self Programming Mechanisms (2019-2024). He has been the Program Chair of ECAI 2020. He is on the Board of EurAI.
Linear-time Temporal Logics on Finite Traces
In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of processes modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics on infinite traces have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption has emerged. We will survey linear temporal logics on finite traces, including LTLf, LDLf, and pure-past LTL, reviewing the main results on Reasoning, Verification, and Synthesis. The talk will also draw connections with work in AI planning, Non-Markovin Decision Processes, Reinforcement Learning, and BPM Declarative Process Modeling, that will then be elaborated on in separate talks by workshop participants.
Invited Speaker: Sheila McIlraith
Sheila McIlraith is a Professor in the Department of Computer Science at the University of Toronto, a Canada CIFAR AI Chair (Vector Institute), and an Associate Director at the Schwartz Reisman Institute for Technology and Society. Prior to joining U of T, McIlraith spent six years as a Research Scientist at Stanford University, and one year at Xerox PARC. McIlraith’s research is in the area of AI knowledge representation and reasoning, and machine learning where she currently studies sequential decision-making, broadly construed, with a focus on human-compatible AI. McIlraith is a Fellow of the ACM and the Association for the Advancement of Artificial Intelligence (AAAI). She and co-authors have been recognized with two test-of-time awards from the International Semantic Web Conference (ISWC) in 2011, and from the International Conference on Automated Planning and Scheduling (ICAPS) in 2022.
Automated Planning with LTL: Techniques, Advances, and its Broad Applicability
Given a description of the dynamics of an environment, the initial state of the world, and a goal condition, automated symbolic planning generates a plan – typically a sequence of actions – that, when executed starting in the initial state, achieves the goal condition. Over the last 20+ years, research in automated planning has resulted in highly efficient algorithms for plan generation under varying models of the environment and goal conditions. In this talk, I’ll briefly review this literature, focusing on techniques for planning with temporally extended goals expressed in syntactic variants of LTL and regular expressions, interpreted over finite or infinite traces. I’ll show how planning in deterministic or nondeterministic systems with such temporally extended goals (or preferences) can be used as the computational core for a diverse set of tasks from web service composition to narrative understanding, goal recognition, automated diagnosis, and reactive synthesis. I’ll conclude with a brief discussion of how some of these same insights have been repurposed in the context of reinforcement learning, solving problems that otherwise could not be solved.
Invited Speaker: Marco Montali
Marco Montali is Full Professor in the Faculty of Engineering at the Free University of Bozen-Bolzano, Italy, where he also coordinates the MSc Program in Computational Data Science. The Leitmotiv of his research is to develop novel, foundational and applied techniques grounded in artificial intelligence, formal methods, and data science to create intelligent agents and information systems that combine processes and data. He has served as PC Chair of BPM 2018, RuleML+RR 2019, ICPM 2020, and CBI 2021, as General Chair of ICPM 2022 and EDOC 2022, and is steering committee member of the IEEE task force on process mining. He is co-author of more than 250 papers and recipient of 10 best paper awards and 2 test-of-time awards. He received the 2015 “Marco Somalvico” award, given by the Italian Association of Artificial Intelligence to the best under 35 Italian researcher advancing the state-of-the-art in artificial intelligence.
Declarative Process Management and mining: A Killer Application for LTLf
Business process management (BPM) is a discipline at the intersection between operations management, computer science, and software and systems engineering, whose grand goal is to support managers, analysts, and domain experts in the design, deployment, enactment, and continuous improvement of (work) processes within an organisation. While processes are traditionally managed in a top-down manner, process mining techniques are revolusionatising BPM, making it possible to automatically discover process models, check conformance between expected and actual executions, monitor and formulate predictions, and ultimately continuously improve processes based on the factual event data recorded inside information systems. In this talk, we focus on the widespread class of knowledge-intensive processes, which challenge the foundations of BPM and process mining, due to their inherent flexibility. We argue that such processes cannot be satisfactory modelled nor understood using conventional, procedural process modelling languages, but are instead best captured using a declarative approach based on temporal constraints. We ground our discussion on one of the most prominent languages in the declarative BPM spectrum: Declare. We show that Declare is naturally formalised in LTLf, and explain how the automata-theoretic characterisation of LTLf provides a solid, effective basis to elegantly solve a variety of central BPM/process mining tasks: model verification, enactment, anticipatory monitoring, and process discovery. In doing so, we touch on interesting recent extensions of LTLf dealing with data and uncertainty.
Invited Speaker: Kristin Yvonne Rozier
Professor Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA and three semesters as an Assistant Professor at the University of Cincinnati. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Dr. Rozier's research focuses on automated techniques for the formal specification, validation, and verification of safety critical systems. Her primary research interests include: design-time checking of system logic and system requirements; runtime system health management; and safety and security analysis. Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; the NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award. She holds an endowed position as Building a World of Difference faculty fellow, is an Associate Fellow of AIAA, and is a Senior Member of IEEE, ACM, and SWE. Dr. Rozier has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.
On the Effectiveness of Mission-time Linear Temporal Logic (MLTL) in AI Applications
Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the temporal operators of LTL, enabling unit-agnostic specification over finite traces. It is arguably the most-used variation of MTL, and the most-used subset of STL in industrial and AI applications. MLTL optimizes the trade-off between expressibility of a wide range of realistic requirements and the ability to author generic, easy-to-validate formulas. We highlight successful AI applications centered around MLTL requirements, including Robonaut2 and the NASA Lunar Gateway Vehicle System Manager. We overview advances in analyzing MLTL, explain the motivation driving these developments, and point out the gaps in the state of the art where there are needs for future work.
Invited Speaker: Ufuk Topcu
Ufuk Topcu is an Associate Professor in the Department of Aerospace Engineerin at The University of Texas at Austin, where he directs the Autonomos Systems Group. Ufuk’s research focuses on the theoretical and algorithmic aspects of the design and verification of autonomous systems, typically at the intersection of formal methods, reinforcement learning, and control theory. He takes a relatively broad view on autonomy and tends to tackle abstract problems motivated by challenges cutting across multiple applications of autonomy.
Automaton-Based Representations of Task Knowledge from Generative Language Models
Automaton-based representations of task knowledge play an important role in control, planning, and learning for sequential decision-making. However, obtaining the high-level task knowledge required to build such automata is often difficult. Meanwhile, large-scale generative language models can automatically generate relevant task knowledge. However, the textual outputs from generative langauge models cannot be formally verified or used for sequential decision-making. I will discuss our recent exploration into constructing automaton-based encodings of high-level task knowledge from a brief natural-language description of the task goal. I will also discuss how the outcomes may be integrated with formal verification and task-guided reinforcement learning.
Invited Speaker: Moshe Vardi
Moshe Y. Vardi is a University Professor, and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the author and co-author of over 700 papers, as well as two books. He is the recipient of several scientific awards, is a fellow of several societies, and a member of several honorary academies. He holds eight honorary doctorates. He is a Senior Editor of Communications of the ACM, the premier publication in computing, focusing on societal impact of information technology.
From Infinite to Finite Horizons
Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the chalenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.