Related papers: The Refinement Calculus of Reactive Systems

The paper presents our research on quantifier elimination (QE) for compositional reasoning and verification. For compositional reasoning, QE provides the foundation of our approach, serving as the calculus for composition to derive the…

We present ReAct!, an interactive tool for high-level reasoning for cognitive robotic applications. ReAct! enables robotic researchers to describe robots' actions and change in dynamic domains, without having to know about the syntactic and…

Reinforcement learning with verifiable rewards (RLVR) has proven effective in eliciting complex reasoning in large language models (LLMs). However, standard RLVR training often leads to excessively verbose processes (in reasoning tasks) and…

The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, specifications…

Reward Machines (RMs) are an established mechanism in Reinforcement Learning (RL) to represent and learn sparse, temporally extended tasks with non-Markovian rewards. RMs rely on high-level information in the form of labels that are emitted…

Reinforcement learning (RL) has become a central post-training tool for improving the reasoning abilities of large language models (LLMs). In these systems, the rollout, the trajectory sampled from a prompt to termination, including…

With the rise of LLMs, there is an increasing need for intelligent recommendation assistants that can handle complex queries and provide personalized, reasoning-driven recommendations. LLM-based recommenders show potential but face…

We present assume-guarantee contracts for continuous-time linear dynamical systems with inputs and outputs. These contracts are used to express specifications on the dynamic behaviour of a system. Contrary to existing approaches, we use…

Conditional term rewriting is an intuitive yet complex extension of term rewriting. In order to benefit from the simpler framework of unconditional rewriting, transformations have been defined to eliminate the conditions of conditional term…

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a…

Chemical reaction networks, or CRNs, are known to stably compute semilinear Boolean-valued predicates and functions, provided that all reactions are irreversible. However, this property does not hold for wet-lab implementations, as all…

This thesis is devoted to the study of a calculus that describes the application of conditional rewriting rules and the obtained results at the same level of representation. We introduce the rewriting calculus, also called the rho-calculus,…

Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically hard, and writing…

An accurate and simple analytical model for the computation of the reflection amplitude and phase of Reconfigurable Intelligent Surfaces is presented. The model is based on a transmission-line circuit representation of the RIS which takes…

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change.…

Large language models (LLMs) can improve their accuracy on various tasks through iteratively refining and revising their output based on feedback. We observe that these revisions can introduce errors, in which case it is better to roll back…

The Reservoir Computing (RC) paradigm posits that sufficiently complex physical systems can be used to massively simplify pattern recognition tasks and nonlinear signal prediction. This work demonstrates how random topological magnetic…

The modelling, specification and study of the semantics of concurrent reactive systems have been interesting research topics for many years now. The aim of this thesis is to exploit the strengths of the (co)algebraic framework in modelling…

Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL,…

Large Multimodal Models (LMMs) excel at comprehending human instructions and demonstrate remarkable results across a broad spectrum of tasks. Reinforcement Learning from Human Feedback (RLHF) and AI Feedback (RLAIF) further refine LLMs by…