Ryan Matheu
University of Maryland, College Park
I am an Electrical & Computer Engineering Ph.D. student and Clark Doctoral Fellow at the University of Maryland, College Park, working under the mentorship of Professor John S. Baras, Distinguished University Professor and Endowed Lockheed Martin Chair in Systems Engineering, and Professor Calin Belta, Brendan Iribe Endowed Professor of Electrical & Computer Engineering and Computer Science.
My research focuses on formal methods for the specification, verification, and control of autonomous systems. Much of my work centers on ternary temporal logic. Temporal logics such as Signal Temporal Logic (STL) provide the formal semantics needed for verification and correct-by-construction control synthesis, but their interpretation is binary. Kleene’s ternary logic $K_3$ introduces a third truth value Unknown to represent the case where there is not enough information to determine whether a specification is True or False. I apply ternary temporal logic to online monitoring and control synthesis over partial trajectories, and to the training of differentiable ternary logic gate networks. I also contribute to integrated data-driven and model-based systems engineering tools for trusted autonomous cyber-physical systems.
Research
Ternary logic for autonomous systems
Temporal logic specifications are typically evaluated with Boolean semantics, which force a verdict of True or False even when a task is still being executed. This line of work uses the ternary logic K3 to evaluate specifications over partial trajectories and partial executions, with applications to gradient-based and mixed-integer control synthesis, online monitoring, and formal verification with timed automata.
Differentiable Ternary Temporal Logic Semantics with Polynomial Surrogate Networks
Smooth approximations of STL enable gradient-based control synthesis, but the interpretation of STL is binary, and a task that has not been completed by the end of a prediction horizon is assigned a verdict of False. This work shows that the satisfaction of any ternary temporal logic formula over a partial trajectory can be represented exactly as a Differentiable Ternary Logic Gate Network (DTLGN), and introduces a moment propagation scheme that yields a smooth likelihood of satisfaction. The animation shows a closed-loop (MPC) rollout on a 7-DoF manipulator, where the presence of a human causes the manipulator to fall back and place the item into the secondary bin.
Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis
This work formulates the qualitative semantics of ternary temporal logic over partial trajectories, where Unknown captures the case in which a partial trajectory has neither satisfied nor violated a specification. We introduce mixed-integer linear encodings for ternary temporal logic over K3, allowing for correct-by-construction control of linear dynamical systems via mixed-integer programming. The figure shows synthesized trajectories for two initial battery levels (left), where the robot must navigate to the charger at C before proceeding to B when the battery is below 80%, and a multi-agent planning task (right).
OMTBT: Online Monitoring of Temporal Behavior Trees with Applications to Closed-Loop Learning
This work proposes quantitative semantics for the online monitoring of temporal logic task specifications over partial executions, composed of an inner logic based on STL and an outer logic in propositional ternary logic. The semantics are a conservative approximation of the final robustness of the specification and are used to design reward functions for reinforcement learning. The animation shows a rollout of the learned policy on a pick-and-place task, which achieved a 100% success rate over 100 test trials.
BT2Automata: Expressing Behavior Trees as Automata for Formal Control Synthesis
This work presents a translation from hierarchical task specifications, evaluated over a balanced ternary logic, to Timed Automata (TA). The TA representation allows for the use of model checkers such as UPPAAL to check for inconsistencies and falsify task specifications with timing constraints, and enables automaton-based and sampling-based control synthesis for robotic tasks.
Systems engineering for trusted autonomy
Autonomous cyber-physical systems require systems engineering methodologies that span both model-based design and data-driven ML/AI components. As part of a team in the Systems Engineering and Integration Lab (SEIL), I contribute to open-source tools that integrate formal verification into the systems engineering lifecycle.
IDDMBSE: Integrating Data-Driven and Model-Based Systems Engineering for Trusted Autonomous Cyber-Physical Systems
IDDMBSE is a collaborative effort in SEIL that extends the model-based systems engineering V-process with a data-driven loop at every step. The methodology is realized as an open-source tool chain spanning SysML-to-ROS architecture mapping, design-space exploration, and formal and runtime verification, and is demonstrated on a trusted autonomous ground robot. The figure shows the contested-terrain Isaac Sim test range released with the tool chain.
rcllean: A ROS 2 Client Library for Lean 4
rcllean is a ROS 2 client library for the Lean 4 programming language and theorem prover. It enables users to write ROS 2 nodes and theorems about their properties in Lean 4.
Robo Lean: Formalized Robotics in Lean 4
Robo Lean is a Lean 4 library, built on Mathlib, that formalizes the mathematical core of robot manipulation from Murray, Li, and Sastry, including rigid transforms, rotations, twists, screws, and wrenches.
Outside the lab
A hiking trip through Saguaro National Park, and a striped bass caught on the Chesapeake Bay.
