EVENT
Event News
ERATO Project Colloquium by S. Akshay (Indian Institute of Technology Bombay)
On Tuesday 6 and Wednesday 7 August, S. Akshay (Indian Institute of Technology Bombay) will give three talks for our project colloquium. Further details can be found below.
Talk 1:
Certified Policy Verification and Synthesis
Abstract:
Markov decision processes can be viewed as transformers of probability distributions, giving rise to a sequence of distributions over MDP states.
This view is useful in many applications, e.g., modeling robot swarms or chemical reaction networks, where the behavior is naturally interpreted as probability distributions over states. Somewhat surprisingly, in this setting basic reachability and safety problems turn out to be computationally intractable. The issue is further complicated by the question of how much memory is allowed: even for simple examples, policies for safety objectives over distributions can require infinite memory and randomization.
In light of this, we ask what can one do to tackle these problems in theory and in practice? After taking a look at some theoretical insights, we adopt an over-approximation route to approach these questions. Inspired by the success of invariant synthesis in program verification, we develop a framework for inductive template-based synthesis of certificates and policies for safety and reach-avoidance objectives in MDPs. We show the effectiveness of our approach as well as explore limitations and future perspectives.
[Based on Joint Work with Krishnendu Chatterjee, Tobias Meggendorfer and Djordje Zikelic at CAV'23 and IJCAI'24]
Talk 2:
Tractable Representations for Boolean Functional Synthesis
Abstract:
It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing the system is a functional problem: to provide functions that produce outputs from inputs. The question we ask is if we can automatically synthesize such a function from the given relation? This question has generated a lot of interest in recent years, especially in the Boolean setting, where despite theoretical hardness results, many techniques and tools have been developed that now scale surprisingly well. In this talk, we shine a light on this problem from a Knowledge Representation perspective. We identify structural properties and develop normal forms for the specification that guarantee provably efficient synthesis. Further, we move towards a characterization of what makes Boolean functional synthesis easy and examine techniques to compile into such forms.
[Based on joint work with Supratik Chakraborty, Sahil Jain and Shetal Shah at CAV'23 and AMAI'23]
Talk 3:
History and Future in Timed Automata: A Unified Model for Real-Time
Abstract:
Timed automata are a well-established model for real-time systems, which use real-valued variables called clocks to model time. Timed specifications, however, are often written in timed temporal logics such as MTL/MITL, which are more easily translated into a related model of event-clock automata (ECA). Even though ECA is a subclass of timed automata, the translation from ECA to Timed automata is expensive. Hence a natural question that arises is whether there is a framework that can capture features of Timed automata, Event-clock automata and more, thus providing directly model-check timed temporal specifications over timed systems.
In this work, we propose a new model, called Generalized Timed Automata (GTA), that uses history and future clocks to unify the features of various models such as timed automata, event-clock automata (with and without diagonal constraints), and even automata with timers. We show a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation of our model and algorithm in TChecker, an open-source platform for timed automata analysis and show promising results. Finally, we will tackle questions of liveness in GTA and, if time permits, explain how this could lead to a new, effective and fast approach for MITL model checking.
[Based on joint work with Paul Gastin, R. Govind, Aniruddha Joshi and B Srivathsan at CAV'23 and CONCUR'24]
Time/Date:
[Talk 1,2] 15:00- / Tuesday 6 August ,2024
[Talk 3] 16:30- / Wednesday 7 August ,2024
Place:
NII Room 1310A and Online
Link:
For the latest information about ERATO colloquium/seminar, please see the webpage.
https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit
Contact:
Kittiphon Phalakarn (ERATO MMSD Colloquium Organizer)
Email: kphalakarn[at] nii.ac.jp